---

Step * 1 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) ∈ ℕ))
8. n : ℕ
9. ∀g:ℕ ⟶ S. (((λn.m) = g ∈ (ℕn ⟶ S)) ⇒ ((F (λn.m)) = (F g) ∈ ℕ))
⊢ ∃B:ℕ. ∀n:S. (n ≤ B)
BY
{ (D 0 With ⌜imax(F (λn.m);n)⌝  THEN Auto THEN RenameVar `k' (-1)) }

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) ∈ ℕ))
10. k : S
⊢ k ≤ imax(F (λn.m);n)

---

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)))
8.  n  :  \mBbbN{}
9.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  S.  (((\mlambda{}n.m)  =  g)  {}\mRightarrow{}  ((F  (\mlambda{}n.m))  =  (F  g)))
\mvdash{}  \mexists{}B:\mBbbN{}.  \mforall{}n:S.  (n  \mleq{}  B)


By

---

Latex:
(D  0  With  \mkleeneopen{}imax(F  (\mlambda{}n.m);n)\mkleeneclose{}    THEN  Auto  THEN  RenameVar  `k'  (-1))

---

Home Index