Metamath Proof Explorer

Theorem initoeu1

Description: Initial objects are essentially unique (strong form), i.e. there is a unique isomorphism between two initial objects, see statement in Lang p. 58 ("... if P, P' are two universal objects [... then there exists a unique isomorphism between them.". (Proposed by BJ, 14-Apr-2020.) (Contributed by AV, 14-Apr-2020)

Ref Expression
Hypotheses initoeu1.c ⊢ φ → C ∈ Cat
initoeu1.a ⊢ φ → A ∈ InitO ⁡ C
initoeu1.b ⊢ φ → B ∈ InitO ⁡ C
Assertion initoeu1 ⊢ φ → ∃! f f ∈ A Iso ⁡ C B

Proof

Step Hyp Ref Expression
1 initoeu1.c ⊢ φ → C ∈ Cat
2 initoeu1.a ⊢ φ → A ∈ InitO ⁡ C
3 initoeu1.b ⊢ φ → B ∈ InitO ⁡ C
4 eqid ⊢ Base C = Base C
5 eqid ⊢ Hom ⁡ C = Hom ⁡ C
6 4 5 1 isinitoi ⊢ φ ∧ A ∈ InitO ⁡ C → A ∈ Base C ∧ ∀ b ∈ Base C ∃! f f ∈ A Hom ⁡ C b
7 2 6 mpdan ⊢ φ → A ∈ Base C ∧ ∀ b ∈ Base C ∃! f f ∈ A Hom ⁡ C b
8 4 5 1 isinitoi ⊢ φ ∧ B ∈ InitO ⁡ C → B ∈ Base C ∧ ∀ a ∈ Base C ∃! g g ∈ B Hom ⁡ C a
9 3 8 mpdan ⊢ φ → B ∈ Base C ∧ ∀ a ∈ Base C ∃! g g ∈ B Hom ⁡ C a
10 oveq2 ⊢ b = B → A Hom ⁡ C b = A Hom ⁡ C B
11 10 eleq2d ⊢ b = B → f ∈ A Hom ⁡ C b ↔ f ∈ A Hom ⁡ C B
12 11 eubidv ⊢ b = B → ∃! f f ∈ A Hom ⁡ C b ↔ ∃! f f ∈ A Hom ⁡ C B
13 12 rspcv ⊢ B ∈ Base C → ∀ b ∈ Base C ∃! f f ∈ A Hom ⁡ C b → ∃! f f ∈ A Hom ⁡ C B
14 eqid ⊢ Iso ⁡ C = Iso ⁡ C
15 1 adantr ⊢ φ ∧ B ∈ Base C ∧ A ∈ Base C → C ∈ Cat
16 simprr ⊢ φ ∧ B ∈ Base C ∧ A ∈ Base C → A ∈ Base C
17 simprl ⊢ φ ∧ B ∈ Base C ∧ A ∈ Base C → B ∈ Base C
18 4 5 14 15 16 17 isohom ⊢ φ ∧ B ∈ Base C ∧ A ∈ Base C → A Iso ⁡ C B ⊆ A Hom ⁡ C B
19 18 adantr ⊢ φ ∧ B ∈ Base C ∧ A ∈ Base C ∧ ∃! f f ∈ A Hom ⁡ C B ∧ ∀ a ∈ Base C ∃! g g ∈ B Hom ⁡ C a → A Iso ⁡ C B ⊆ A Hom ⁡ C B
20 euex ⊢ ∃! f f ∈ A Hom ⁡ C B → ∃ f f ∈ A Hom ⁡ C B
21 20 a1i ⊢ φ ∧ B ∈ Base C ∧ A ∈ Base C → ∃! f f ∈ A Hom ⁡ C B → ∃ f f ∈ A Hom ⁡ C B
22 oveq2 ⊢ a = A → B Hom ⁡ C a = B Hom ⁡ C A
23 22 eleq2d ⊢ a = A → g ∈ B Hom ⁡ C a ↔ g ∈ B Hom ⁡ C A
24 23 eubidv ⊢ a = A → ∃! g g ∈ B Hom ⁡ C a ↔ ∃! g g ∈ B Hom ⁡ C A
25 24 rspcva ⊢ A ∈ Base C ∧ ∀ a ∈ Base C ∃! g g ∈ B Hom ⁡ C a → ∃! g g ∈ B Hom ⁡ C A
26 euex ⊢ ∃! g g ∈ B Hom ⁡ C A → ∃ g g ∈ B Hom ⁡ C A
27 25 26 syl ⊢ A ∈ Base C ∧ ∀ a ∈ Base C ∃! g g ∈ B Hom ⁡ C a → ∃ g g ∈ B Hom ⁡ C A
28 27 ex ⊢ A ∈ Base C → ∀ a ∈ Base C ∃! g g ∈ B Hom ⁡ C a → ∃ g g ∈ B Hom ⁡ C A
29 28 ad2antll ⊢ φ ∧ B ∈ Base C ∧ A ∈ Base C → ∀ a ∈ Base C ∃! g g ∈ B Hom ⁡ C a → ∃ g g ∈ B Hom ⁡ C A
30 eqid ⊢ Inv ⁡ C = Inv ⁡ C
31 15 ad2antrr ⊢ φ ∧ B ∈ Base C ∧ A ∈ Base C ∧ g ∈ B Hom ⁡ C A ∧ f ∈ A Hom ⁡ C B → C ∈ Cat
32 16 ad2antrr ⊢ φ ∧ B ∈ Base C ∧ A ∈ Base C ∧ g ∈ B Hom ⁡ C A ∧ f ∈ A Hom ⁡ C B → A ∈ Base C
33 17 ad2antrr ⊢ φ ∧ B ∈ Base C ∧ A ∈ Base C ∧ g ∈ B Hom ⁡ C A ∧ f ∈ A Hom ⁡ C B → B ∈ Base C
34 1 2 3 2initoinv ⊢ φ ∧ g ∈ B Hom ⁡ C A ∧ f ∈ A Hom ⁡ C B → f A Inv ⁡ C B g
35 34 ad4ant134 ⊢ φ ∧ B ∈ Base C ∧ A ∈ Base C ∧ g ∈ B Hom ⁡ C A ∧ f ∈ A Hom ⁡ C B → f A Inv ⁡ C B g
36 4 30 31 32 33 14 35 inviso1 ⊢ φ ∧ B ∈ Base C ∧ A ∈ Base C ∧ g ∈ B Hom ⁡ C A ∧ f ∈ A Hom ⁡ C B → f ∈ A Iso ⁡ C B
37 36 ex ⊢ φ ∧ B ∈ Base C ∧ A ∈ Base C ∧ g ∈ B Hom ⁡ C A → f ∈ A Hom ⁡ C B → f ∈ A Iso ⁡ C B
38 37 eximdv ⊢ φ ∧ B ∈ Base C ∧ A ∈ Base C ∧ g ∈ B Hom ⁡ C A → ∃ f f ∈ A Hom ⁡ C B → ∃ f f ∈ A Iso ⁡ C B
39 38 expcom ⊢ g ∈ B Hom ⁡ C A → φ ∧ B ∈ Base C ∧ A ∈ Base C → ∃ f f ∈ A Hom ⁡ C B → ∃ f f ∈ A Iso ⁡ C B
40 39 exlimiv ⊢ ∃ g g ∈ B Hom ⁡ C A → φ ∧ B ∈ Base C ∧ A ∈ Base C → ∃ f f ∈ A Hom ⁡ C B → ∃ f f ∈ A Iso ⁡ C B
41 40 com3l ⊢ φ ∧ B ∈ Base C ∧ A ∈ Base C → ∃ f f ∈ A Hom ⁡ C B → ∃ g g ∈ B Hom ⁡ C A → ∃ f f ∈ A Iso ⁡ C B
42 41 impd ⊢ φ ∧ B ∈ Base C ∧ A ∈ Base C → ∃ f f ∈ A Hom ⁡ C B ∧ ∃ g g ∈ B Hom ⁡ C A → ∃ f f ∈ A Iso ⁡ C B
43 21 29 42 syl2and ⊢ φ ∧ B ∈ Base C ∧ A ∈ Base C → ∃! f f ∈ A Hom ⁡ C B ∧ ∀ a ∈ Base C ∃! g g ∈ B Hom ⁡ C a → ∃ f f ∈ A Iso ⁡ C B
44 43 imp ⊢ φ ∧ B ∈ Base C ∧ A ∈ Base C ∧ ∃! f f ∈ A Hom ⁡ C B ∧ ∀ a ∈ Base C ∃! g g ∈ B Hom ⁡ C a → ∃ f f ∈ A Iso ⁡ C B
45 simprl ⊢ φ ∧ B ∈ Base C ∧ A ∈ Base C ∧ ∃! f f ∈ A Hom ⁡ C B ∧ ∀ a ∈ Base C ∃! g g ∈ B Hom ⁡ C a → ∃! f f ∈ A Hom ⁡ C B
46 euelss ⊢ A Iso ⁡ C B ⊆ A Hom ⁡ C B ∧ ∃ f f ∈ A Iso ⁡ C B ∧ ∃! f f ∈ A Hom ⁡ C B → ∃! f f ∈ A Iso ⁡ C B
47 19 44 45 46 syl3anc ⊢ φ ∧ B ∈ Base C ∧ A ∈ Base C ∧ ∃! f f ∈ A Hom ⁡ C B ∧ ∀ a ∈ Base C ∃! g g ∈ B Hom ⁡ C a → ∃! f f ∈ A Iso ⁡ C B
48 47 exp42 ⊢ φ → B ∈ Base C → A ∈ Base C → ∃! f f ∈ A Hom ⁡ C B ∧ ∀ a ∈ Base C ∃! g g ∈ B Hom ⁡ C a → ∃! f f ∈ A Iso ⁡ C B
49 48 com24 ⊢ φ → ∃! f f ∈ A Hom ⁡ C B ∧ ∀ a ∈ Base C ∃! g g ∈ B Hom ⁡ C a → A ∈ Base C → B ∈ Base C → ∃! f f ∈ A Iso ⁡ C B
50 49 com14 ⊢ B ∈ Base C → ∃! f f ∈ A Hom ⁡ C B ∧ ∀ a ∈ Base C ∃! g g ∈ B Hom ⁡ C a → A ∈ Base C → φ → ∃! f f ∈ A Iso ⁡ C B
51 50 expd ⊢ B ∈ Base C → ∃! f f ∈ A Hom ⁡ C B → ∀ a ∈ Base C ∃! g g ∈ B Hom ⁡ C a → A ∈ Base C → φ → ∃! f f ∈ A Iso ⁡ C B
52 13 51 syldc ⊢ ∀ b ∈ Base C ∃! f f ∈ A Hom ⁡ C b → B ∈ Base C → ∀ a ∈ Base C ∃! g g ∈ B Hom ⁡ C a → A ∈ Base C → φ → ∃! f f ∈ A Iso ⁡ C B
53 52 com15 ⊢ φ → B ∈ Base C → ∀ a ∈ Base C ∃! g g ∈ B Hom ⁡ C a → A ∈ Base C → ∀ b ∈ Base C ∃! f f ∈ A Hom ⁡ C b → ∃! f f ∈ A Iso ⁡ C B
54 53 impd ⊢ φ → B ∈ Base C ∧ ∀ a ∈ Base C ∃! g g ∈ B Hom ⁡ C a → A ∈ Base C → ∀ b ∈ Base C ∃! f f ∈ A Hom ⁡ C b → ∃! f f ∈ A Iso ⁡ C B
55 9 54 mpd ⊢ φ → A ∈ Base C → ∀ b ∈ Base C ∃! f f ∈ A Hom ⁡ C b → ∃! f f ∈ A Iso ⁡ C B
56 55 impd ⊢ φ → A ∈ Base C ∧ ∀ b ∈ Base C ∃! f f ∈ A Hom ⁡ C b → ∃! f f ∈ A Iso ⁡ C B
57 7 56 mpd ⊢ φ → ∃! f f ∈ A Iso ⁡ C B