Metamath Proof Explorer


Theorem dfinito2

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

Ref Expression
Assertion dfinito2 InitO = c Cat TermO oppCat c

Proof

Step Hyp Ref Expression
1 df-inito InitO = c Cat a Base c | b Base c ∃! h h a Hom c b
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 termoval c Cat TermO oppCat c = a Base c | b Base c ∃! h h b Hom oppCat c a
8 eqid Hom c = Hom c
9 8 2 oppchom b Hom oppCat c a = a Hom c b
10 9 eleq2i h b Hom oppCat c a h a Hom c b
11 10 eubii ∃! h h b Hom oppCat c a ∃! h h a Hom c b
12 11 ralbii b Base c ∃! h h b Hom oppCat c a b Base c ∃! h h a Hom c b
13 12 rabbii a Base c | b Base c ∃! h h b Hom oppCat c a = a Base c | b Base c ∃! h h a Hom c b
14 7 13 eqtrdi c Cat TermO oppCat c = a Base c | b Base c ∃! h h a Hom c b
15 14 mpteq2ia c Cat TermO oppCat c = c Cat a Base c | b Base c ∃! h h a Hom c b
16 1 15 eqtr4i InitO = c Cat TermO oppCat c