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 ⊢φ→∃!ff∈AIso⁡CB

Proof

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