Nuprl Lemma : isect2_functionality_wrt_subtype_rel

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


Definitions occuring in Statement :  isect2: T1 ⋂ T2 uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a subtype_rel: A ⊆B isect2: T1 ⋂ T2 bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else 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

\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