---

Step * of Lemma groupoid-square2_wf

No Annotations
∀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
{ TACTIC:(ProveWfLemma
          THEN MemTypeCD
          THEN Auto
          THEN TACTIC:(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:
No  Annotations
\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:
TACTIC:(ProveWfLemma
                THEN  MemTypeCD
                THEN  Auto
                THEN  TACTIC:(Unfold  `cat-square-commutes`  0
                                          THEN  ...\mcdot{}
                                          THEN  Auto))

---

Home Index