Metamath Proof Explorer

Theorem coafval

Description: The value of the composition of arrows. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses coafval.o 
|- .x. = ( compA ` C )
coafval.a 
|- A = ( Arrow ` C )
coafval.x 
|- .xb = ( comp ` C )
Assertion coafval 
|- .x. = ( g e. A , f e. { h e. A | ( codA ` h ) = ( domA ` g ) } |-> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. .xb ( codA ` g ) ) ( 2nd ` f ) ) >. )

Proof

Step Hyp Ref Expression
1 coafval.o 
 |-  .x. = ( compA ` C )
2 coafval.a 
 |-  A = ( Arrow ` C )
3 coafval.x 
 |-  .xb = ( comp ` C )
4 fveq2 
 |-  ( c = C -> ( Arrow ` c ) = ( Arrow ` C ) )
5 4 2 eqtr4di 
 |-  ( c = C -> ( Arrow ` c ) = A )
6 5 rabeqdv 
 |-  ( c = C -> { h e. ( Arrow ` c ) | ( codA ` h ) = ( domA ` g ) } = { h e. A | ( codA ` h ) = ( domA ` g ) } )
7 fveq2 
 |-  ( c = C -> ( comp ` c ) = ( comp ` C ) )
8 7 3 eqtr4di 
 |-  ( c = C -> ( comp ` c ) = .xb )
9 8 oveqd 
 |-  ( c = C -> ( <. ( domA ` f ) , ( domA ` g ) >. ( comp ` c ) ( codA ` g ) ) = ( <. ( domA ` f ) , ( domA ` g ) >. .xb ( codA ` g ) ) )
10 9 oveqd 
 |-  ( c = C -> ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. ( comp ` c ) ( codA ` g ) ) ( 2nd ` f ) ) = ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. .xb ( codA ` g ) ) ( 2nd ` f ) ) )
11 10 oteq3d 
 |-  ( c = C -> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. ( comp ` c ) ( codA ` g ) ) ( 2nd ` f ) ) >. = <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. .xb ( codA ` g ) ) ( 2nd ` f ) ) >. )
12 5 6 11 mpoeq123dv 
 |-  ( c = C -> ( g e. ( Arrow ` c ) , f e. { h e. ( Arrow ` c ) | ( codA ` h ) = ( domA ` g ) } |-> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. ( comp ` c ) ( codA ` g ) ) ( 2nd ` f ) ) >. ) = ( g e. A , f e. { h e. A | ( codA ` h ) = ( domA ` g ) } |-> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. .xb ( codA ` g ) ) ( 2nd ` f ) ) >. ) )
13 df-coa 
 |-  compA = ( c e. Cat |-> ( g e. ( Arrow ` c ) , f e. { h e. ( Arrow ` c ) | ( codA ` h ) = ( domA ` g ) } |-> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. ( comp ` c ) ( codA ` g ) ) ( 2nd ` f ) ) >. ) )
14 2 fvexi 
 |-  A e. _V
15 14 rabex 
 |-  { h e. A | ( codA ` h ) = ( domA ` g ) } e. _V
16 14 15 mpoex 
 |-  ( g e. A , f e. { h e. A | ( codA ` h ) = ( domA ` g ) } |-> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. .xb ( codA ` g ) ) ( 2nd ` f ) ) >. ) e. _V
17 12 13 16 fvmpt 
 |-  ( C e. Cat -> ( compA ` C ) = ( g e. A , f e. { h e. A | ( codA ` h ) = ( domA ` g ) } |-> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. .xb ( codA ` g ) ) ( 2nd ` f ) ) >. ) )
18 13 fvmptndm 
 |-  ( -. C e. Cat -> ( compA ` C ) = (/) )
19 2 arwrcl 
 |-  ( f e. A -> C e. Cat )
20 19 con3i 
 |-  ( -. C e. Cat -> -. f e. A )
21 20 eq0rdv 
 |-  ( -. C e. Cat -> A = (/) )
22 eqidd 
 |-  ( -. C e. Cat -> { h e. A | ( codA ` h ) = ( domA ` g ) } = { h e. A | ( codA ` h ) = ( domA ` g ) } )
23 eqidd 
 |-  ( -. C e. Cat -> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. .xb ( codA ` g ) ) ( 2nd ` f ) ) >. = <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. .xb ( codA ` g ) ) ( 2nd ` f ) ) >. )
24 21 22 23 mpoeq123dv 
 |-  ( -. C e. Cat -> ( g e. A , f e. { h e. A | ( codA ` h ) = ( domA ` g ) } |-> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. .xb ( codA ` g ) ) ( 2nd ` f ) ) >. ) = ( g e. (/) , f e. { h e. A | ( codA ` h ) = ( domA ` g ) } |-> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. .xb ( codA ` g ) ) ( 2nd ` f ) ) >. ) )
25 mpo0 
 |-  ( g e. (/) , f e. { h e. A | ( codA ` h ) = ( domA ` g ) } |-> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. .xb ( codA ` g ) ) ( 2nd ` f ) ) >. ) = (/)
26 24 25 eqtrdi 
 |-  ( -. C e. Cat -> ( g e. A , f e. { h e. A | ( codA ` h ) = ( domA ` g ) } |-> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. .xb ( codA ` g ) ) ( 2nd ` f ) ) >. ) = (/) )
27 18 26 eqtr4d 
 |-  ( -. C e. Cat -> ( compA ` C ) = ( g e. A , f e. { h e. A | ( codA ` h ) = ( domA ` g ) } |-> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. .xb ( codA ` g ) ) ( 2nd ` f ) ) >. ) )
28 17 27 pm2.61i 
 |-  ( compA ` C ) = ( g e. A , f e. { h e. A | ( codA ` h ) = ( domA ` g ) } |-> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. .xb ( codA ` g ) ) ( 2nd ` f ) ) >. )
29 1 28 eqtri 
 |-  .x. = ( g e. A , f e. { h e. A | ( codA ` h ) = ( domA ` g ) } |-> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. .xb ( codA ` g ) ) ( 2nd ` f ) ) >. )