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
|
syl5eq |
|- ( -. C e. _V -> X = (/) ) |
22 |
|
fvprc |
|- ( -. D e. _V -> ( Base ` D ) = (/) ) |
23 |
3 22
|
syl5eq |
|- ( -. 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
|
syl5eq |
|- ( -. ( 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 ) |