### Nuprl Lemma : choice-principle_wf

`∀[T:Type]. (ChoicePrinciple(T) ∈ 𝕌')`

Proof

Definitions occuring in Statement :  choice-principle: `ChoicePrinciple(T)` uall: `∀[x:A]. B[x]` member: `t ∈ T` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` choice-principle: `ChoicePrinciple(T)` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` and: `P ∧ Q`
Lemmas referenced :  equiv_rel_true true_wf quotient_wf iff_wf all_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule thin instantiate lemma_by_obid sqequalHypSubstitution isectElimination functionEquality cumulativity hypothesisEquality universeEquality lambdaEquality applyEquality hypothesis because_Cache independent_isectElimination axiomEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[T:Type].  (ChoicePrinciple(T)  \mmember{}  \mBbbU{}')

Date html generated: 2016_05_14-PM-09_42_14
Last ObjectModification: 2016_01_11-PM-02_11_15

Theory : continuity

Home Index