---

Step * of Lemma pseudo-bounded-not-unbounded

∀[S:{S:Type| S ⊆r ℕ} ]. (pseudo-bounded(S) ⇒ (¬(∀B:ℕ. ∃n:{B...}. (n ∈ S))))
BY
{ (Intro
   THEN (Assert S ⊆r ℕ BY
               (Unhide THEN Auto))
   THEN (Assert ∀n:ℕ. (n ∈ S ∈ ℙ) BY
               ((D 0 THENA Auto) THEN Assert ⌜n ∈ Base⌝⋅ THEN Auto))
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN Skolemize (-1) `f'
   THEN Auto) }

1
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

---

Latex:

---

Latex:
\mforall{}[S:\{S:Type|  S  \msubseteq{}r  \mBbbN{}\}  ].  (pseudo-bounded(S)  {}\mRightarrow{}  (\mneg{}(\mforall{}B:\mBbbN{}.  \mexists{}n:\{B...\}.  (n  \mmember{}  S))))


By

---

Latex:
(Intro
  THEN  (Assert  S  \msubseteq{}r  \mBbbN{}  BY
                          (Unhide  THEN  Auto))
  THEN  (Assert  \mforall{}n:\mBbbN{}.  (n  \mmember{}  S  \mmember{}  \mBbbP{})  BY
                          ((D  0  THENA  Auto)  THEN  Assert  \mkleeneopen{}n  \mmember{}  Base\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  Skolemize  (-1)  `f'
  THEN  Auto)

---

Home Index