Step
*
1
of Lemma
kripke2b-baire-seq_wf
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 ⟶ ℕ)}
BY
{ (MemTypeCD THEN Auto) }
1
.....set predicate.....
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)
⊢ a = cantor2baire(b) ∈ (ℕx ⟶ ℕ)
Latex:
Latex:
1. a : \mBbbN{} {}\mrightarrow{} \mBbbN{}
2. x : \mBbbN{}
3. F : \mforall{}b:\{b:\mBbbN{} {}\mrightarrow{} \mBbbN{}| a = b\} . \mexists{}n:\mBbbN{}. ((b n) \mgeq{} ((a x) + 1) )
4. b : \mBbbN{} {}\mrightarrow{} \mBbbB{}
5. eq-finite-seqs(a;cantor2baire(b);x) \mmember{} \mBbbB{}
6. \muparrow{}eq-finite-seqs(a;cantor2baire(b);x)
\mvdash{} cantor2baire(b) \mmember{} \{b:\mBbbN{} {}\mrightarrow{} \mBbbN{}| a = b\}
By
Latex:
(MemTypeCD THEN Auto)
Home
Index