---

Step * of Lemma equal-nat-inf-infinity

∀[x:ℕ∞]. uiff(x = ∞ ∈ ℕ∞;∀i:ℕ. (¬(x = i∞ ∈ ℕ∞)))
BY
{ Auto }

1
1. x : ℕ∞
2. x = ∞ ∈ ℕ∞
3. i : ℕ
⊢ ¬(x = i∞ ∈ ℕ∞)

2
1. x : ℕ∞
2. ∀i:ℕ. (¬(x = i∞ ∈ ℕ∞))
⊢ x = ∞ ∈ ℕ∞

---

Latex:

---

Latex:
\mforall{}[x:\mBbbN{}\minfty{}].  uiff(x  =  \minfty{};\mforall{}i:\mBbbN{}.  (\mneg{}(x  =  i\minfty{})))


By

---

Latex:
Auto

---

Home Index