---

Step * 1 of Lemma cat-final-isomorphic


1. [C] : SmallCategory
2. fnl1 : cat-ob(C)@i
3. fnl2 : cat-ob(C)@i
4. Final(fnl1)
5. Final(fnl2)
6. ∀[f,g:cat-arrow(C) fnl1 fnl2].  (f = g ∈ (cat-arrow(C) fnl1 fnl2))
7. f : cat-arrow(C) fnl1 fnl2
⊢ cat-isomorphism(C;fnl1;fnl2;f)
BY
{ (DupHyp (-4)
   THEN (D -1 With ⌜fnl2⌝  THENA Auto)
   THEN D -1
   THEN RenameVar `g' (-1)
   THEN D 0 With ⌜g⌝ 
   THEN Auto
   THEN UnfoldTopAb 0) }

1
1. C : SmallCategory
2. fnl1 : cat-ob(C)@i
3. fnl2 : cat-ob(C)@i
4. Final(fnl1)
5. Final(fnl2)
6. ∀[f,g:cat-arrow(C) fnl1 fnl2].  (f = g ∈ (cat-arrow(C) fnl1 fnl2))
7. f : cat-arrow(C) fnl1 fnl2
8. ∀[f,g:cat-arrow(C) fnl2 fnl1].  (f = g ∈ (cat-arrow(C) fnl2 fnl1))
9. g : cat-arrow(C) fnl2 fnl1
⊢ (cat-comp(C) fnl1 fnl2 fnl1 f g) = (cat-id(C) fnl1) ∈ (cat-arrow(C) fnl1 fnl1)

2
1. C : SmallCategory
2. fnl1 : cat-ob(C)@i
3. fnl2 : cat-ob(C)@i
4. Final(fnl1)
5. Final(fnl2)
6. ∀[f,g:cat-arrow(C) fnl1 fnl2].  (f = g ∈ (cat-arrow(C) fnl1 fnl2))
7. f : cat-arrow(C) fnl1 fnl2
8. ∀[f,g:cat-arrow(C) fnl2 fnl1].  (f = g ∈ (cat-arrow(C) fnl2 fnl1))
9. g : cat-arrow(C) fnl2 fnl1
10. fg=1
⊢ (cat-comp(C) fnl2 fnl1 fnl2 g f) = (cat-id(C) fnl2) ∈ (cat-arrow(C) fnl2 fnl2)

---

Latex:

---

Latex:

1.  [C]  :  SmallCategory
2.  fnl1  :  cat-ob(C)@i
3.  fnl2  :  cat-ob(C)@i
4.  Final(fnl1)
5.  Final(fnl2)
6.  \mforall{}[f,g:cat-arrow(C)  fnl1  fnl2].    (f  =  g)
7.  f  :  cat-arrow(C)  fnl1  fnl2
\mvdash{}  cat-isomorphism(C;fnl1;fnl2;f)


By

---

Latex:
(DupHyp  (-4)
  THEN  (D  -1  With  \mkleeneopen{}fnl2\mkleeneclose{}    THENA  Auto)
  THEN  D  -1
  THEN  RenameVar  `g'  (-1)
  THEN  D  0  With  \mkleeneopen{}g\mkleeneclose{} 
  THEN  Auto
  THEN  UnfoldTopAb  0)

---

Home Index