Metamath Proof Explorer


Theorem termoid

Description: For a terminal object, the identity arrow is the one and only morphism of the object to the object itself. (Contributed by AV, 18-Apr-2020)

Ref Expression
Hypotheses isinitoi.b B=BaseC
isinitoi.h H=HomC
isinitoi.c φCCat
Assertion termoid φOTermOCOHO=IdCO

Proof

Step Hyp Ref Expression
1 isinitoi.b B=BaseC
2 isinitoi.h H=HomC
3 isinitoi.c φCCat
4 1 2 3 istermoi φOTermOCOBoB∃!hhoHO
5 oveq1 o=OoHO=OHO
6 5 eleq2d o=OhoHOhOHO
7 6 eubidv o=O∃!hhoHO∃!hhOHO
8 7 rspcv OBoB∃!hhoHO∃!hhOHO
9 8 adantl φOTermOCOBoB∃!hhoHO∃!hhOHO
10 eusn ∃!hhOHOhOHO=h
11 eqid IdC=IdC
12 3 ad2antrr φOTermOCOBCCat
13 simpr φOTermOCOBOB
14 1 2 11 12 13 catidcl φOTermOCOBIdCOOHO
15 fvex IdCOV
16 15 elsn IdCOhIdCO=h
17 eqcom IdCO=hh=IdCO
18 sneqbg hVh=IdCOh=IdCO
19 18 bicomd hVh=IdCOh=IdCO
20 19 elv h=IdCOh=IdCO
21 16 17 20 3bitri IdCOhh=IdCO
22 21 biimpi IdCOhh=IdCO
23 22 a1i OHO=hIdCOhh=IdCO
24 eleq2 OHO=hIdCOOHOIdCOh
25 eqeq1 OHO=hOHO=IdCOh=IdCO
26 23 24 25 3imtr4d OHO=hIdCOOHOOHO=IdCO
27 14 26 syl5 OHO=hφOTermOCOBOHO=IdCO
28 27 exlimiv hOHO=hφOTermOCOBOHO=IdCO
29 28 com12 φOTermOCOBhOHO=hOHO=IdCO
30 10 29 syl5bi φOTermOCOB∃!hhOHOOHO=IdCO
31 9 30 syld φOTermOCOBoB∃!hhoHOOHO=IdCO
32 31 expimpd φOTermOCOBoB∃!hhoHOOHO=IdCO
33 4 32 mpd φOTermOCOHO=IdCO