Metamath Proof Explorer

Theorem catidex

Description: Each object in a category has an associated 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 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 ) )

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 id 
 |-  ( x = X -> x = X )
7 6 6 oveq12d 
 |-  ( x = X -> ( x H x ) = ( X H X ) )
8 oveq2 
 |-  ( x = X -> ( y H x ) = ( y H X ) )
9 opeq2 
 |-  ( x = X -> <. y , x >. = <. y , X >. )
10 9 6 oveq12d 
 |-  ( x = X -> ( <. y , x >. .x. x ) = ( <. y , X >. .x. X ) )
11 10 oveqd 
 |-  ( x = X -> ( g ( <. y , x >. .x. x ) f ) = ( g ( <. y , X >. .x. X ) f ) )
12 11 eqeq1d 
 |-  ( x = X -> ( ( g ( <. y , x >. .x. x ) f ) = f <-> ( g ( <. y , X >. .x. X ) f ) = f ) )
13 8 12 raleqbidv 
 |-  ( x = X -> ( A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f <-> A. f e. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f ) )
14 oveq1 
 |-  ( x = X -> ( x H y ) = ( X H y ) )
15 6 6 opeq12d 
 |-  ( x = X -> <. x , x >. = <. X , X >. )
16 15 oveq1d 
 |-  ( x = X -> ( <. x , x >. .x. y ) = ( <. X , X >. .x. y ) )
17 16 oveqd 
 |-  ( x = X -> ( f ( <. x , x >. .x. y ) g ) = ( f ( <. X , X >. .x. y ) g ) )
18 17 eqeq1d 
 |-  ( x = X -> ( ( f ( <. x , x >. .x. y ) g ) = f <-> ( f ( <. X , X >. .x. y ) g ) = f ) )
19 14 18 raleqbidv 
 |-  ( x = X -> ( A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f <-> A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) )
20 13 19 anbi12d 
 |-  ( x = 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. ( y H X ) ( g ( <. y , X >. .x. X ) f ) = f /\ A. f e. ( X H y ) ( f ( <. X , X >. .x. y ) g ) = f ) ) )
21 20 ralbidv 
 |-  ( x = 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. 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 ) ) )
22 7 21 rexeqbidv 
 |-  ( x = X -> ( 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 ) ) )
23 1 2 3 iscat 
 |-  ( C e. Cat -> ( C e. Cat <-> A. x e. B ( 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 ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) ) )
24 23 ibi 
 |-  ( C e. Cat -> A. x e. B ( 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 ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) )
25 simpl 
 |-  ( ( 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 ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) 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 ) )
26 25 ralimi 
 |-  ( A. x e. B ( 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 ) /\ A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) /\ A. w e. B A. k e. ( z H w ) ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) ) ) -> A. x e. B 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 ) )
27 4 24 26 3syl 
 |-  ( ph -> A. x e. B 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 ) )
28 22 27 5 rspcdva 
 |-  ( 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 ) )