Metamath Proof Explorer

Theorem xpccofval

Description: Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017) (Proof shortened by AV, 2-Mar-2024)

Ref Expression
Hypotheses xpccofval.t 
|- T = ( C Xc. D )
xpccofval.b 
|- B = ( Base ` T )
xpccofval.k 
|- K = ( Hom ` T )
xpccofval.o1 
|- .x. = ( comp ` C )
xpccofval.o2 
|- .xb = ( comp ` D )
xpccofval.o 
|- O = ( comp ` T )
Assertion xpccofval 
|- O = ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) K y ) , f e. ( K ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) )

Proof

Step Hyp Ref Expression
1 xpccofval.t 
 |-  T = ( C Xc. D )
2 xpccofval.b 
 |-  B = ( Base ` T )
3 xpccofval.k 
 |-  K = ( Hom ` T )
4 xpccofval.o1 
 |-  .x. = ( comp ` C )
5 xpccofval.o2 
 |-  .xb = ( comp ` D )
6 xpccofval.o 
 |-  O = ( comp ` T )
7 eqid 
 |-  ( Base ` C ) = ( Base ` C )
8 eqid 
 |-  ( Base ` D ) = ( Base ` D )
9 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
10 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
11 simpl 
 |-  ( ( C e. _V /\ D e. _V ) -> C e. _V )
12 simpr 
 |-  ( ( C e. _V /\ D e. _V ) -> D e. _V )
13 1 7 8 xpcbas 
 |-  ( ( Base ` C ) X. ( Base ` D ) ) = ( Base ` T )
14 2 13 eqtr4i 
 |-  B = ( ( Base ` C ) X. ( Base ` D ) )
15 14 a1i 
 |-  ( ( C e. _V /\ D e. _V ) -> B = ( ( Base ` C ) X. ( Base ` D ) ) )
16 1 2 9 10 3 xpchomfval 
 |-  K = ( u e. B , v e. B |-> ( ( ( 1st ` u ) ( Hom ` C ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` D ) ( 2nd ` v ) ) ) )
17 16 a1i 
 |-  ( ( C e. _V /\ D e. _V ) -> K = ( u e. B , v e. B |-> ( ( ( 1st ` u ) ( Hom ` C ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` D ) ( 2nd ` v ) ) ) ) )
18 eqidd 
 |-  ( ( C e. _V /\ D e. _V ) -> ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) K y ) , f e. ( K ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) = ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) K y ) , f e. ( K ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) )
19 1 7 8 9 10 4 5 11 12 15 17 18 xpcval 
 |-  ( ( C e. _V /\ D e. _V ) -> T = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , K >. , <. ( comp ` ndx ) , ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) K y ) , f e. ( K ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. } )
20 catstr 
 |-  { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , K >. , <. ( comp ` ndx ) , ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) K y ) , f e. ( K ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. } Struct <. 1 , ; 1 5 >.
21 ccoid 
 |-  comp = Slot ( comp ` ndx )
22 snsstp3 
 |-  { <. ( comp ` ndx ) , ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) K y ) , f e. ( K ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. } C_ { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , K >. , <. ( comp ` ndx ) , ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) K y ) , f e. ( K ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. }
23 2 fvexi 
 |-  B e. _V
24 23 23 xpex 
 |-  ( B X. B ) e. _V
25 24 23 mpoex 
 |-  ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) K y ) , f e. ( K ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) e. _V
26 25 a1i 
 |-  ( ( C e. _V /\ D e. _V ) -> ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) K y ) , f e. ( K ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) e. _V )
27 19 20 21 22 26 6 strfv3 
 |-  ( ( C e. _V /\ D e. _V ) -> O = ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) K y ) , f e. ( K ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) )
28 fnxpc 
 |-  Xc. Fn ( _V X. _V )
29 28 fndmi 
 |-  dom Xc. = ( _V X. _V )
30 29 ndmov 
 |-  ( -. ( C e. _V /\ D e. _V ) -> ( C Xc. D ) = (/) )
31 1 30 syl5eq 
 |-  ( -. ( C e. _V /\ D e. _V ) -> T = (/) )
32 31 fveq2d 
 |-  ( -. ( C e. _V /\ D e. _V ) -> ( comp ` T ) = ( comp ` (/) ) )
33 21 str0 
 |-  (/) = ( comp ` (/) )
34 32 6 33 3eqtr4g 
 |-  ( -. ( C e. _V /\ D e. _V ) -> O = (/) )
35 31 fveq2d 
 |-  ( -. ( C e. _V /\ D e. _V ) -> ( Base ` T ) = ( Base ` (/) ) )
36 base0 
 |-  (/) = ( Base ` (/) )
37 35 2 36 3eqtr4g 
 |-  ( -. ( C e. _V /\ D e. _V ) -> B = (/) )
38 37 olcd 
 |-  ( -. ( C e. _V /\ D e. _V ) -> ( ( B X. B ) = (/) \/ B = (/) ) )
39 0mpo0 
 |-  ( ( ( B X. B ) = (/) \/ B = (/) ) -> ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) K y ) , f e. ( K ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) = (/) )
40 38 39 syl 
 |-  ( -. ( C e. _V /\ D e. _V ) -> ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) K y ) , f e. ( K ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) = (/) )
41 34 40 eqtr4d 
 |-  ( -. ( C e. _V /\ D e. _V ) -> O = ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) K y ) , f e. ( K ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) )
42 27 41 pm2.61i 
 |-  O = ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) K y ) , f e. ( K ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) )