Metamath Proof Explorer

Theorem xpchomfval

Description: Set of morphisms of the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017) (Proof shortened by AV, 1-Mar-2024)

Ref Expression
Hypotheses xpchomfval.t 
|- T = ( C Xc. D )
xpchomfval.y 
|- B = ( Base ` T )
xpchomfval.h 
|- H = ( Hom ` C )
xpchomfval.j 
|- J = ( Hom ` D )
xpchomfval.k 
|- K = ( Hom ` T )
Assertion xpchomfval 
|- K = ( u e. B , v e. B |-> ( ( ( 1st ` u ) H ( 1st ` v ) ) X. ( ( 2nd ` u ) J ( 2nd ` v ) ) ) )

Proof

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