### Nuprl Lemma : subtype_rel_isect

`∀[A,T:Type]. ∀[B:T ⟶ Type].  uiff(A ⊆r (⋂x:T. B[x]);∀[x:T]. (A ⊆r B[x]))`

Proof

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

Latex:
\mforall{}[A,T:Type].  \mforall{}[B:T  {}\mrightarrow{}  Type].    uiff(A  \msubseteq{}r  (\mcap{}x:T.  B[x]);\mforall{}[x:T].  (A  \msubseteq{}r  B[x]))

Date html generated: 2016_05_13-PM-03_18_52
Last ObjectModification: 2015_12_26-AM-09_08_08

Theory : subtype_0

Home Index