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 biimtrid ⊢ φ ∧ 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