---

Step * 1 1 1 of Lemma general-fan-theorem-troelstra-sq


1. X : n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ@i'
2. ∀f:ℕ ⟶ 𝔹. ⇃(∃n:ℕ. X[n;f])@i
3. ∃F:(ℕ ⟶ 𝔹) ⟶ ℕ. ∀f:ℕ ⟶ 𝔹. (X (F f) f)@i
⊢ ∀f:ℕ ⟶ 𝔹. ∃n:ℕ. X[n;f]
BY
{ ((ExRepD THENA Auto) THEN InstConcl [⌜F f⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbP{}@i'
2.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \00D9(\mexists{}n:\mBbbN{}.  X[n;f])@i
3.  \mexists{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  (X  (F  f)  f)@i
\mvdash{}  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}n:\mBbbN{}.  X[n;f]


By

---

Latex:
((ExRepD  THENA  Auto)  THEN  InstConcl  [\mkleeneopen{}F  f\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index