### Nuprl Lemma : subtype_rel_simple_product

`∀[A,B,C,D:Type].  ((A × B) ⊆r (C × D)) supposing ((B ⊆r D) and (A ⊆r C))`

Proof

Definitions occuring in Statement :  uimplies: `b supposing a` subtype_rel: `A ⊆r 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: `b supposing a` so_lambda: `λ2x.t[x]` so_apply: `x[s]` all: `∀x:A. B[x]` subtype_rel: `A ⊆r 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

Latex:
\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