Metamath Proof Explorer

Theorem cidval

Description: Each object in a category has an associated identity arrow. (Contributed by Mario Carneiro, 2-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 )
cidval.x 
|- ( ph -> X e. B )
Assertion cidval 
|- ( ph -> ( .1. ` X ) = ( 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 cidval.x 
 |-  ( ph -> X e. B )
7 1 2 3 4 5 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 ) ) ) )
8 simpr 
 |-  ( ( ph /\ x = X ) -> x = X )
9 8 8 oveq12d 
 |-  ( ( ph /\ x = X ) -> ( x H x ) = ( X H X ) )
10 8 oveq2d 
 |-  ( ( ph /\ x = X ) -> ( y H x ) = ( y H X ) )
11 8 opeq2d 
 |-  ( ( ph /\ x = X ) -> <. y , x >. = <. y , X >. )
12 11 8 oveq12d 
 |-  ( ( ph /\ x = X ) -> ( <. y , x >. .x. x ) = ( <. y , X >. .x. X ) )
13 12 oveqd 
 |-  ( ( ph /\ x = X ) -> ( g ( <. y , x >. .x. x ) f ) = ( g ( <. y , X >. .x. X ) f ) )
14 13 eqeq1d 
 |-  ( ( ph /\ x = X ) -> ( ( g ( <. y , x >. .x. x ) f ) = f <-> ( g ( <. y , X >. .x. X ) f ) = f ) )
15 10 14 raleqbidv 
 |-  ( ( ph /\ 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 ) )
16 8 oveq1d 
 |-  ( ( ph /\ x = X ) -> ( x H y ) = ( X H y ) )
17 8 8 opeq12d 
 |-  ( ( ph /\ x = X ) -> <. x , x >. = <. X , X >. )
18 17 oveq1d 
 |-  ( ( ph /\ x = X ) -> ( <. x , x >. .x. y ) = ( <. X , X >. .x. y ) )
19 18 oveqd 
 |-  ( ( ph /\ x = X ) -> ( f ( <. x , x >. .x. y ) g ) = ( f ( <. X , X >. .x. y ) g ) )
20 19 eqeq1d 
 |-  ( ( ph /\ x = X ) -> ( ( f ( <. x , x >. .x. y ) g ) = f <-> ( f ( <. X , X >. .x. y ) g ) = f ) )
21 16 20 raleqbidv 
 |-  ( ( ph /\ 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 ) )
22 15 21 anbi12d 
 |-  ( ( ph /\ 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 ) ) )
23 22 ralbidv 
 |-  ( ( ph /\ 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 ) ) )
24 9 23 riotaeqbidv 
 |-  ( ( ph /\ x = X ) -> ( 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 ) ) = ( 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 ) ) )
25 riotaex 
 |-  ( 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 ) ) e. _V
26 25 a1i 
 |-  ( ph -> ( 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 ) ) e. _V )
27 7 24 6 26 fvmptd 
 |-  ( ph -> ( .1. ` X ) = ( 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 ) ) )