---

Step * 1 of Lemma assert-isdM0


1. I : fset(ℕ)
2. x : Point(dM(I))
3. ↑isdM0(x)
⊢ x = 0 ∈ Point(dM(I))
BY
{ (Symmetry THEN (All (RWO "dM-point") THENA Auto)) }

1
1. I : fset(ℕ)
2. x : {ac:fset(fset(names(I) + names(I)))| ↑fset-antichain(union-deq(names(I);names(I);NamesDeq;NamesDeq);ac)} 
3. ↑isdM0(x)
⊢ 0 = x ∈ {ac:fset(fset(names(I) + names(I)))| ↑fset-antichain(union-deq(names(I);names(I);NamesDeq;NamesDeq);ac)} 

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  x  :  Point(dM(I))
3.  \muparrow{}isdM0(x)
\mvdash{}  x  =  0


By

---

Latex:
(Symmetry  THEN  (All  (RWO  "dM-point")  THENA  Auto))

---

Home Index