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=BaseC
isinitoi.h ⊢H=Hom⁡C
isinitoi.c ⊢φ→C∈Cat
Assertion initoid ⊢φ∧O∈InitO⁡C→OHO=Id⁡C⁡O

Proof

Step Hyp Ref Expression
1 isinitoi.b ⊢B=BaseC
2 isinitoi.h ⊢H=Hom⁡C
3 isinitoi.c ⊢φ→C∈Cat
4 1 2 3 isinitoi ⊢φ∧O∈InitO⁡C→O∈B∧∀o∈B∃!hh∈OHo
5 oveq2 ⊢o=O→OHo=OHO
6 5 eleq2d ⊢o=O→h∈OHo↔h∈OHO
7 6 eubidv ⊢o=O→∃!hh∈OHo↔∃!hh∈OHO
8 7 rspcv ⊢O∈B→∀o∈B∃!hh∈OHo→∃!hh∈OHO
9 8 adantl ⊢φ∧O∈InitO⁡C∧O∈B→∀o∈B∃!hh∈OHo→∃!hh∈OHO
10 eusn ⊢∃!hh∈OHO↔∃hOHO=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∈OHO
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 ⊢OHO=h→Id⁡C⁡O∈h→h=Id⁡C⁡O
24 eleq2 ⊢OHO=h→Id⁡C⁡O∈OHO↔Id⁡C⁡O∈h
25 eqeq1 ⊢OHO=h→OHO=Id⁡C⁡O↔h=Id⁡C⁡O
26 23 24 25 3imtr4d ⊢OHO=h→Id⁡C⁡O∈OHO→OHO=Id⁡C⁡O
27 14 26 syl5 ⊢OHO=h→φ∧O∈InitO⁡C∧O∈B→OHO=Id⁡C⁡O
28 27 exlimiv ⊢∃hOHO=h→φ∧O∈InitO⁡C∧O∈B→OHO=Id⁡C⁡O
29 28 com12 ⊢φ∧O∈InitO⁡C∧O∈B→∃hOHO=h→OHO=Id⁡C⁡O
30 10 29 biimtrid ⊢φ∧O∈InitO⁡C∧O∈B→∃!hh∈OHO→OHO=Id⁡C⁡O
31 9 30 syld ⊢φ∧O∈InitO⁡C∧O∈B→∀o∈B∃!hh∈OHo→OHO=Id⁡C⁡O
32 31 expimpd ⊢φ∧O∈InitO⁡C→O∈B∧∀o∈B∃!hh∈OHo→OHO=Id⁡C⁡O
33 4 32 mpd ⊢φ∧O∈InitO⁡C→OHO=Id⁡C⁡O