---

Step * 1 1 2 of Lemma not-not-finite-all-or-exists


1. T : Type
2. n : ℕ
3. T ~ ℕn
4. P : T ⟶ ℙ
5. ∀i:T. Dec(P[i])
6. f : ℕn ⟶ T
7. Bij(ℕn;T;f)
8. ∀i:ℕn. Dec(P[f i])
9. ¬(∃i:ℕn. (¬P[f i]))
10. i : T
⊢ P[i]
BY
{ (D 7 THEN (D 8 With ⌜i⌝  THENA Auto) THEN D -1 THEN (RWO "-1<" 0 THENA Auto) THEN SupposeNot) }

1
1. T : Type
2. n : ℕ
3. T ~ ℕn
4. P : T ⟶ ℙ
5. ∀i:T. Dec(P[i])
6. f : ℕn ⟶ T
7. Inj(ℕn;T;f)
8. ∀i:ℕn. Dec(P[f i])
9. ¬(∃i:ℕn. (¬P[f i]))
10. i : T
11. a : ℕn
12. (f a) = i ∈ T
13. ¬P[f a]
⊢ P[f a]

---

Latex:

---

Latex:

1.  T  :  Type
2.  n  :  \mBbbN{}
3.  T  \msim{}  \mBbbN{}n
4.  P  :  T  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}i:T.  Dec(P[i])
6.  f  :  \mBbbN{}n  {}\mrightarrow{}  T
7.  Bij(\mBbbN{}n;T;f)
8.  \mforall{}i:\mBbbN{}n.  Dec(P[f  i])
9.  \mneg{}(\mexists{}i:\mBbbN{}n.  (\mneg{}P[f  i]))
10.  i  :  T
\mvdash{}  P[i]


By

---

Latex:
(D  7  THEN  (D  8  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)  THEN  D  -1  THEN  (RWO  "-1<"  0  THENA  Auto)  THEN  SupposeNot)

---

Home Index