---

Step * 1 1 of Lemma assert-isdM1


1. I : fset(ℕ)
2. x : Point(dM(I))
3. {x ∈ fset(fset(names(I) + names(I)))}
4. uiff(↑isdM1(x);x = {{}} ∈ fset(fset(names(I) + names(I))))
⊢ uiff(x = {{}} ∈ fset(fset(names(I) + names(I)));x = 1 ∈ Point(dM(I)))
BY
{ ((RWO "dM1-sq-singleton-empty" 0 THENA Auto) THEN (RWO "dM-point" 0 THENA Auto)) }

1
1. I : fset(ℕ)
2. x : Point(dM(I))
3. {x ∈ fset(fset(names(I) + names(I)))}
4. uiff(↑isdM1(x);x = {{}} ∈ fset(fset(names(I) + names(I))))
⊢ uiff(x = {{}} ∈ fset(fset(names(I) + names(I)));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.  \{x  \mmember{}  fset(fset(names(I)  +  names(I)))\}
4.  uiff(\muparrow{}isdM1(x);x  =  \{\{\}\})
\mvdash{}  uiff(x  =  \{\{\}\};x  =  1)


By

---

Latex:
((RWO  "dM1-sq-singleton-empty"  0  THENA  Auto)  THEN  (RWO  "dM-point"  0  THENA  Auto))

---

Home Index