Nuprl Lemma : isect2_subtype_rel3
∀[A,B,C:Type]. A ⋂ B ⊆r C supposing (A ⊆r C) ∨ (B ⊆r C)
Proof
Definitions occuring in Statement :
isect2: T1 ⋂ T2,
uimplies: b supposing a,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
or: P ∨ Q,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
or: P ∨ Q,
subtype_rel: A ⊆r B,
prop: ℙ
Lemmas referenced :
or_wf,
subtype_rel_wf,
subtype_rel_transitivity,
isect2_wf,
isect2_subtype_rel,
isect2_subtype_rel2
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalHypSubstitution,
unionElimination,
thin,
sqequalRule,
axiomEquality,
hypothesis,
lemma_by_obid,
isectElimination,
hypothesisEquality,
isect_memberEquality,
because_Cache,
equalityTransitivity,
equalitySymmetry,
universeEquality,
independent_isectElimination
Latex:
\mforall{}[A,B,C:Type]. A \mcap{} B \msubseteq{}r C supposing (A \msubseteq{}r C) \mvee{} (B \msubseteq{}r C)
Date html generated:
2016_05_13-PM-03_58_10
Last ObjectModification:
2015_12_26-AM-10_51_07
Theory : bool_1
Home
Index