Step * 1 1 1 1 1 2 of Lemma finite-partition-property


1. : ℕ
2. : ℕ ⟶ ℕk
3. ∀i:ℕk. (∀n:ℕ(¬¬(∃m:ℕ(n < m ∧ ((f m) i ∈ ℤ))))))
4. ∀i:ℕk. (¬¬(∃n:ℕ(∃m:ℕ(n < m ∧ ((f m) i ∈ ℤ))))))
5. ∀[B:ℕ ⟶ ℙ]. ∀n:ℕ((∀i:ℕn. (¬¬(B i)))  (¬¬(∀i:ℕn. (B i))))
6. ∀i:ℕk. ∃n:ℕ(∃m:ℕ(n < m ∧ ((f m) i ∈ ℤ))))
7. ∃n:ℕ. ∀i:ℕk. (∃m:ℕ(n < m ∧ ((f m) i ∈ ℤ))))
⊢ False
BY
(-1) }

1
1. : ℕ
2. : ℕ ⟶ ℕk
3. ∀i:ℕk. (∀n:ℕ(¬¬(∃m:ℕ(n < m ∧ ((f m) i ∈ ℤ))))))
4. ∀i:ℕk. (¬¬(∃n:ℕ(∃m:ℕ(n < m ∧ ((f m) i ∈ ℤ))))))
5. ∀[B:ℕ ⟶ ℙ]. ∀n:ℕ((∀i:ℕn. (¬¬(B i)))  (¬¬(∀i:ℕn. (B i))))
6. ∀i:ℕk. ∃n:ℕ(∃m:ℕ(n < m ∧ ((f m) i ∈ ℤ))))
7. : ℕ
8. ∀i:ℕk. (∃m:ℕ(n < m ∧ ((f m) i ∈ ℤ))))
⊢ False


Latex:


Latex:

1.  k  :  \mBbbN{}
2.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}k
3.  \mforall{}i:\mBbbN{}k.  (\mneg{}(\mforall{}n:\mBbbN{}.  (\mneg{}\mneg{}(\mexists{}m:\mBbbN{}.  (n  <  m  \mwedge{}  ((f  m)  =  i))))))
4.  \mforall{}i:\mBbbN{}k.  (\mneg{}\mneg{}(\mexists{}n:\mBbbN{}.  (\mneg{}(\mexists{}m:\mBbbN{}.  (n  <  m  \mwedge{}  ((f  m)  =  i))))))
5.  \mforall{}[B:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  \mforall{}n:\mBbbN{}.  ((\mforall{}i:\mBbbN{}n.  (\mneg{}\mneg{}(B  i)))  {}\mRightarrow{}  (\mneg{}\mneg{}(\mforall{}i:\mBbbN{}n.  (B  i))))
6.  \mforall{}i:\mBbbN{}k.  \mexists{}n:\mBbbN{}.  (\mneg{}(\mexists{}m:\mBbbN{}.  (n  <  m  \mwedge{}  ((f  m)  =  i))))
7.  \mexists{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}k.  (\mneg{}(\mexists{}m:\mBbbN{}.  (n  <  m  \mwedge{}  ((f  m)  =  i))))
\mvdash{}  False


By


Latex:
D  (-1)




Home Index