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 
|- ( ph -> C e. Cat )
initoeu1.a 
|- ( ph -> A e. ( InitO ` C ) )
initoeu1.b 
|- ( ph -> B e. ( InitO ` C ) )
Assertion initoeu1 
|- ( ph -> E! f f e. ( A ( Iso ` C ) B ) )

Proof

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