Metamath Proof Explorer

Theorem initoeu2

Description: Initial objects are essentially unique, if A is an initial object, then so is every object that is isomorphic to A. Proposition 7.3 (2) in Adamek p. 102. (Contributed by AV, 10-Apr-2020)

Ref Expression
Hypotheses initoeu1.c ⊢ φ → C ∈ Cat
initoeu1.a ⊢ φ → A ∈ InitO ⁡ C
initoeu2.i ⊢ φ → A ≃ 𝑐 ⁡ C B
Assertion initoeu2 ⊢ φ → B ∈ InitO ⁡ C

Proof

Step Hyp Ref Expression
1 initoeu1.c ⊢ φ → C ∈ Cat
2 initoeu1.a ⊢ φ → A ∈ InitO ⁡ C
3 initoeu2.i ⊢ φ → A ≃ 𝑐 ⁡ C B
4 ciclcl ⊢ C ∈ Cat ∧ A ≃ 𝑐 ⁡ C B → A ∈ Base C
5 1 4 sylan ⊢ φ ∧ A ≃ 𝑐 ⁡ C B → A ∈ Base C
6 cicrcl ⊢ C ∈ Cat ∧ A ≃ 𝑐 ⁡ C B → B ∈ Base C
7 1 6 sylan ⊢ φ ∧ A ≃ 𝑐 ⁡ C B → B ∈ Base C
8 1 adantr ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C → C ∈ Cat
9 cicsym ⊢ C ∈ Cat ∧ A ≃ 𝑐 ⁡ C B → B ≃ 𝑐 ⁡ C A
10 8 9 sylan ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ A ≃ 𝑐 ⁡ C B → B ≃ 𝑐 ⁡ C A
11 eqid ⊢ Iso ⁡ C = Iso ⁡ C
12 eqid ⊢ Base C = Base C
13 simprr ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C → B ∈ Base C
14 simprl ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C → A ∈ Base C
15 11 12 8 13 14 cic ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C → B ≃ 𝑐 ⁡ C A ↔ ∃ k k ∈ B Iso ⁡ C A
16 eqid ⊢ Hom ⁡ C = Hom ⁡ C
17 12 16 1 isinitoi ⊢ φ ∧ A ∈ InitO ⁡ C → A ∈ Base C ∧ ∀ a ∈ Base C ∃! f f ∈ A Hom ⁡ C a
18 2 17 mpdan ⊢ φ → A ∈ Base C ∧ ∀ a ∈ Base C ∃! f f ∈ A Hom ⁡ C a
19 oveq2 ⊢ a = b → A Hom ⁡ C a = A Hom ⁡ C b
20 19 eleq2d ⊢ a = b → f ∈ A Hom ⁡ C a ↔ f ∈ A Hom ⁡ C b
21 20 eubidv ⊢ a = b → ∃! f f ∈ A Hom ⁡ C a ↔ ∃! f f ∈ A Hom ⁡ C b
22 21 rspcva ⊢ b ∈ Base C ∧ ∀ a ∈ Base C ∃! f f ∈ A Hom ⁡ C a → ∃! f f ∈ A Hom ⁡ C b
23 nfv ⊢ Ⅎ h f ∈ A Hom ⁡ C b
24 nfv ⊢ Ⅎ f h ∈ A Hom ⁡ C b
25 eleq1w ⊢ f = h → f ∈ A Hom ⁡ C b ↔ h ∈ A Hom ⁡ C b
26 23 24 25 cbveuw ⊢ ∃! f f ∈ A Hom ⁡ C b ↔ ∃! h h ∈ A Hom ⁡ C b
27 euex ⊢ ∃! h h ∈ A Hom ⁡ C b → ∃ h h ∈ A Hom ⁡ C b
28 1 adantr ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C → C ∈ Cat
29 simpr ⊢ A ∈ Base C ∧ B ∈ Base C → B ∈ Base C
30 29 ad2antrl ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C → B ∈ Base C
31 simprll ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C → A ∈ Base C
32 12 16 11 28 30 31 isohom ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C → B Iso ⁡ C A ⊆ B Hom ⁡ C A
33 32 sselda ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C ∧ k ∈ B Iso ⁡ C A → k ∈ B Hom ⁡ C A
34 eqid ⊢ comp ⁡ C = comp ⁡ C
35 28 ad2antrr ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C ∧ k ∈ B Iso ⁡ C A ∧ k ∈ B Hom ⁡ C A ∧ h ∈ A Hom ⁡ C b → C ∈ Cat
36 30 ad2antrr ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C ∧ k ∈ B Iso ⁡ C A ∧ k ∈ B Hom ⁡ C A ∧ h ∈ A Hom ⁡ C b → B ∈ Base C
37 31 ad2antrr ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C ∧ k ∈ B Iso ⁡ C A ∧ k ∈ B Hom ⁡ C A ∧ h ∈ A Hom ⁡ C b → A ∈ Base C
38 simprr ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C → b ∈ Base C
39 38 ad2antrr ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C ∧ k ∈ B Iso ⁡ C A ∧ k ∈ B Hom ⁡ C A ∧ h ∈ A Hom ⁡ C b → b ∈ Base C
40 simprl ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C ∧ k ∈ B Iso ⁡ C A ∧ k ∈ B Hom ⁡ C A ∧ h ∈ A Hom ⁡ C b → k ∈ B Hom ⁡ C A
41 simprr ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C ∧ k ∈ B Iso ⁡ C A ∧ k ∈ B Hom ⁡ C A ∧ h ∈ A Hom ⁡ C b → h ∈ A Hom ⁡ C b
42 12 16 34 35 36 37 39 40 41 catcocl ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C ∧ k ∈ B Iso ⁡ C A ∧ k ∈ B Hom ⁡ C A ∧ h ∈ A Hom ⁡ C b → h B A comp ⁡ C b k ∈ B Hom ⁡ C b
43 simp-4l ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C ∧ k ∈ B Iso ⁡ C A ∧ k ∈ B Hom ⁡ C A ∧ h ∈ A Hom ⁡ C b ∧ h B A comp ⁡ C b k ∈ B Hom ⁡ C b → φ
44 df-3an ⊢ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C ↔ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C
45 44 biimpri ⊢ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C → A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C
46 45 ad4antlr ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C ∧ k ∈ B Iso ⁡ C A ∧ k ∈ B Hom ⁡ C A ∧ h ∈ A Hom ⁡ C b ∧ h B A comp ⁡ C b k ∈ B Hom ⁡ C b → A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C
47 simpr ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C ∧ k ∈ B Iso ⁡ C A → k ∈ B Iso ⁡ C A
48 47 ad2antrr ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C ∧ k ∈ B Iso ⁡ C A ∧ k ∈ B Hom ⁡ C A ∧ h ∈ A Hom ⁡ C b ∧ h B A comp ⁡ C b k ∈ B Hom ⁡ C b → k ∈ B Iso ⁡ C A
49 41 adantr ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C ∧ k ∈ B Iso ⁡ C A ∧ k ∈ B Hom ⁡ C A ∧ h ∈ A Hom ⁡ C b ∧ h B A comp ⁡ C b k ∈ B Hom ⁡ C b → h ∈ A Hom ⁡ C b
50 simpr ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C ∧ k ∈ B Iso ⁡ C A ∧ k ∈ B Hom ⁡ C A ∧ h ∈ A Hom ⁡ C b ∧ h B A comp ⁡ C b k ∈ B Hom ⁡ C b → h B A comp ⁡ C b k ∈ B Hom ⁡ C b
51 1 2 12 16 11 34 initoeu2lem2 ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C ∧ k ∈ B Iso ⁡ C A ∧ h ∈ A Hom ⁡ C b ∧ h B A comp ⁡ C b k ∈ B Hom ⁡ C b → ∃! f f ∈ A Hom ⁡ C b → ∃! g g ∈ B Hom ⁡ C b
52 43 46 48 49 50 51 syl113anc ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C ∧ k ∈ B Iso ⁡ C A ∧ k ∈ B Hom ⁡ C A ∧ h ∈ A Hom ⁡ C b ∧ h B A comp ⁡ C b k ∈ B Hom ⁡ C b → ∃! f f ∈ A Hom ⁡ C b → ∃! g g ∈ B Hom ⁡ C b
53 42 52 mpdan ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C ∧ k ∈ B Iso ⁡ C A ∧ k ∈ B Hom ⁡ C A ∧ h ∈ A Hom ⁡ C b → ∃! f f ∈ A Hom ⁡ C b → ∃! g g ∈ B Hom ⁡ C b
54 53 ex ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C ∧ k ∈ B Iso ⁡ C A → k ∈ B Hom ⁡ C A ∧ h ∈ A Hom ⁡ C b → ∃! f f ∈ A Hom ⁡ C b → ∃! g g ∈ B Hom ⁡ C b
55 33 54 mpand ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C ∧ k ∈ B Iso ⁡ C A → h ∈ A Hom ⁡ C b → ∃! f f ∈ A Hom ⁡ C b → ∃! g g ∈ B Hom ⁡ C b
56 55 ex ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C → k ∈ B Iso ⁡ C A → h ∈ A Hom ⁡ C b → ∃! f f ∈ A Hom ⁡ C b → ∃! g g ∈ B Hom ⁡ C b
57 56 com23 ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C → h ∈ A Hom ⁡ C b → k ∈ B Iso ⁡ C A → ∃! f f ∈ A Hom ⁡ C b → ∃! g g ∈ B Hom ⁡ C b
58 57 ex ⊢ φ → A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C → h ∈ A Hom ⁡ C b → k ∈ B Iso ⁡ C A → ∃! f f ∈ A Hom ⁡ C b → ∃! g g ∈ B Hom ⁡ C b
59 58 com15 ⊢ ∃! f f ∈ A Hom ⁡ C b → A ∈ Base C ∧ B ∈ Base C ∧ b ∈ Base C → h ∈ A Hom ⁡ C b → k ∈ B Iso ⁡ C A → φ → ∃! g g ∈ B Hom ⁡ C b
60 59 expd ⊢ ∃! f f ∈ A Hom ⁡ C b → A ∈ Base C ∧ B ∈ Base C → b ∈ Base C → h ∈ A Hom ⁡ C b → k ∈ B Iso ⁡ C A → φ → ∃! g g ∈ B Hom ⁡ C b
61 60 com24 ⊢ ∃! f f ∈ A Hom ⁡ C b → h ∈ A Hom ⁡ C b → b ∈ Base C → A ∈ Base C ∧ B ∈ Base C → k ∈ B Iso ⁡ C A → φ → ∃! g g ∈ B Hom ⁡ C b
62 61 com12 ⊢ h ∈ A Hom ⁡ C b → ∃! f f ∈ A Hom ⁡ C b → b ∈ Base C → A ∈ Base C ∧ B ∈ Base C → k ∈ B Iso ⁡ C A → φ → ∃! g g ∈ B Hom ⁡ C b
63 62 exlimiv ⊢ ∃ h h ∈ A Hom ⁡ C b → ∃! f f ∈ A Hom ⁡ C b → b ∈ Base C → A ∈ Base C ∧ B ∈ Base C → k ∈ B Iso ⁡ C A → φ → ∃! g g ∈ B Hom ⁡ C b
64 27 63 syl ⊢ ∃! h h ∈ A Hom ⁡ C b → ∃! f f ∈ A Hom ⁡ C b → b ∈ Base C → A ∈ Base C ∧ B ∈ Base C → k ∈ B Iso ⁡ C A → φ → ∃! g g ∈ B Hom ⁡ C b
65 26 64 sylbi ⊢ ∃! f f ∈ A Hom ⁡ C b → ∃! f f ∈ A Hom ⁡ C b → b ∈ Base C → A ∈ Base C ∧ B ∈ Base C → k ∈ B Iso ⁡ C A → φ → ∃! g g ∈ B Hom ⁡ C b
66 65 pm2.43i ⊢ ∃! f f ∈ A Hom ⁡ C b → b ∈ Base C → A ∈ Base C ∧ B ∈ Base C → k ∈ B Iso ⁡ C A → φ → ∃! g g ∈ B Hom ⁡ C b
67 66 com12 ⊢ b ∈ Base C → ∃! f f ∈ A Hom ⁡ C b → A ∈ Base C ∧ B ∈ Base C → k ∈ B Iso ⁡ C A → φ → ∃! g g ∈ B Hom ⁡ C b
68 67 adantr ⊢ b ∈ Base C ∧ ∀ a ∈ Base C ∃! f f ∈ A Hom ⁡ C a → ∃! f f ∈ A Hom ⁡ C b → A ∈ Base C ∧ B ∈ Base C → k ∈ B Iso ⁡ C A → φ → ∃! g g ∈ B Hom ⁡ C b
69 22 68 mpd ⊢ b ∈ Base C ∧ ∀ a ∈ Base C ∃! f f ∈ A Hom ⁡ C a → A ∈ Base C ∧ B ∈ Base C → k ∈ B Iso ⁡ C A → φ → ∃! g g ∈ B Hom ⁡ C b
70 69 ex ⊢ b ∈ Base C → ∀ a ∈ Base C ∃! f f ∈ A Hom ⁡ C a → A ∈ Base C ∧ B ∈ Base C → k ∈ B Iso ⁡ C A → φ → ∃! g g ∈ B Hom ⁡ C b
71 70 com15 ⊢ φ → ∀ a ∈ Base C ∃! f f ∈ A Hom ⁡ C a → A ∈ Base C ∧ B ∈ Base C → k ∈ B Iso ⁡ C A → b ∈ Base C → ∃! g g ∈ B Hom ⁡ C b
72 71 adantld ⊢ φ → A ∈ Base C ∧ ∀ a ∈ Base C ∃! f f ∈ A Hom ⁡ C a → A ∈ Base C ∧ B ∈ Base C → k ∈ B Iso ⁡ C A → b ∈ Base C → ∃! g g ∈ B Hom ⁡ C b
73 18 72 mpd ⊢ φ → A ∈ Base C ∧ B ∈ Base C → k ∈ B Iso ⁡ C A → b ∈ Base C → ∃! g g ∈ B Hom ⁡ C b
74 73 imp ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C → k ∈ B Iso ⁡ C A → b ∈ Base C → ∃! g g ∈ B Hom ⁡ C b
75 74 exlimdv ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C → ∃ k k ∈ B Iso ⁡ C A → b ∈ Base C → ∃! g g ∈ B Hom ⁡ C b
76 15 75 sylbid ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C → B ≃ 𝑐 ⁡ C A → b ∈ Base C → ∃! g g ∈ B Hom ⁡ C b
77 76 adantr ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ A ≃ 𝑐 ⁡ C B → B ≃ 𝑐 ⁡ C A → b ∈ Base C → ∃! g g ∈ B Hom ⁡ C b
78 10 77 mpd ⊢ φ ∧ A ∈ Base C ∧ B ∈ Base C ∧ A ≃ 𝑐 ⁡ C B → b ∈ Base C → ∃! g g ∈ B Hom ⁡ C b
79 78 an32s ⊢ φ ∧ A ≃ 𝑐 ⁡ C B ∧ A ∈ Base C ∧ B ∈ Base C → b ∈ Base C → ∃! g g ∈ B Hom ⁡ C b
80 79 ralrimiv ⊢ φ ∧ A ≃ 𝑐 ⁡ C B ∧ A ∈ Base C ∧ B ∈ Base C → ∀ b ∈ Base C ∃! g g ∈ B Hom ⁡ C b
81 1 ad2antrr ⊢ φ ∧ A ≃ 𝑐 ⁡ C B ∧ A ∈ Base C ∧ B ∈ Base C → C ∈ Cat
82 simprr ⊢ φ ∧ A ≃ 𝑐 ⁡ C B ∧ A ∈ Base C ∧ B ∈ Base C → B ∈ Base C
83 12 16 81 82 isinito ⊢ φ ∧ A ≃ 𝑐 ⁡ C B ∧ A ∈ Base C ∧ B ∈ Base C → B ∈ InitO ⁡ C ↔ ∀ b ∈ Base C ∃! g g ∈ B Hom ⁡ C b
84 80 83 mpbird ⊢ φ ∧ A ≃ 𝑐 ⁡ C B ∧ A ∈ Base C ∧ B ∈ Base C → B ∈ InitO ⁡ C
85 84 ex ⊢ φ ∧ A ≃ 𝑐 ⁡ C B → A ∈ Base C ∧ B ∈ Base C → B ∈ InitO ⁡ C
86 5 7 85 mp2and ⊢ φ ∧ A ≃ 𝑐 ⁡ C B → B ∈ InitO ⁡ C
87 3 86 mpdan ⊢ φ → B ∈ InitO ⁡ C