---

Step * of Lemma face-forall-implies

No Annotations
∀[H:j⊢]. ∀[phi:{H.𝕀 ⊢ _:𝔽}].  H.𝕀 ⊢ (((∀ phi))p ⇒ phi)
BY
{ (Intros
   THEN (Assert p ∈ H.𝕀 j⟶ H BY
               Auto)
   THEN D 0
   THEN Auto
   THEN RepUR ``cube-context-adjoin`` -2
   THEN D -2
   THEN (RWO "interval-type-at" (-2) THENA Auto)
   THEN RepUR ``interval-presheaf`` -2
   THEN RenameVar `x' (-2)
   THEN (InstLemma `nc-p_wf` [⌜I⌝;⌜new-name(I)⌝;⌜x⌝]⋅ THENA Auto)
   THEN (Assert <new-name(I)> ∈ 𝕀(s(alpha)) BY
               ((RWO "interval-type-at" 0 THENA Auto) THEN RepUR ``interval-presheaf`` 0 THEN Auto))) }

1
1. H : CubicalSet{j}
2. phi : {H.𝕀 ⊢ _:𝔽}
3. p ∈ H.𝕀 j⟶ H
4. I : fset(ℕ)
5. alpha : H(I)
6. x : Point(dM(I))
7. ((∀ phi))p(<alpha, x>) = 1 ∈ Point(face_lattice(I))
8. (new-name(I)/x) ∈ I ⟶ I+new-name(I)
9. <new-name(I)> ∈ 𝕀(s(alpha))
⊢ phi(<alpha, x>) = 1 ∈ Point(face_lattice(I))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H:j\mvdash{}].  \mforall{}[phi:\{H.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}].    H.\mBbbI{}  \mvdash{}  (((\mforall{}  phi))p  {}\mRightarrow{}  phi)


By

---

Latex:
(Intros
  THEN  (Assert  p  \mmember{}  H.\mBbbI{}  j{}\mrightarrow{}  H  BY
                          Auto)
  THEN  D  0
  THEN  Auto
  THEN  RepUR  ``cube-context-adjoin``  -2
  THEN  D  -2
  THEN  (RWO  "interval-type-at"  (-2)  THENA  Auto)
  THEN  RepUR  ``interval-presheaf``  -2
  THEN  RenameVar  `x'  (-2)
  THEN  (InstLemma  `nc-p\_wf`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}new-name(I)\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  <new-name(I)>  \mmember{}  \mBbbI{}(s(alpha))  BY
                          ((RWO  "interval-type-at"  0  THENA  Auto)  THEN  RepUR  ``interval-presheaf``  0  THEN  Auto)))

---

Home Index