---

Step * 1 1 of Lemma not-choice-baire-to-nat-ssq


1. ∀P:((ℕ ⟶ ℕ) ⟶ ℕ) ⟶ ℙ. (∀t:(ℕ ⟶ ℕ) ⟶ ℕ. (↓P[t]) ⇐⇒ ↓∀t:(ℕ ⟶ ℕ) ⟶ ℕ. P[t])
2. ∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ.  ((f = g ∈ (ℕM f ⟶ ℕ)) ⇒ ((F f) = (F g) ∈ ℕ))
⊢ False
BY
{ ((Assert ⌜¬unsquashed-WCP⌝⋅ THENA Auto)
   THEN D (-1)
   THEN (D 0 THENA Auto)
   THEN (InstHyp [⌜F⌝] (-2)⋅ THENA Auto)
   THEN ExRepD
   THEN InstConcl [⌜M⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}P:((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbP{}.  (\mforall{}t:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  (\mdownarrow{}P[t])  \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}\mforall{}t:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  P[t])
2.  \mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \mexists{}M:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  \mforall{}f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g)))
\mvdash{}  False


By

---

Latex:
((Assert  \mkleeneopen{}\mneg{}unsquashed-WCP\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  (D  0  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}F\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  InstConcl  [\mkleeneopen{}M\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index