---

Step * 3 of Lemma satisfies-irr-face


1. I : fset(ℕ)
2. J : fset(ℕ)
3. as : fset(names(I))
4. bs : fset(names(I))
5. g : J ⟶ I
6. ∀[s:fset(Point(face_lattice(J)))]
     uiff(/\(s) = 1 ∈ Point(face_lattice(J));∀x:Point(face_lattice(J)). (x ∈ s ⇒ (x = 1 ∈ Point(face_lattice(J)))))
7. ∀a:names(I). (a ∈ as ⇒ ((g a) = 0 ∈ Point(dM(J))))
8. ∀b:names(I). (b ∈ bs ⇒ ((g b) = 1 ∈ Point(dM(J))))
9. x : Point(face_lattice(J))
10. x ∈ <g>"(λa.(a=0)"(as))
⊢ x = 1 ∈ Point(face_lattice(J))
BY
{ ((RWO  "fset-image-compose" (-1) THENA Auto)
   THEN (RWO  "member-fset-image-iff" (-1) THENA Auto)
   THEN RepUR ``compose`` -1
   THEN SqExRepD
   THEN (RWW "fl-morph-fl0 fl-morph-fl1" (-1) THENA Auto)) }

1
1. I : fset(ℕ)
2. J : fset(ℕ)
3. as : fset(names(I))
4. bs : fset(names(I))
5. g : J ⟶ I
6. ∀[s:fset(Point(face_lattice(J)))]
     uiff(/\(s) = 1 ∈ Point(face_lattice(J));∀x:Point(face_lattice(J)). (x ∈ s ⇒ (x = 1 ∈ Point(face_lattice(J)))))
7. ∀a:names(I). (a ∈ as ⇒ ((g a) = 0 ∈ Point(dM(J))))
8. ∀b:names(I). (b ∈ bs ⇒ ((g b) = 1 ∈ Point(dM(J))))
9. x : Point(face_lattice(J))
10. x1 : names(I)
11. x1 ∈ as
12. x = dM-to-FL(J;¬(g x1)) ∈ Point(face_lattice(J))
⊢ x = 1 ∈ Point(face_lattice(J))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  J  :  fset(\mBbbN{})
3.  as  :  fset(names(I))
4.  bs  :  fset(names(I))
5.  g  :  J  {}\mrightarrow{}  I
6.  \mforall{}[s:fset(Point(face\_lattice(J)))].  uiff(/\mbackslash{}(s)  =  1;\mforall{}x:Point(face\_lattice(J)).  (x  \mmember{}  s  {}\mRightarrow{}  (x  =  1)))
7.  \mforall{}a:names(I).  (a  \mmember{}  as  {}\mRightarrow{}  ((g  a)  =  0))
8.  \mforall{}b:names(I).  (b  \mmember{}  bs  {}\mRightarrow{}  ((g  b)  =  1))
9.  x  :  Point(face\_lattice(J))
10.  x  \mmember{}  <g>"(\mlambda{}a.(a=0)"(as))
\mvdash{}  x  =  1


By

---

Latex:
((RWO    "fset-image-compose"  (-1)  THENA  Auto)
  THEN  (RWO    "member-fset-image-iff"  (-1)  THENA  Auto)
  THEN  RepUR  ``compose``  -1
  THEN  SqExRepD
  THEN  (RWW  "fl-morph-fl0  fl-morph-fl1"  (-1)  THENA  Auto))

---

Home Index