---

Step * 1 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. ∀x:Point(face_lattice(J))
     ((↓∃x1:names(I). (x1 ∈ as ∧ (x = dM-to-FL(J;¬(g x1)) ∈ Point(face_lattice(J)))))
     ⇒ (x = 1 ∈ Point(face_lattice(J))))
8. a : names(I)
9. a ∈ as
⊢ (g a) = 0 ∈ Point(dM(J))
BY
{ (InstHyp [⌜dM-to-FL(J;¬(g a))⌝] (-3)⋅ 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. ∀x:Point(face_lattice(J))
     ((↓∃x1:names(I). (x1 ∈ as ∧ (x = dM-to-FL(J;¬(g x1)) ∈ Point(face_lattice(J)))))
     ⇒ (x = 1 ∈ Point(face_lattice(J))))
8. a : names(I)
9. a ∈ as
10. dM-to-FL(J;¬(g a)) = 1 ∈ Point(face_lattice(J))
⊢ (g a) = 0 ∈ Point(dM(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{}x:Point(face\_lattice(J)).  ((\mdownarrow{}\mexists{}x1:names(I).  (x1  \mmember{}  as  \mwedge{}  (x  =  dM-to-FL(J;\mneg{}(g  x1)))))  {}\mRightarrow{}  (x  =  1))
8.  a  :  names(I)
9.  a  \mmember{}  as
\mvdash{}  (g  a)  =  0


By

---

Latex:
(InstHyp  [\mkleeneopen{}dM-to-FL(J;\mneg{}(g  a))\mkleeneclose{}]  (-3)\mcdot{}  THEN  Auto)

---

Home Index