Step * 3 1 of Lemma nc-se'-p


1. fset(ℕ)
2. : ℕ
3. : ℕ
4. {n:ℕ| ¬n ∈ J} 
5. names(J+z)
6. x ≠ z
7. x ∈ names(J)
8. n ∈ ℤ
⊢ <k> = <x> ∈ Point(dM(J+k))
BY
(MemTypeHD (-2) THENA Auto) }

1
1. fset(ℕ)
2. : ℕ
3. : ℕ
4. {n:ℕ| ¬n ∈ J} 
5. names(J+z)
6. x ≠ z
7. x ∈ ℕ
8. x ∈ J
9. n ∈ ℤ
⊢ <k> = <x> ∈ Point(dM(J+k))


Latex:


Latex:

1.  J  :  fset(\mBbbN{})
2.  k  :  \mBbbN{}
3.  z  :  \mBbbN{}
4.  n  :  \{n:\mBbbN{}|  \mneg{}n  \mmember{}  J\} 
5.  x  :  names(J+z)
6.  x  \mneq{}  z
7.  x  \mmember{}  names(J)
8.  x  =  n
\mvdash{}  <k>  =  <x>


By


Latex:
(MemTypeHD  (-2)  THENA  Auto)




Home Index