Nuprl Lemma : subtype_rel_function

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


Definitions occuring in Statement :  uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] function: x:A ⟶ B[x] 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 functionExtensionality applyEquality hypothesisEquality thin hypothesis sqequalHypSubstitution sqequalRule functionEquality axiomEquality lemma_by_obid isectElimination isect_memberEquality because_Cache equalityTransitivity equalitySymmetry universeEquality

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

Date html generated: 2016_05_13-PM-03_18_38
Last ObjectModification: 2015_12_26-AM-09_08_25

Theory : subtype_0

Home Index