---

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


By

---

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

---

Home Index