Nuprl Lemma : subtype_rel_transitivity

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


Definitions occuring in Statement :  uimplies: supposing a subtype_rel: A ⊆B uall: [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 istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule axiomEquality hypothesis universeIsType extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality isect_memberEquality_alt isectIsTypeImplies inhabitedIsType instantiate universeEquality lambdaEquality_alt applyEquality

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

Date html generated: 2020_05_19-PM-09_35_10
Last ObjectModification: 2019_12_05-PM-00_02_01

Theory : subtype_0

Home Index