---

Step * of Lemma cat-square-commutes_wf

No Annotations
∀[C:SmallCategory]. ∀[x,y1,y2,z:cat-ob(C)]. ∀[x_y1:cat-arrow(C) x y1]. ∀[y1_z:cat-arrow(C) y1 z]. ∀[x_y2:cat-arrow(C) x 
                                                                                                         y2].
∀[y2_z:cat-arrow(C) y2 z].
  (x_y1 o y1_z = x_y2 o y2_z ∈ ℙ)
BY
{ TACTIC:ProveWfLemma }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[x,y1,y2,z:cat-ob(C)].  \mforall{}[x$_{y1}$:cat-arrow(C)  x  y1].  \mforall{}[y1\mbackslash{}\000Cff24_{z}$:cat-arrow(C)  y1  z].
\mforall{}[x$_{y2}$:cat-arrow(C)  x  y2].  \mforall{}[y2$_{z}$:cat-arrow(C)  y2  z]\000C.
    (x$_{y1}$  o  y1$_{z}$  =  x$_{y2}$  o  y2\mbackslash{}f\000Cf24_{z}$  \mmember{}  \mBbbP{})


By

---

Latex:
TACTIC:ProveWfLemma

---

Home Index