---

Step * 1 of Lemma implies-face-forall-holds


1. H : CubicalSet{j}
2. phi : {H.𝕀 ⊢ _:𝔽}
3. H.𝕀 ⊢ (1(𝔽) ⇒ phi)
4. I : fset(ℕ)
5. rho : H(I)
6. 1(𝔽)(rho) = 1 ∈ Point(face_lattice(I))
⊢ (∀new-name(I).phi((s(rho);<new-name(I)>))) = 1 ∈ Point(face_lattice(I))
BY
{ ((D 3 With ⌜I+new-name(I)⌝  THENA Auto) THEN (D -1 With ⌜(s(rho);<new-name(I)>)⌝  THENA Auto)) }

1
1. H : CubicalSet{j}
2. phi : {H.𝕀 ⊢ _:𝔽}
3. I : fset(ℕ)
4. rho : H(I)
5. 1(𝔽)(rho) = 1 ∈ Point(face_lattice(I))
⊢ <new-name(I)> ∈ 𝕀(s(rho))

2
1. H : CubicalSet{j}
2. phi : {H.𝕀 ⊢ _:𝔽}
3. I : fset(ℕ)
4. rho : H(I)
5. 1(𝔽)(rho) = 1 ∈ Point(face_lattice(I))
6. (1(𝔽)((s(rho);<new-name(I)>)) = 1 ∈ Point(face_lattice(I+new-name(I))))
⇒ (phi((s(rho);<new-name(I)>)) = 1 ∈ Point(face_lattice(I+new-name(I))))
⊢ (∀new-name(I).phi((s(rho);<new-name(I)>))) = 1 ∈ Point(face_lattice(I))

---

Latex:

---

Latex:

1.  H  :  CubicalSet\{j\}
2.  phi  :  \{H.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}
3.  H.\mBbbI{}  \mvdash{}  (1(\mBbbF{})  {}\mRightarrow{}  phi)
4.  I  :  fset(\mBbbN{})
5.  rho  :  H(I)
6.  1(\mBbbF{})(rho)  =  1
\mvdash{}  (\mforall{}new-name(I).phi((s(rho);<new-name(I)>)))  =  1


By

---

Latex:
((D  3  With  \mkleeneopen{}I+new-name(I)\mkleeneclose{}    THENA  Auto)  THEN  (D  -1  With  \mkleeneopen{}(s(rho);<new-name(I)>)\mkleeneclose{}    THENA  Auto))

---

Home Index