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