---

Step * of Lemma cat-final-isomorphic

∀[C:SmallCategory]. ∀fnl1,fnl2:cat-ob(C).  (Final(fnl1) ⇒ Final(fnl2) ⇒ cat-isomorphic(C;fnl1;fnl2))
BY
{ (Auto
   THEN DupHyp (-1)
   THEN (D -1 With ⌜fnl1⌝  THENA Auto)
   THEN D -1
   THEN RenameVar `f' (-1)
   THEN D 0 With ⌜f⌝ 
   THEN Auto) }

1
1. [C] : SmallCategory
2. fnl1 : cat-ob(C)
3. fnl2 : cat-ob(C)
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)

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory]
    \mforall{}fnl1,fnl2:cat-ob(C).    (Final(fnl1)  {}\mRightarrow{}  Final(fnl2)  {}\mRightarrow{}  cat-isomorphic(C;fnl1;fnl2))


By

---

Latex:
(Auto
  THEN  DupHyp  (-1)
  THEN  (D  -1  With  \mkleeneopen{}fnl1\mkleeneclose{}    THENA  Auto)
  THEN  D  -1
  THEN  RenameVar  `f'  (-1)
  THEN  D  0  With  \mkleeneopen{}f\mkleeneclose{} 
  THEN  Auto)

---

Home Index