Nuprl Lemma : axiom-choice-1X-quot

`∀X:Type. ∀P:(ℕ ⟶ ℕ) ⟶ X ⟶ ℙ.  ((∀f:ℕ ⟶ ℕ. ⇃(∃m:X. (P f m))) `` ⇃(∃F:(ℕ ⟶ ℕ) ⟶ X. ∀f:ℕ ⟶ ℕ. (P f (F f))))`

Proof

Definitions occuring in Statement :  quotient: `x,y:A//B[x; y]` nat: `ℕ` prop: `ℙ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` true: `True` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` uall: `∀[x:A]. B[x]` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` exists: `∃x:A. B[x]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a`
Lemmas referenced :  equiv_rel_true true_wf exists_wf quotient_wf all_wf canonicalizable-nat-to-nat canonicalizable_wf trivial-quotient-true nat_wf axiom-choice-quot
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin functionEquality hypothesis independent_functionElimination isectElimination hypothesisEquality because_Cache sqequalRule lambdaEquality cumulativity applyEquality independent_isectElimination universeEquality

Latex:
\mforall{}X:Type.  \mforall{}P:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbP{}.
((\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \00D9(\mexists{}m:X.  (P  f  m)))  {}\mRightarrow{}  \00D9(\mexists{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  X.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  (P  f  (F  f))))

Date html generated: 2016_05_14-PM-09_42_33
Last ObjectModification: 2016_01_06-PM-01_29_32

Theory : continuity

Home Index