---

Step * 1 2 of Lemma pseudo-bounded-not-unbounded


1. S : {S:Type| S ⊆r ℕ} 
2. S ⊆r ℕ
3. ∀n:ℕ. (n ∈ S ∈ ℙ)
4. ∀B:ℕ. ∃n:{B...}. (n ∈ S)
5. f : B:ℕ ⟶ {B...}
6. ∀B:ℕ. (f B ∈ S)
7. ∃k:ℕ. ∀n:{k...}. f n < n
⊢ False
BY
{ ExRepD }

1
1. S : {S:Type| S ⊆r ℕ} 
2. S ⊆r ℕ
3. ∀n:ℕ. (n ∈ S ∈ ℙ)
4. ∀B:ℕ. ∃n:{B...}. (n ∈ S)
5. f : B:ℕ ⟶ {B...}
6. ∀B:ℕ. (f B ∈ S)
7. k : ℕ
8. ∀n:{k...}. f n < n
⊢ False

---

Latex:

---

Latex:

1.  S  :  \{S:Type|  S  \msubseteq{}r  \mBbbN{}\} 
2.  S  \msubseteq{}r  \mBbbN{}
3.  \mforall{}n:\mBbbN{}.  (n  \mmember{}  S  \mmember{}  \mBbbP{})
4.  \mforall{}B:\mBbbN{}.  \mexists{}n:\{B...\}.  (n  \mmember{}  S)
5.  f  :  B:\mBbbN{}  {}\mrightarrow{}  \{B...\}
6.  \mforall{}B:\mBbbN{}.  (f  B  \mmember{}  S)
7.  \mexists{}k:\mBbbN{}.  \mforall{}n:\{k...\}.  f  n  <  n
\mvdash{}  False


By

---

Latex:
ExRepD

---

Home Index