---

Step * 1 of Lemma not-all-finite


1. [T] : Type
2. [P] : T ⟶ ℙ
3. ∀x:T. Dec(P[x])
4. k : ℕ
5. T ~ ℕk
6. ¬(∀x:T. P[x])
⊢ ∃x:T. (¬P[x])
BY
{ (RepeatFor 2 (D -2)
   THEN Unfold `surject` -2
   THEN (Skolemize (-2) `g' THENA Auto)
   THEN Assert ⌜Dec(∀x:ℕk. P[g x])⌝⋅
   THEN Auto
   THEN D -1
   THEN Try ((RWO "not-all-int_seg" (-1) 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. ¬(∀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])

2
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])

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}x:T.  Dec(P[x])
4.  k  :  \mBbbN{}
5.  T  \msim{}  \mBbbN{}k
6.  \mneg{}(\mforall{}x:T.  P[x])
\mvdash{}  \mexists{}x:T.  (\mneg{}P[x])


By

---

Latex:
(RepeatFor  2  (D  -2)
  THEN  Unfold  `surject`  -2
  THEN  (Skolemize  (-2)  `g'  THENA  Auto)
  THEN  Assert  \mkleeneopen{}Dec(\mforall{}x:\mBbbN{}k.  P[g  x])\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  D  -1
  THEN  Try  ((RWO  "not-all-int\_seg"  (-1)  THEN  Auto)))

---

Home Index