---

Step * 1 1 2 1 1 of Lemma face-forall-decomp


1. H : CubicalSet{j}
2. phi : {H.𝕀 ⊢ _:𝔽}
3. H.𝕀 ⊢ (((∀ phi))p ⇒ phi)
4. p ∈ H.𝕀 j⟶ H
5. I : fset(ℕ)
6. alpha : H(I)
7. x : Point(dM(I))
8. phi(<alpha, x>) = 1 ∈ Point(face_lattice(I))
9. (new-name(I)/x) ∈ I ⟶ I+new-name(I)
10. <new-name(I)> ∈ 𝕀(s(alpha))
11. (phi((s(alpha);<new-name(I)>)))<(new-name(I)/x)> = phi((alpha;x)) ∈ Point(face_lattice(I))
12. (phi((s(alpha);<new-name(I)>)))<(new-name(I)/x)> = 1 ∈ Point(face_lattice(I))
⊢ (((∀ phi))p ∨ ((phi ∧ (q=0)) ∨ (phi ∧ (q=1))))(<alpha, x>) = 1 ∈ Point(face_lattice(I))
BY
{ (RWW "face-or-at face-and-at" 0 THENA Auto) }

1
1. H : CubicalSet{j}
2. phi : {H.𝕀 ⊢ _:𝔽}
3. H.𝕀 ⊢ (((∀ phi))p ⇒ phi)
4. p ∈ H.𝕀 j⟶ H
5. I : fset(ℕ)
6. alpha : H(I)
7. x : Point(dM(I))
8. phi(<alpha, x>) = 1 ∈ Point(face_lattice(I))
9. (new-name(I)/x) ∈ I ⟶ I+new-name(I)
10. <new-name(I)> ∈ 𝕀(s(alpha))
11. (phi((s(alpha);<new-name(I)>)))<(new-name(I)/x)> = phi((alpha;x)) ∈ Point(face_lattice(I))
12. (phi((s(alpha);<new-name(I)>)))<(new-name(I)/x)> = 1 ∈ Point(face_lattice(I))
⊢ ((∀ phi))p(<alpha, x>) ∨ phi(<alpha, x>) ∧ (q=0)(<alpha, x>) ∨ phi(<alpha, x>) ∧ (q=1)(<alpha, x>) = 1 ∈ Point(face_la\000Cttice(I))

---

Latex:

---

Latex:

1.  H  :  CubicalSet\{j\}
2.  phi  :  \{H.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}
3.  H.\mBbbI{}  \mvdash{}  (((\mforall{}  phi))p  {}\mRightarrow{}  phi)
4.  p  \mmember{}  H.\mBbbI{}  j{}\mrightarrow{}  H
5.  I  :  fset(\mBbbN{})
6.  alpha  :  H(I)
7.  x  :  Point(dM(I))
8.  phi(<alpha,  x>)  =  1
9.  (new-name(I)/x)  \mmember{}  I  {}\mrightarrow{}  I+new-name(I)
10.  <new-name(I)>  \mmember{}  \mBbbI{}(s(alpha))
11.  (phi((s(alpha);<new-name(I)>)))<(new-name(I)/x)>  =  phi((alpha;x))
12.  (phi((s(alpha);<new-name(I)>)))<(new-name(I)/x)>  =  1
\mvdash{}  (((\mforall{}  phi))p  \mvee{}  ((phi  \mwedge{}  (q=0))  \mvee{}  (phi  \mwedge{}  (q=1))))(<alpha,  x>)  =  1


By

---

Latex:
(RWW  "face-or-at  face-and-at"  0  THENA  Auto)

---

Home Index