---

Step * 1 1 of Lemma not-all-finite


1. [T] : Type
2. [P] : T ⟶ ℙ
3. ∀x:T. Dec(P[x])
4. k : ℕ
5. f : T ⟶ ℕk
6. Inj(T;ℕk;f)
7. ∀b:ℕk. ∃a:T. ((f a) = b ∈ ℕk)
8. ¬(∀x:T. P[x])
9. g : b:ℕk ⟶ T
10. ∀b:ℕk. ((f (g b)) = b ∈ ℕk)
11. ∀x:ℕk. P[g x]
⊢ ∃x:T. (¬P[x])
BY
{ (D -4 THEN Auto) }

1
1. [T] : Type
2. [P] : T ⟶ ℙ
3. ∀x:T. Dec(P[x])
4. k : ℕ
5. f : T ⟶ ℕk
6. Inj(T;ℕk;f)
7. ∀b:ℕk. ∃a:T. ((f a) = b ∈ ℕk)
8. g : b:ℕk ⟶ T
9. ∀b:ℕk. ((f (g b)) = b ∈ ℕk)
10. ∀x:ℕk. P[g x]
11. x : T
⊢ P[x]

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}x:T.  Dec(P[x])
4.  k  :  \mBbbN{}
5.  f  :  T  {}\mrightarrow{}  \mBbbN{}k
6.  Inj(T;\mBbbN{}k;f)
7.  \mforall{}b:\mBbbN{}k.  \mexists{}a:T.  ((f  a)  =  b)
8.  \mneg{}(\mforall{}x:T.  P[x])
9.  g  :  b:\mBbbN{}k  {}\mrightarrow{}  T
10.  \mforall{}b:\mBbbN{}k.  ((f  (g  b))  =  b)
11.  \mforall{}x:\mBbbN{}k.  P[g  x]
\mvdash{}  \mexists{}x:T.  (\mneg{}P[x])


By

---

Latex:
(D  -4  THEN  Auto)

---

Home Index