Metamath Proof Explorer


Theorem dftermo2

Description: A terminal object is an initial object in the opposite category. An alternate definition of df-termo depending on df-inito . (Contributed by Zhi Wang, 29-Aug-2024)

Ref Expression
Assertion dftermo2 TermO = c Cat InitO oppCat c

Proof

Step Hyp Ref Expression
1 df-termo TermO = c Cat a Base c | b Base c ∃! h h b Hom c a
2 eqid oppCat c = oppCat c
3 2 oppccat c Cat oppCat c Cat
4 eqid Base c = Base c
5 2 4 oppcbas Base c = Base oppCat c
6 eqid Hom oppCat c = Hom oppCat c
7 3 5 6 initoval c Cat InitO oppCat c = a Base c | b Base c ∃! h h a Hom oppCat c b
8 eqid Hom c = Hom c
9 8 2 oppchom a Hom oppCat c b = b Hom c a
10 9 eleq2i h a Hom oppCat c b h b Hom c a
11 10 eubii ∃! h h a Hom oppCat c b ∃! h h b Hom c a
12 11 ralbii b Base c ∃! h h a Hom oppCat c b b Base c ∃! h h b Hom c a
13 12 rabbii a Base c | b Base c ∃! h h a Hom oppCat c b = a Base c | b Base c ∃! h h b Hom c a
14 7 13 eqtrdi c Cat InitO oppCat c = a Base c | b Base c ∃! h h b Hom c a
15 14 mpteq2ia c Cat InitO oppCat c = c Cat a Base c | b Base c ∃! h h b Hom c a
16 1 15 eqtr4i TermO = c Cat InitO oppCat c