Metamath Proof Explorer

Theorem cidfval

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

Ref Expression
Hypotheses cidfval.b 
|- B = ( Base ` C )
cidfval.h 
|- H = ( Hom ` C )
cidfval.o 
|- .x. = ( comp ` C )
cidfval.c 
|- ( ph -> C e. Cat )
cidfval.i 
|- .1. = ( Id ` C )
Assertion cidfval 
|- ( ph -> .1. = ( x e. B |-> ( iota_ 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 cidfval.b 
 |-  B = ( Base ` C )
2 cidfval.h 
 |-  H = ( Hom ` C )
3 cidfval.o 
 |-  .x. = ( comp ` C )
4 cidfval.c 
 |-  ( ph -> C e. Cat )
5 cidfval.i 
 |-  .1. = ( Id ` C )
6 fvexd 
 |-  ( c = C -> ( Base ` c ) e. _V )
7 fveq2 
 |-  ( c = C -> ( Base ` c ) = ( Base ` C ) )
8 7 1 eqtr4di 
 |-  ( c = C -> ( Base ` c ) = B )
9 fvexd 
 |-  ( ( c = C /\ b = B ) -> ( Hom ` c ) e. _V )
10 simpl 
 |-  ( ( c = C /\ b = B ) -> c = C )
11 10 fveq2d 
 |-  ( ( c = C /\ b = B ) -> ( Hom ` c ) = ( Hom ` C ) )
12 11 2 eqtr4di 
 |-  ( ( c = C /\ b = B ) -> ( Hom ` c ) = H )
13 fvexd 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> ( comp ` c ) e. _V )
14 simpll 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> c = C )
15 14 fveq2d 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> ( comp ` c ) = ( comp ` C ) )
16 15 3 eqtr4di 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> ( comp ` c ) = .x. )
17 simpllr 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> b = B )
18 simplr 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> h = H )
19 18 oveqd 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( x h x ) = ( x H x ) )
20 18 oveqd 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( y h x ) = ( y H x ) )
21 simpr 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> o = .x. )
22 21 oveqd 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( <. y , x >. o x ) = ( <. y , x >. .x. x ) )
23 22 oveqd 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( g ( <. y , x >. o x ) f ) = ( g ( <. y , x >. .x. x ) f ) )
24 23 eqeq1d 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( ( g ( <. y , x >. o x ) f ) = f <-> ( g ( <. y , x >. .x. x ) f ) = f ) )
25 20 24 raleqbidv 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f <-> A. f e. ( y H x ) ( g ( <. y , x >. .x. x ) f ) = f ) )
26 18 oveqd 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( x h y ) = ( x H y ) )
27 21 oveqd 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( <. x , x >. o y ) = ( <. x , x >. .x. y ) )
28 27 oveqd 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( f ( <. x , x >. o y ) g ) = ( f ( <. x , x >. .x. y ) g ) )
29 28 eqeq1d 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( ( f ( <. x , x >. o y ) g ) = f <-> ( f ( <. x , x >. .x. y ) g ) = f ) )
30 26 29 raleqbidv 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f <-> A. f e. ( x H y ) ( f ( <. x , x >. .x. y ) g ) = f ) )
31 25 30 anbi12d 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o 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 ) ) )
32 17 31 raleqbidv 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o 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 ) ) )
33 19 32 riotaeqbidv 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( iota_ g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) ) = ( iota_ 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 ) ) )
34 17 33 mpteq12dv 
 |-  ( ( ( ( c = C /\ b = B ) /\ h = H ) /\ o = .x. ) -> ( x e. b |-> ( iota_ g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) ) ) = ( x e. B |-> ( iota_ 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 ) ) ) )
35 13 16 34 csbied2 
 |-  ( ( ( c = C /\ b = B ) /\ h = H ) -> [_ ( comp ` c ) / o ]_ ( x e. b |-> ( iota_ g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) ) ) = ( x e. B |-> ( iota_ 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 ) ) ) )
36 9 12 35 csbied2 
 |-  ( ( c = C /\ b = B ) -> [_ ( Hom ` c ) / h ]_ [_ ( comp ` c ) / o ]_ ( x e. b |-> ( iota_ g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) ) ) = ( x e. B |-> ( iota_ 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 ) ) ) )
37 6 8 36 csbied2 
 |-  ( c = C -> [_ ( Base ` c ) / b ]_ [_ ( Hom ` c ) / h ]_ [_ ( comp ` c ) / o ]_ ( x e. b |-> ( iota_ g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) ) ) = ( x e. B |-> ( iota_ 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 ) ) ) )
38 df-cid 
 |-  Id = ( c e. Cat |-> [_ ( Base ` c ) / b ]_ [_ ( Hom ` c ) / h ]_ [_ ( comp ` c ) / o ]_ ( x e. b |-> ( iota_ g e. ( x h x ) A. y e. b ( A. f e. ( y h x ) ( g ( <. y , x >. o x ) f ) = f /\ A. f e. ( x h y ) ( f ( <. x , x >. o y ) g ) = f ) ) ) )
39 37 38 1 mptfvmpt 
 |-  ( C e. Cat -> ( Id ` C ) = ( x e. B |-> ( iota_ 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 ) ) ) )
40 4 39 syl 
 |-  ( ph -> ( Id ` C ) = ( x e. B |-> ( iota_ 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 ) ) ) )
41 5 40 syl5eq 
 |-  ( ph -> .1. = ( x e. B |-> ( iota_ 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 ) ) ) )