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