---

Step * of Lemma kripke2b-baire-seq_wf

∀[a:ℕ ⟶ ℕ]. ∀[x:ℕ]. ∀[F:∀b:{b:ℕ ⟶ ℕ| a = b ∈ (ℕx ⟶ ℕ)} . ∃n:ℕ. ((b n) ≥ ((a x) + 1) )].
  (kripke2b-baire-seq(a;x;F) ∈ (ℕ ⟶ 𝔹) ⟶ ℕ)
BY
{ ProveWfLemma }

1
1. a : ℕ ⟶ ℕ
2. x : ℕ
3. F : ∀b:{b:ℕ ⟶ ℕ| a = b ∈ (ℕx ⟶ ℕ)} . ∃n:ℕ. ((b n) ≥ ((a x) + 1) )
4. b : ℕ ⟶ 𝔹
5. eq-finite-seqs(a;cantor2baire(b);x) ∈ 𝔹
6. ↑eq-finite-seqs(a;cantor2baire(b);x)
⊢ cantor2baire(b) ∈ {b:ℕ ⟶ ℕ| a = b ∈ (ℕx ⟶ ℕ)} 

---

Latex:

---

Latex:
\mforall{}[a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[x:\mBbbN{}].  \mforall{}[F:\mforall{}b:\{b:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}|  a  =  b\}  .  \mexists{}n:\mBbbN{}.  ((b  n)  \mgeq{}  ((a  x)  +  1)  )].
    (kripke2b-baire-seq(a;x;F)  \mmember{}  (\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbN{})


By

---

Latex:
ProveWfLemma

---

Home Index