---

Step * 3 1 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. x1 : names(I)
11. x1 ∈ as
12. x = dM-to-FL(J;¬(g x1)) ∈ Point(face_lattice(J))
⊢ x = 1 ∈ Point(face_lattice(J))
BY
{ (RWO "-6" (-1) THEN 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;¬(0)) ∈ 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.  x1  :  names(I)
11.  x1  \mmember{}  as
12.  x  =  dM-to-FL(J;\mneg{}(g  x1))
\mvdash{}  x  =  1


By

---

Latex:
(RWO  "-6"  (-1)  THEN  Auto)

---

Home Index