Metamath Proof Explorer


Theorem initoid

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

Ref Expression
Hypotheses isinitoi.b B = Base C
isinitoi.h H = Hom C
isinitoi.c φ C Cat
Assertion initoid φ O InitO C O H O = Id C O

Proof

Step Hyp Ref Expression
1 isinitoi.b B = Base C
2 isinitoi.h H = Hom C
3 isinitoi.c φ C Cat
4 1 2 3 isinitoi φ O InitO C O B o B ∃! h h O H o
5 oveq2 o = O O H o = O H O
6 5 eleq2d o = O h O H o h O H O
7 6 eubidv o = O ∃! h h O H o ∃! h h O H O
8 7 rspcv O B o B ∃! h h O H o ∃! h h O H O
9 8 adantl φ O InitO C O B o B ∃! h h O H o ∃! h h O H O
10 eusn ∃! h h O H O h O H O = h
11 eqid Id C = Id C
12 3 ad2antrr φ O InitO C O B C Cat
13 simpr φ O InitO C O B O B
14 1 2 11 12 13 catidcl φ O InitO C O B Id C O O H O
15 fvex Id C O V
16 15 elsn Id C O h Id C O = h
17 eqcom Id C O = h h = Id C O
18 sneqbg h V h = Id C O h = Id C O
19 18 bicomd h V h = Id C O h = Id C O
20 19 elv h = Id C O h = Id C O
21 16 17 20 3bitri Id C O h h = Id C O
22 21 biimpi Id C O h h = Id C O
23 22 a1i O H O = h Id C O h h = Id C O
24 eleq2 O H O = h Id C O O H O Id C O h
25 eqeq1 O H O = h O H O = Id C O h = Id C O
26 23 24 25 3imtr4d O H O = h Id C O O H O O H O = Id C O
27 14 26 syl5 O H O = h φ O InitO C O B O H O = Id C O
28 27 exlimiv h O H O = h φ O InitO C O B O H O = Id C O
29 28 com12 φ O InitO C O B h O H O = h O H O = Id C O
30 10 29 syl5bi φ O InitO C O B ∃! h h O H O O H O = Id C O
31 9 30 syld φ O InitO C O B o B ∃! h h O H o O H O = Id C O
32 31 expimpd φ O InitO C O B o B ∃! h h O H o O H O = Id C O
33 4 32 mpd φ O InitO C O H O = Id C O