### Nuprl Lemma : isect_subtype_rel_trivial

`∀[A,C:Type]. ∀[B:A ⟶ Type].  (⋂x:A. B[x]) ⊆r C supposing ∃x:A. (B[x] ⊆r C)`

Proof

Definitions occuring in Statement :  uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` so_apply: `x[s]` exists: `∃x:A. B[x]` isect: `⋂x:A. B[x]` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` subtype_rel: `A ⊆r B` exists: `∃x:A. B[x]` so_apply: `x[s]` prop: `ℙ` so_lambda: `λ2x.t[x]`
Lemmas referenced :  exists_wf subtype_rel_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaEquality sqequalHypSubstitution productElimination thin hypothesisEquality applyEquality sqequalRule isectElimination equalityTransitivity equalitySymmetry hypothesis isectEquality axiomEquality lemma_by_obid isect_memberEquality because_Cache functionEquality cumulativity universeEquality

Latex:
\mforall{}[A,C:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].    (\mcap{}x:A.  B[x])  \msubseteq{}r  C  supposing  \mexists{}x:A.  (B[x]  \msubseteq{}r  C)

Date html generated: 2016_05_13-PM-03_18_58
Last ObjectModification: 2015_12_26-AM-09_08_00

Theory : subtype_0

Home Index