---

Step * of Lemma groupoid-square1_wf

No Annotations
∀[G:Groupoid]. ∀[x00,x10,x01,x11:cat-ob(cat(G))]. ∀[a:cat-arrow(cat(G)) x00 x10]. ∀[b:cat-arrow(cat(G)) x10 x11].
∀[c:cat-arrow(cat(G)) x00 x01].
  (groupoid-square1(G;x00;x10;x01;x11;a;b;c) ∈ {d:cat-arrow(cat(G)) x01 x11| a o b = c o d} )
BY
{ TACTIC:(ProveWfLemma THEN MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. G : Groupoid
2. x00 : cat-ob(cat(G))
3. x10 : cat-ob(cat(G))
4. x01 : cat-ob(cat(G))
5. x11 : cat-ob(cat(G))
6. a : cat-arrow(cat(G)) x00 x10
7. b : cat-arrow(cat(G)) x10 x11
8. c : cat-arrow(cat(G)) x00 x01
⊢ a o b = c o cat-comp(cat(G)) x01 x10 x11 (cat-comp(cat(G)) x01 x00 x10 groupoid-inv(G;x00;x01;c) a) b

---

Latex:

---

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


By

---

Latex:
TACTIC:(ProveWfLemma  THEN  MemTypeCD  THEN  Auto)

---

Home Index