---

Step * 1 1 1 2 1 of Lemma comp_nat_ind_tp

.....wf..... 
1. P : ℕ ⟶ ℙ{k}
2. ∀i:ℕ. ((∀j:ℕ. P[j] supposing j < i) ⇒ P[i])
3. i : ℕ
⊢ i + 1 ∈ ℕ
BY
{ ArithMemberReflEqTypeCD }

1
1. P : ℕ ⟶ ℙ{k}
2. ∀i:ℕ. ((∀j:ℕ. P[j] supposing j < i) ⇒ P[i])
3. i : ℕ
⊢ i + 1 ∈ ℤ

2
.....set predicate..... 
1. P : ℕ ⟶ ℙ{k}
2. ∀i:ℕ. ((∀j:ℕ. P[j] supposing j < i) ⇒ P[i])
3. i : ℕ
⊢ 0 ≤ (i + 1)

3
.....wf..... 
1. P : ℕ ⟶ ℙ{k}
2. ∀i:ℕ. ((∀j:ℕ. P[j] supposing j < i) ⇒ P[i])
3. i : ℕ
4. i1 : ℤ
⊢ istype(0 ≤ i1)

---

Latex:

---

Latex:
.....wf..... 
1.  P  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}\{k\}
2.  \mforall{}i:\mBbbN{}.  ((\mforall{}j:\mBbbN{}.  P[j]  supposing  j  <  i)  {}\mRightarrow{}  P[i])
3.  i  :  \mBbbN{}
\mvdash{}  i  +  1  \mmember{}  \mBbbN{}


By

---

Latex:
ArithMemberReflEqTypeCD

---

Home Index