---

Step * 1 1 of Lemma not-assert-bdd-all


1. n : ℕ
2. P : ℕn ⟶ 𝔹
3. ¬(∃i:ℕn. (¬↑P[i]))
4. i : ℕn
5. ¬↑P[i]
⊢ ↑P[i]
BY
{ (D -3 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  P  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbB{}
3.  \mneg{}(\mexists{}i:\mBbbN{}n.  (\mneg{}\muparrow{}P[i]))
4.  i  :  \mBbbN{}n
5.  \mneg{}\muparrow{}P[i]
\mvdash{}  \muparrow{}P[i]


By

---

Latex:
(D  -3  THEN  Auto)

---

Home Index