Nuprl Lemma : union_subtype_base

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


Proof




Definitions occuring in Statement :  uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] union: left right base: Base universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a subtype_rel: A ⊆B member: t ∈ T
Lemmas referenced :  istype-universe subtype_rel_wf base_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaEquality_alt,  unionElimination thin sqequalRule baseApply closedConclusion baseClosed cut hypothesisEquality applyEquality hypothesis sqequalHypSubstitution Error :unionIsType,  introduction extract_by_obid isectElimination Error :universeIsType,  Error :inhabitedIsType,  universeEquality

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



Date html generated: 2019_06_20-AM-11_19_28
Last ObjectModification: 2018_10_06-AM-09_07_21

Theory : subtype_0


Home Index