Metamath Proof Explorer

Theorem catideu

Description: Each object in a category has a unique identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses catidex.b 
|- B = ( Base ` C )
catidex.h 
|- H = ( Hom ` C )
catidex.o 
|- .x. = ( comp ` C )
catidex.c 
|- ( ph -> C e. Cat )
catidex.x 
|- ( ph -> X e. B )
Assertion catideu 
|- ( ph -> E! g e. ( X H X ) A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) )

Proof

Step Hyp Ref Expression
1 catidex.b 
 |-  B = ( Base ` C )
2 catidex.h 
 |-  H = ( Hom ` C )
3 catidex.o 
 |-  .x. = ( comp ` C )
4 catidex.c 
 |-  ( ph -> C e. Cat )
5 catidex.x 
 |-  ( ph -> X e. B )
6 1 2 3 4 5 catidex 
 |-  ( ph -> E. g e. ( X H X ) A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) )
7 oveq1 
 |-  ( y = X -> ( y H X ) = ( X H X ) )
8 opeq1 
 |-  ( y = X -> <. y , X >. = <. X , X >. )
9 8 oveq1d 
 |-  ( y = X -> ( <. y , X >. .x. X ) = ( <. X , X >. .x. X ) )
10 9 oveqd 
 |-  ( y = X -> ( g ( <. y , X >. .x. X ) f ) = ( g ( <. X , X >. .x. X ) f ) )
11 10 eqeq1d 
 |-  ( y = X -> ( ( g ( <. y , X >. .x. X ) f ) = f <-> ( g ( <. X , X >. .x. X ) f ) = f ) )
12 7 11 raleqbidv 
 |-  ( y = X -> ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f <-> A. f e. ( X H X ) ( g ( <. X , X >. .x. X ) f ) = f ) )
13 oveq2 
 |-  ( y = X -> ( X H y ) = ( X H X ) )
14 oveq2 
 |-  ( y = X -> ( <. X , X >. .x. y ) = ( <. X , X >. .x. X ) )
15 14 oveqd 
 |-  ( y = X -> ( f ( <. X , X >. .x. y ) g ) = ( f ( <. X , X >. .x. X ) g ) )
16 15 eqeq1d 
 |-  ( y = X -> ( ( f ( <. X , X >. .x. y ) g ) = f <-> ( f ( <. X , X >. .x. X ) g ) = f ) )
17 13 16 raleqbidv 
 |-  ( y = X -> ( A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f <-> A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) g ) = f ) )
18 12 17 anbi12d 
 |-  ( y = X -> ( ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) <-> ( A. f e. ( X H X ) ( g ( <. X , X >. .x. X ) f ) = f /\ A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) g ) = f ) ) )
19 18 rspcv 
 |-  ( X e. B -> ( A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) -> ( A. f e. ( X H X ) ( g ( <. X , X >. .x. X ) f ) = f /\ A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) g ) = f ) ) )
20 5 19 syl 
 |-  ( ph -> ( A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) -> ( A. f e. ( X H X ) ( g ( <. X , X >. .x. X ) f ) = f /\ A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) g ) = f ) ) )
21 20 ralrimivw 
 |-  ( ph -> A. g e. ( X H X ) ( A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) -> ( A. f e. ( X H X ) ( g ( <. X , X >. .x. X ) f ) = f /\ A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) g ) = f ) ) )
22 an3 
 |-  ( ( ( A. f e. ( X H X ) ( g ( <. X , X >. .x. X ) f ) = f /\ A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) g ) = f ) /\ ( A. f e. ( X H X ) ( h ( <. X , X >. .x. X ) f ) = f /\ A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) h ) = f ) ) -> ( A. f e. ( X H X ) ( g ( <. X , X >. .x. X ) f ) = f /\ A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) h ) = f ) )
23 oveq2 
 |-  ( f = h -> ( g ( <. X , X >. .x. X ) f ) = ( g ( <. X , X >. .x. X ) h ) )
24 id 
 |-  ( f = h -> f = h )
25 23 24 eqeq12d 
 |-  ( f = h -> ( ( g ( <. X , X >. .x. X ) f ) = f <-> ( g ( <. X , X >. .x. X ) h ) = h ) )
26 25 rspcv 
 |-  ( h e. ( X H X ) -> ( A. f e. ( X H X ) ( g ( <. X , X >. .x. X ) f ) = f -> ( g ( <. X , X >. .x. X ) h ) = h ) )
27 oveq1 
 |-  ( f = g -> ( f ( <. X , X >. .x. X ) h ) = ( g ( <. X , X >. .x. X ) h ) )
28 id 
 |-  ( f = g -> f = g )
29 27 28 eqeq12d 
 |-  ( f = g -> ( ( f ( <. X , X >. .x. X ) h ) = f <-> ( g ( <. X , X >. .x. X ) h ) = g ) )
30 29 rspcv 
 |-  ( g e. ( X H X ) -> ( A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) h ) = f -> ( g ( <. X , X >. .x. X ) h ) = g ) )
31 26 30 im2anan9r 
 |-  ( ( g e. ( X H X ) /\ h e. ( X H X ) ) -> ( ( A. f e. ( X H X ) ( g ( <. X , X >. .x. X ) f ) = f /\ A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) h ) = f ) -> ( ( g ( <. X , X >. .x. X ) h ) = h /\ ( g ( <. X , X >. .x. X ) h ) = g ) ) )
32 eqtr2 
 |-  ( ( ( g ( <. X , X >. .x. X ) h ) = h /\ ( g ( <. X , X >. .x. X ) h ) = g ) -> h = g )
33 32 equcomd 
 |-  ( ( ( g ( <. X , X >. .x. X ) h ) = h /\ ( g ( <. X , X >. .x. X ) h ) = g ) -> g = h )
34 22 31 33 syl56 
 |-  ( ( g e. ( X H X ) /\ h e. ( X H X ) ) -> ( ( ( A. f e. ( X H X ) ( g ( <. X , X >. .x. X ) f ) = f /\ A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) g ) = f ) /\ ( A. f e. ( X H X ) ( h ( <. X , X >. .x. X ) f ) = f /\ A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) h ) = f ) ) -> g = h ) )
35 34 rgen2 
 |-  A. g e. ( X H X ) A. h e. ( X H X ) ( ( ( A. f e. ( X H X ) ( g ( <. X , X >. .x. X ) f ) = f /\ A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) g ) = f ) /\ ( A. f e. ( X H X ) ( h ( <. X , X >. .x. X ) f ) = f /\ A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) h ) = f ) ) -> g = h )
36 35 a1i 
 |-  ( ph -> A. g e. ( X H X ) A. h e. ( X H X ) ( ( ( A. f e. ( X H X ) ( g ( <. X , X >. .x. X ) f ) = f /\ A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) g ) = f ) /\ ( A. f e. ( X H X ) ( h ( <. X , X >. .x. X ) f ) = f /\ A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) h ) = f ) ) -> g = h ) )
37 oveq1 
 |-  ( g = h -> ( g ( <. X , X >. .x. X ) f ) = ( h ( <. X , X >. .x. X ) f ) )
38 37 eqeq1d 
 |-  ( g = h -> ( ( g ( <. X , X >. .x. X ) f ) = f <-> ( h ( <. X , X >. .x. X ) f ) = f ) )
39 38 ralbidv 
 |-  ( g = h -> ( A. f e. ( X H X ) ( g ( <. X , X >. .x. X ) f ) = f <-> A. f e. ( X H X ) ( h ( <. X , X >. .x. X ) f ) = f ) )
40 oveq2 
 |-  ( g = h -> ( f ( <. X , X >. .x. X ) g ) = ( f ( <. X , X >. .x. X ) h ) )
41 40 eqeq1d 
 |-  ( g = h -> ( ( f ( <. X , X >. .x. X ) g ) = f <-> ( f ( <. X , X >. .x. X ) h ) = f ) )
42 41 ralbidv 
 |-  ( g = h -> ( A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) g ) = f <-> A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) h ) = f ) )
43 39 42 anbi12d 
 |-  ( g = h -> ( ( A. f e. ( X H X ) ( g ( <. X , X >. .x. X ) f ) = f /\ A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) g ) = f ) <-> ( A. f e. ( X H X ) ( h ( <. X , X >. .x. X ) f ) = f /\ A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) h ) = f ) ) )
44 43 rmo4 
 |-  ( E* g e. ( X H X ) ( A. f e. ( X H X ) ( g ( <. X , X >. .x. X ) f ) = f /\ A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) g ) = f ) <-> A. g e. ( X H X ) A. h e. ( X H X ) ( ( ( A. f e. ( X H X ) ( g ( <. X , X >. .x. X ) f ) = f /\ A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) g ) = f ) /\ ( A. f e. ( X H X ) ( h ( <. X , X >. .x. X ) f ) = f /\ A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) h ) = f ) ) -> g = h ) )
45 36 44 sylibr 
 |-  ( ph -> E* g e. ( X H X ) ( A. f e. ( X H X ) ( g ( <. X , X >. .x. X ) f ) = f /\ A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) g ) = f ) )
46 rmoim 
 |-  ( A. g e. ( X H X ) ( A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) -> ( A. f e. ( X H X ) ( g ( <. X , X >. .x. X ) f ) = f /\ A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) g ) = f ) ) -> ( E* g e. ( X H X ) ( A. f e. ( X H X ) ( g ( <. X , X >. .x. X ) f ) = f /\ A. f e. ( X H X ) ( f ( <. X , X >. .x. X ) g ) = f ) -> E* g e. ( X H X ) A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) ) )
47 21 45 46 sylc 
 |-  ( ph -> E* g e. ( X H X ) A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) )
48 reu5 
 |-  ( E! g e. ( X H X ) A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) <-> ( E. g e. ( X H X ) A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) /\ E* g e. ( X H X ) A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) ) )
49 6 47 48 sylanbrc 
 |-  ( ph -> E! g e. ( X H X ) A. y e. B ( A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) )