---

Step * 1 2 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
{ ExRepD }

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. ¬(∀x:T. P[x])
9. g : b:ℕk ⟶ T
10. ∀b:ℕk. ((f (g b)) = b ∈ ℕk)
11. x : ℕk
12. ¬P[g x]
⊢ ∃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.  \mexists{}x:\mBbbN{}k.  (\mneg{}P[g  x])
\mvdash{}  \mexists{}x:T.  (\mneg{}P[x])


By

---

Latex:
ExRepD

---

Home Index