### Nuprl Lemma : double_isect_subtype_rel

`∀[T1,T2:Type]. ∀[B:T1 ⟶ T2 ⟶ Type]. ∀[x:T1]. ∀[y:T2].  ((⋂x:T1. ⋂y:T2.  B[x;y]) ⊆r B[x;y])`

Proof

Definitions occuring in Statement :  subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2]` isect: `⋂x:A. B[x]` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` so_apply: `x[s1;s2]` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` implies: `P `` Q` prop: `ℙ`
Lemmas referenced :  equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lambdaEquality isectElimination hypothesisEquality equalityTransitivity equalitySymmetry hypothesis thin isectEquality cumulativity applyEquality functionExtensionality lambdaFormation extract_by_obid sqequalHypSubstitution dependent_functionElimination independent_functionElimination axiomEquality isect_memberEquality because_Cache functionEquality universeEquality

Latex:
\mforall{}[T1,T2:Type].  \mforall{}[B:T1  {}\mrightarrow{}  T2  {}\mrightarrow{}  Type].  \mforall{}[x:T1].  \mforall{}[y:T2].    ((\mcap{}x:T1.  \mcap{}y:T2.    B[x;y])  \msubseteq{}r  B[x;y])

Date html generated: 2017_04_14-AM-07_14_04
Last ObjectModification: 2017_02_27-PM-02_49_57

Theory : subtype_0

Home Index