### Nuprl Lemma : isect2_functionality_wrt_subtype_rel

`∀[A1,B1,A2,B2:Type].  (A1 ⋂ B1 ⊆r A2 ⋂ B2) supposing ((A1 ⊆r A2) and (B1 ⊆r B2))`

Proof

Definitions occuring in Statement :  isect2: `T1 ⋂ T2` uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` subtype_rel: `A ⊆r B` isect2: `T1 ⋂ T2` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` guard: `{T}` bfalse: `ff`
Lemmas referenced :  subtype_rel_wf isect2_subtype_rel subtype_rel_transitivity isect2_wf isect2_subtype_rel2 bool_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule axiomEquality hypothesis lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality isect_memberEquality because_Cache equalityTransitivity equalitySymmetry lambdaEquality unionElimination equalityElimination applyEquality independent_isectElimination

Latex:
\mforall{}[A1,B1,A2,B2:Type].    (A1  \mcap{}  B1  \msubseteq{}r  A2  \mcap{}  B2)  supposing  ((A1  \msubseteq{}r  A2)  and  (B1  \msubseteq{}r  B2))

Date html generated: 2016_05_13-PM-04_10_45
Last ObjectModification: 2015_12_26-AM-11_22_47

Theory : subtype_1

Home Index