Metamath Proof Explorer

Theorem xpcbas

Description: Set of objects of the binary product of categories. (Contributed by Mario Carneiro, 10-Jan-2017)

Ref Expression
Hypotheses xpcbas.t 
|- T = ( C Xc. D )
xpcbas.x 
|- X = ( Base ` C )
xpcbas.y 
|- Y = ( Base ` D )
Assertion xpcbas 
|- ( X X. Y ) = ( Base ` T )

Proof

Step Hyp Ref Expression
1 xpcbas.t 
 |-  T = ( C Xc. D )
2 xpcbas.x 
 |-  X = ( Base ` C )
3 xpcbas.y 
 |-  Y = ( Base ` D )
4 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
5 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
6 eqid 
 |-  ( comp ` C ) = ( comp ` C )
7 eqid 
 |-  ( comp ` D ) = ( comp ` D )
8 simpl 
 |-  ( ( C e. _V /\ D e. _V ) -> C e. _V )
9 simpr 
 |-  ( ( C e. _V /\ D e. _V ) -> D e. _V )
10 eqidd 
 |-  ( ( C e. _V /\ D e. _V ) -> ( X X. Y ) = ( X X. Y ) )
11 eqidd 
 |-  ( ( C e. _V /\ D e. _V ) -> ( u e. ( X X. Y ) , v e. ( X X. Y ) |-> ( ( ( 1st ` u ) ( Hom ` C ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` D ) ( 2nd ` v ) ) ) ) = ( u e. ( X X. Y ) , v e. ( X X. Y ) |-> ( ( ( 1st ` u ) ( Hom ` C ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` D ) ( 2nd ` v ) ) ) ) )
12 eqidd 
 |-  ( ( C e. _V /\ D e. _V ) -> ( x e. ( ( X X. Y ) X. ( X X. Y ) ) , y e. ( X X. Y ) |-> ( g e. ( ( 2nd ` x ) ( u e. ( X X. Y ) , v e. ( X X. Y ) |-> ( ( ( 1st ` u ) ( Hom ` C ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` D ) ( 2nd ` v ) ) ) ) y ) , f e. ( ( u e. ( X X. Y ) , v e. ( X X. Y ) |-> ( ( ( 1st ` u ) ( Hom ` C ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` D ) ( 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. ( ( X X. Y ) X. ( X X. Y ) ) , y e. ( X X. Y ) |-> ( g e. ( ( 2nd ` x ) ( u e. ( X X. Y ) , v e. ( X X. Y ) |-> ( ( ( 1st ` u ) ( Hom ` C ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` D ) ( 2nd ` v ) ) ) ) y ) , f e. ( ( u e. ( X X. Y ) , v e. ( X X. Y ) |-> ( ( ( 1st ` u ) ( Hom ` C ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` D ) ( 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 ) ) >. ) ) )
13 1 2 3 4 5 6 7 8 9 10 11 12 xpcval 
 |-  ( ( C e. _V /\ D e. _V ) -> T = { <. ( Base ` ndx ) , ( X X. Y ) >. , <. ( Hom ` ndx ) , ( u e. ( X X. Y ) , v e. ( X X. Y ) |-> ( ( ( 1st ` u ) ( Hom ` C ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` D ) ( 2nd ` v ) ) ) ) >. , <. ( comp ` ndx ) , ( x e. ( ( X X. Y ) X. ( X X. Y ) ) , y e. ( X X. Y ) |-> ( g e. ( ( 2nd ` x ) ( u e. ( X X. Y ) , v e. ( X X. Y ) |-> ( ( ( 1st ` u ) ( Hom ` C ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` D ) ( 2nd ` v ) ) ) ) y ) , f e. ( ( u e. ( X X. Y ) , v e. ( X X. Y ) |-> ( ( ( 1st ` u ) ( Hom ` C ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` D ) ( 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 ) ) >. ) ) >. } )
14 2 fvexi 
 |-  X e. _V
15 3 fvexi 
 |-  Y e. _V
16 14 15 xpex 
 |-  ( X X. Y ) e. _V
17 16 a1i 
 |-  ( ( C e. _V /\ D e. _V ) -> ( X X. Y ) e. _V )
18 13 17 estrreslem1 
 |-  ( ( C e. _V /\ D e. _V ) -> ( X X. Y ) = ( Base ` T ) )
19 base0 
 |-  (/) = ( Base ` (/) )
20 fvprc 
 |-  ( -. C e. _V -> ( Base ` C ) = (/) )
21 2 20 eqtrid 
 |-  ( -. C e. _V -> X = (/) )
22 fvprc 
 |-  ( -. D e. _V -> ( Base ` D ) = (/) )
23 3 22 eqtrid 
 |-  ( -. D e. _V -> Y = (/) )
24 21 23 orim12i 
 |-  ( ( -. C e. _V \/ -. D e. _V ) -> ( X = (/) \/ Y = (/) ) )
25 ianor 
 |-  ( -. ( C e. _V /\ D e. _V ) <-> ( -. C e. _V \/ -. D e. _V ) )
26 xpeq0 
 |-  ( ( X X. Y ) = (/) <-> ( X = (/) \/ Y = (/) ) )
27 24 25 26 3imtr4i 
 |-  ( -. ( C e. _V /\ D e. _V ) -> ( X X. Y ) = (/) )
28 fnxpc 
 |-  Xc. Fn ( _V X. _V )
29 fndm 
 |-  ( Xc. Fn ( _V X. _V ) -> dom Xc. = ( _V X. _V ) )
30 28 29 ax-mp 
 |-  dom Xc. = ( _V X. _V )
31 30 ndmov 
 |-  ( -. ( C e. _V /\ D e. _V ) -> ( C Xc. D ) = (/) )
32 1 31 eqtrid 
 |-  ( -. ( C e. _V /\ D e. _V ) -> T = (/) )
33 32 fveq2d 
 |-  ( -. ( C e. _V /\ D e. _V ) -> ( Base ` T ) = ( Base ` (/) ) )
34 19 27 33 3eqtr4a 
 |-  ( -. ( C e. _V /\ D e. _V ) -> ( X X. Y ) = ( Base ` T ) )
35 18 34 pm2.61i 
 |-  ( X X. Y ) = ( Base ` T )