---

Step * 1 of Lemma irr-face-morph-satisfies


1. I : fset(ℕ)
2. as : fset(names(I))
3. bs : fset(names(I))
4. ↑fset-disjoint(NamesDeq;as;bs)
5. ∀a:names(I). (a ∈ as ⇒ ((irr-face-morph(I;as;bs) a) = 0 ∈ Point(dM(I))))
6. b : names(I)
7. b ∈ bs
8. b ∈ as
⊢ 0 = 1 ∈ Point(dM(I))
BY
{ ((RWO "assert-fset-disjoint" 4 THENA Auto) THEN (InstHyp [⌜b⌝] 4⋅ THENA Auto) THEN D -1 THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  as  :  fset(names(I))
3.  bs  :  fset(names(I))
4.  \muparrow{}fset-disjoint(NamesDeq;as;bs)
5.  \mforall{}a:names(I).  (a  \mmember{}  as  {}\mRightarrow{}  ((irr-face-morph(I;as;bs)  a)  =  0))
6.  b  :  names(I)
7.  b  \mmember{}  bs
8.  b  \mmember{}  as
\mvdash{}  0  =  1


By

---

Latex:
((RWO  "assert-fset-disjoint"  4  THENA  Auto)  THEN  (InstHyp  [\mkleeneopen{}b\mkleeneclose{}]  4\mcdot{}  THENA  Auto)  THEN  D  -1  THEN  Auto)

---

Home Index