Nuprl Lemma : subtype_rel_union

[A,B,C,D:Type].  ((A B) ⊆(C D)) supposing ((B ⊆D) and (A ⊆C))


Definitions occuring in Statement :  uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] union: left right universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a subtype_rel: A ⊆B
Lemmas referenced :  subtype_rel_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaEquality unionElimination thin inlEquality hypothesisEquality applyEquality hypothesis sqequalHypSubstitution sqequalRule inrEquality because_Cache unionEquality axiomEquality lemma_by_obid isectElimination isect_memberEquality equalityTransitivity equalitySymmetry universeEquality

\mforall{}[A,B,C,D:Type].    ((A  +  B)  \msubseteq{}r  (C  +  D))  supposing  ((B  \msubseteq{}r  D)  and  (A  \msubseteq{}r  C))

Date html generated: 2016_05_13-PM-03_18_42
Last ObjectModification: 2015_12_26-AM-09_08_21

Theory : subtype_0

Home Index