Nuprl Lemma : subtype_rel_sum

[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_union subtype_rel_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_isectElimination hypothesis sqequalRule axiomEquality isect_memberEquality because_Cache 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_44
Last ObjectModification: 2015_12_26-AM-09_08_13

Theory : subtype_0

Home Index