Metamath Proof Explorer

Theorem termoeu1

Description: Terminal objects are essentially unique (strong form), i.e. there is a unique isomorphism between two terminal 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, 18-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 termoeu1.c ⊢ φ → C ∈ Cat
2 termoeu1.a ⊢ φ → A ∈ TermO ⁡ C
3 termoeu1.b ⊢ φ → B ∈ TermO ⁡ C
4 eqid ⊢ Base C = Base C
5 eqid ⊢ Hom ⁡ C = Hom ⁡ C
6 4 5 1 istermoi ⊢ φ ∧ B ∈ TermO ⁡ C → B ∈ Base C ∧ ∀ a ∈ Base C ∃! f f ∈ a Hom ⁡ C B
7 3 6 mpdan ⊢ φ → B ∈ Base C ∧ ∀ a ∈ Base C ∃! f f ∈ a Hom ⁡ C B
8 4 5 1 istermoi ⊢ φ ∧ A ∈ TermO ⁡ C → A ∈ Base C ∧ ∀ b ∈ Base C ∃! g g ∈ b Hom ⁡ C A
9 2 8 mpdan ⊢ φ → A ∈ Base C ∧ ∀ b ∈ Base C ∃! g g ∈ b Hom ⁡ C A
10 oveq1 ⊢ a = A → a Hom ⁡ C B = A Hom ⁡ C B
11 10 eleq2d ⊢ a = A → f ∈ a Hom ⁡ C B ↔ f ∈ A Hom ⁡ C B
12 11 eubidv ⊢ a = A → ∃! f f ∈ a Hom ⁡ C B ↔ ∃! f f ∈ A Hom ⁡ C B
13 12 rspcv ⊢ A ∈ Base C → ∀ a ∈ Base C ∃! f f ∈ a Hom ⁡ C B → ∃! f f ∈ A Hom ⁡ C B
14 eqid ⊢ Iso ⁡ C = Iso ⁡ C
15 1 adantr ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C → C ∈ Cat
16 simprl ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C → A ∈ Base C
17 simprr ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C → B ∈ Base C
18 4 5 14 15 16 17 isohom ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C → A Iso ⁡ C B ⊆ A Hom ⁡ C B
19 18 adantr ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ ∃! f f ∈ A Hom ⁡ C B ∧ ∀ b ∈ 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 ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C → ∃! f f ∈ A Hom ⁡ C B → ∃ f f ∈ A Hom ⁡ C B
22 oveq1 ⊢ b = B → b Hom ⁡ C A = B Hom ⁡ C A
23 22 eleq2d ⊢ b = B → g ∈ b Hom ⁡ C A ↔ g ∈ B Hom ⁡ C A
24 23 eubidv ⊢ b = B → ∃! g g ∈ b Hom ⁡ C A ↔ ∃! g g ∈ B Hom ⁡ C A
25 24 rspcva ⊢ B ∈ Base C ∧ ∀ b ∈ 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 ⊢ B ∈ Base C ∧ ∀ b ∈ Base C ∃! g g ∈ b Hom ⁡ C A → ∃ g g ∈ B Hom ⁡ C A
28 27 ex ⊢ B ∈ Base C → ∀ b ∈ Base C ∃! g g ∈ b Hom ⁡ C A → ∃ g g ∈ B Hom ⁡ C A
29 28 ad2antll ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C → ∀ b ∈ Base C ∃! g g ∈ b Hom ⁡ C A → ∃ g g ∈ B Hom ⁡ C A
30 eqid ⊢ Inv ⁡ C = Inv ⁡ C
31 15 ad2antrr ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ g ∈ B Hom ⁡ C A ∧ f ∈ A Hom ⁡ C B → C ∈ Cat
32 16 ad2antrr ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ g ∈ B Hom ⁡ C A ∧ f ∈ A Hom ⁡ C B → A ∈ Base C
33 17 ad2antrr ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ g ∈ B Hom ⁡ C A ∧ f ∈ A Hom ⁡ C B → B ∈ Base C
34 1 2 3 2termoinv ⊢ φ ∧ g ∈ B Hom ⁡ C A ∧ f ∈ A Hom ⁡ C B → f A Inv ⁡ C B g
35 34 ad4ant134 ⊢ φ ∧ A ∈ Base C ∧ B ∈ 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 ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ g ∈ B Hom ⁡ C A ∧ f ∈ A Hom ⁡ C B → f ∈ A Iso ⁡ C B
37 36 ex ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ g ∈ B Hom ⁡ C A → f ∈ A Hom ⁡ C B → f ∈ A Iso ⁡ C B
38 37 eximdv ⊢ φ ∧ A ∈ Base C ∧ B ∈ 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 → φ ∧ A ∈ Base C ∧ B ∈ Base C → ∃ f f ∈ A Hom ⁡ C B → ∃ f f ∈ A Iso ⁡ C B
40 39 exlimiv ⊢ ∃ g g ∈ B Hom ⁡ C A → φ ∧ A ∈ Base C ∧ B ∈ Base C → ∃ f f ∈ A Hom ⁡ C B → ∃ f f ∈ A Iso ⁡ C B
41 40 com3l ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C → ∃ f f ∈ A Hom ⁡ C B → ∃ g g ∈ B Hom ⁡ C A → ∃ f f ∈ A Iso ⁡ C B
42 41 impd ⊢ φ ∧ A ∈ Base C ∧ B ∈ 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 ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C → ∃! f f ∈ A Hom ⁡ C B ∧ ∀ b ∈ Base C ∃! g g ∈ b Hom ⁡ C A → ∃ f f ∈ A Iso ⁡ C B
44 43 imp ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ ∃! f f ∈ A Hom ⁡ C B ∧ ∀ b ∈ Base C ∃! g g ∈ b Hom ⁡ C A → ∃ f f ∈ A Iso ⁡ C B
45 simprl ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ ∃! f f ∈ A Hom ⁡ C B ∧ ∀ b ∈ 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 ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ ∃! f f ∈ A Hom ⁡ C B ∧ ∀ b ∈ Base C ∃! g g ∈ b Hom ⁡ C A → ∃! f f ∈ A Iso ⁡ C B
48 47 exp42 ⊢ φ → A ∈ Base C → B ∈ Base C → ∃! f f ∈ A Hom ⁡ C B ∧ ∀ b ∈ Base C ∃! g g ∈ b Hom ⁡ C A → ∃! f f ∈ A Iso ⁡ C B
49 48 com24 ⊢ φ → ∃! f f ∈ A Hom ⁡ C B ∧ ∀ b ∈ Base C ∃! g g ∈ b Hom ⁡ C A → B ∈ Base C → A ∈ Base C → ∃! f f ∈ A Iso ⁡ C B
50 49 com14 ⊢ A ∈ Base C → ∃! f f ∈ A Hom ⁡ C B ∧ ∀ b ∈ Base C ∃! g g ∈ b Hom ⁡ C A → B ∈ Base C → φ → ∃! f f ∈ A Iso ⁡ C B
51 50 expd ⊢ A ∈ Base C → ∃! f f ∈ A Hom ⁡ C B → ∀ b ∈ Base C ∃! g g ∈ b Hom ⁡ C A → B ∈ Base C → φ → ∃! f f ∈ A Iso ⁡ C B
52 13 51 syldc ⊢ ∀ a ∈ Base C ∃! f f ∈ a Hom ⁡ C B → A ∈ Base C → ∀ b ∈ Base C ∃! g g ∈ b Hom ⁡ C A → B ∈ Base C → φ → ∃! f f ∈ A Iso ⁡ C B
53 52 com15 ⊢ φ → A ∈ Base C → ∀ b ∈ Base C ∃! g g ∈ b Hom ⁡ C A → B ∈ Base C → ∀ a ∈ Base C ∃! f f ∈ a Hom ⁡ C B → ∃! f f ∈ A Iso ⁡ C B
54 53 impd ⊢ φ → A ∈ Base C ∧ ∀ b ∈ Base C ∃! g g ∈ b Hom ⁡ C A → B ∈ Base C → ∀ a ∈ Base C ∃! f f ∈ a Hom ⁡ C B → ∃! f f ∈ A Iso ⁡ C B
55 9 54 mpd ⊢ φ → B ∈ Base C → ∀ a ∈ Base C ∃! f f ∈ a Hom ⁡ C B → ∃! f f ∈ A Iso ⁡ C B
56 55 impd ⊢ φ → B ∈ Base C ∧ ∀ a ∈ Base C ∃! f f ∈ a Hom ⁡ C B → ∃! f f ∈ A Iso ⁡ C B
57 7 56 mpd ⊢ φ → ∃! f f ∈ A Iso ⁡ C B