---

Step * 1 of Lemma pseudo-bounded-is-bounded


1. [S] : {S:Type| S ⊆r ℕ} 
2. S ⊆r ℕ
3. m : S
4. ∀f:ℕ ⟶ S. ∃k:ℕ. ∀n:{k...}. f n < n
5. F : f:(ℕ ⟶ S) ⟶ ℕ
6. ∀f:ℕ ⟶ S. ∀n:{F f...}.  f n < n
7. ∀f:ℕ ⟶ S. ∃n:ℕ. ∀g:ℕ ⟶ S. ((f = g ∈ (ℕn ⟶ S)) ⇒ ((F f) = (F g) ∈ ℕ))
⊢ ∃B:ℕ. ∀n:S. (n ≤ B)
BY
{ ((InstHyp [⌜λn.m⌝] (-1)⋅ THENA Auto) THEN Reduce 0 THEN ExRepD) }

1
1. [S] : {S:Type| S ⊆r ℕ} 
2. S ⊆r ℕ
3. m : S
4. ∀f:ℕ ⟶ S. ∃k:ℕ. ∀n:{k...}. f n < n
5. F : f:(ℕ ⟶ S) ⟶ ℕ
6. ∀f:ℕ ⟶ S. ∀n:{F f...}.  f n < n
7. ∀f:ℕ ⟶ S. ∃n:ℕ. ∀g:ℕ ⟶ S. ((f = g ∈ (ℕn ⟶ S)) ⇒ ((F f) = (F g) ∈ ℕ))
8. n : ℕ
9. ∀g:ℕ ⟶ S. (((λn.m) = g ∈ (ℕn ⟶ S)) ⇒ ((F (λn.m)) = (F g) ∈ ℕ))
⊢ ∃B:ℕ. ∀n:S. (n ≤ B)

---

Latex:

---

Latex:

1.  [S]  :  \{S:Type|  S  \msubseteq{}r  \mBbbN{}\} 
2.  S  \msubseteq{}r  \mBbbN{}
3.  m  :  S
4.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  S.  \mexists{}k:\mBbbN{}.  \mforall{}n:\{k...\}.  f  n  <  n
5.  F  :  f:(\mBbbN{}  {}\mrightarrow{}  S)  {}\mrightarrow{}  \mBbbN{}
6.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  S.  \mforall{}n:\{F  f...\}.    f  n  <  n
7.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  S.  \mexists{}n:\mBbbN{}.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  S.  ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g)))
\mvdash{}  \mexists{}B:\mBbbN{}.  \mforall{}n:S.  (n  \mleq{}  B)


By

---

Latex:
((InstHyp  [\mkleeneopen{}\mlambda{}n.m\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  Reduce  0  THEN  ExRepD)

---

Home Index