---

Step * of Lemma cat-inverse-unique

∀[C:SmallCategory]. ∀[x,y:cat-ob(C)]. ∀[f:cat-arrow(C) x y]. ∀[g2,g1:cat-arrow(C) y x].
  (g1 = g2 ∈ (cat-arrow(C) y x)) supposing ((∃h:cat-arrow(C) y x. hf=1) and fg2=1 and fg1=1)
BY
{ ((Intros THEN ExRepD)
   THEN (FLemma `left-right-inverse-unique` [-1; -4] THENA Auto)
   THEN (FLemma `left-right-inverse-unique` [-2; -4] THENA Auto)) }

1
1. C : SmallCategory
2. x : cat-ob(C)
3. y : cat-ob(C)
4. f : cat-arrow(C) x y
5. g2 : cat-arrow(C) y x
6. g1 : cat-arrow(C) y x
7. fg1=1
8. fg2=1
9. h : cat-arrow(C) y x
10. hf=1
11. g1 = h ∈ (cat-arrow(C) y x)
12. g2 = h ∈ (cat-arrow(C) y x)
⊢ g1 = g2 ∈ (cat-arrow(C) y x)

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[x,y:cat-ob(C)].  \mforall{}[f:cat-arrow(C)  x  y].  \mforall{}[g2,g1:cat-arrow(C)  y  x].
    (g1  =  g2)  supposing  ((\mexists{}h:cat-arrow(C)  y  x.  hf=1)  and  fg2=1  and  fg1=1)


By

---

Latex:
((Intros  THEN  ExRepD)
  THEN  (FLemma  `left-right-inverse-unique`  [-1;  -4]  THENA  Auto)
  THEN  (FLemma  `left-right-inverse-unique`  [-2;  -4]  THENA  Auto))

---

Home Index