---

Step * 1 1 of Lemma assert-isdM0


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)} 
BY
{ (RWO "dM0-sq-empty" 0 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)
⊢ {} = 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  :  \{ac:fset(fset(names(I)  +  names(I)))| 
                \muparrow{}fset-antichain(union-deq(names(I);names(I);NamesDeq;NamesDeq);ac)\} 
3.  \muparrow{}isdM0(x)
\mvdash{}  0  =  x


By

---

Latex:
(RWO  "dM0-sq-empty"  0  THENA  Auto)

---

Home Index