---

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


1. S : {S:Type| S ⊆r ℕ} 
2. S ⊆r ℕ
3. ∀n:ℕ. (n ∈ S ∈ ℙ)
4. pseudo-bounded(S)
5. ∀B:ℕ. ∃n:{B...}. (n ∈ S)
6. f : B:ℕ ⟶ {B...}
7. ∀B:ℕ. (f B ∈ S)
⊢ False
BY
{ (D -4 With ⌜f⌝  THEN Auto) }

1
.....wf..... 
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)
⊢ f ∈ ℕ ⟶ S

2
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

---

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.  pseudo-bounded(S)
5.  \mforall{}B:\mBbbN{}.  \mexists{}n:\{B...\}.  (n  \mmember{}  S)
6.  f  :  B:\mBbbN{}  {}\mrightarrow{}  \{B...\}
7.  \mforall{}B:\mBbbN{}.  (f  B  \mmember{}  S)
\mvdash{}  False


By

---

Latex:
(D  -4  With  \mkleeneopen{}f\mkleeneclose{}    THEN  Auto)

---

Home Index