Nuprl Lemma : subtype_rel_simple_product

[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] product: x:A × B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a so_lambda: λ2x.t[x] so_apply: x[s] all: x:A. B[x] subtype_rel: A ⊆B
Lemmas referenced :  subtype_rel_product subtype_rel_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule lambdaEquality independent_isectElimination hypothesis lambdaFormation because_Cache axiomEquality isect_memberEquality equalityTransitivity equalitySymmetry universeEquality

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

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

Theory : subtype_0

Home Index