---

Step * of Lemma groupoid-square2_wf

∀G:Groupoid. ∀x00,x10,x01,x11:cat-ob(cat(G)). ∀d:cat-arrow(cat(G)) x01 x11. ∀b:cat-arrow(cat(G)) x10 x11.
∀c:cat-arrow(cat(G)) x00 x01.
  (groupoid-square2(G;x00;x10;x01;x11;b;c;d) ∈ {a:cat-arrow(cat(G)) x00 x10| a o b = c o d} )
BY
{ (ProveWfLemma
   THEN MemTypeCD
   THEN Auto
   THEN (Unfold `cat-square-commutes` 0
         THEN RWW "cat-comp-assoc groupoid-left-cancellation groupoid_inv.2 cat-comp-ident.2" 0⋅
         THEN Auto)) }

---

Latex:

---

Latex:
\mforall{}G:Groupoid.  \mforall{}x00,x10,x01,x11:cat-ob(cat(G)).  \mforall{}d:cat-arrow(cat(G))  x01  x11.
\mforall{}b:cat-arrow(cat(G))  x10  x11.  \mforall{}c:cat-arrow(cat(G))  x00  x01.
    (groupoid-square2(G;x00;x10;x01;x11;b;c;d)  \mmember{}  \{a:cat-arrow(cat(G))  x00  x10|  a  o  b  =  c  o  d\}  )


By

---

Latex:
(ProveWfLemma
  THEN  MemTypeCD
  THEN  Auto
  THEN  (Unfold  `cat-square-commutes`  0
              THEN  RWW  "cat-comp-assoc  groupoid-left-cancellation  groupoid\_inv.2  cat-comp-ident.2"  0\mcdot{}
              THEN  Auto))

---

Home Index