Metamath Proof Explorer

Theorem xpcpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same product category. (Contributed by Mario Carneiro, 17-Jan-2017)

Ref Expression
Hypotheses xpcpropd.1 
|- ( ph -> ( Homf ` A ) = ( Homf ` B ) )
xpcpropd.2 
|- ( ph -> ( comf ` A ) = ( comf ` B ) )
xpcpropd.3 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
xpcpropd.4 
|- ( ph -> ( comf ` C ) = ( comf ` D ) )
xpcpropd.a 
|- ( ph -> A e. V )
xpcpropd.b 
|- ( ph -> B e. V )
xpcpropd.c 
|- ( ph -> C e. V )
xpcpropd.d 
|- ( ph -> D e. V )
Assertion xpcpropd 
|- ( ph -> ( A Xc. C ) = ( B Xc. D ) )

Proof

Step Hyp Ref Expression
1 xpcpropd.1 
 |-  ( ph -> ( Homf ` A ) = ( Homf ` B ) )
2 xpcpropd.2 
 |-  ( ph -> ( comf ` A ) = ( comf ` B ) )
3 xpcpropd.3 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
4 xpcpropd.4 
 |-  ( ph -> ( comf ` C ) = ( comf ` D ) )
5 xpcpropd.a 
 |-  ( ph -> A e. V )
6 xpcpropd.b 
 |-  ( ph -> B e. V )
7 xpcpropd.c 
 |-  ( ph -> C e. V )
8 xpcpropd.d 
 |-  ( ph -> D e. V )
9 eqid 
 |-  ( A Xc. C ) = ( A Xc. C )
10 eqid 
 |-  ( Base ` A ) = ( Base ` A )
11 eqid 
 |-  ( Base ` C ) = ( Base ` C )
12 eqid 
 |-  ( Hom ` A ) = ( Hom ` A )
13 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
14 eqid 
 |-  ( comp ` A ) = ( comp ` A )
15 eqid 
 |-  ( comp ` C ) = ( comp ` C )
16 eqidd 
 |-  ( ph -> ( ( Base ` A ) X. ( Base ` C ) ) = ( ( Base ` A ) X. ( Base ` C ) ) )
17 9 10 11 xpcbas 
 |-  ( ( Base ` A ) X. ( Base ` C ) ) = ( Base ` ( A Xc. C ) )
18 eqid 
 |-  ( Hom ` ( A Xc. C ) ) = ( Hom ` ( A Xc. C ) )
19 9 17 12 13 18 xpchomfval 
 |-  ( Hom ` ( A Xc. C ) ) = ( u e. ( ( Base ` A ) X. ( Base ` C ) ) , v e. ( ( Base ` A ) X. ( Base ` C ) ) |-> ( ( ( 1st ` u ) ( Hom ` A ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` C ) ( 2nd ` v ) ) ) )
20 19 a1i 
 |-  ( ph -> ( Hom ` ( A Xc. C ) ) = ( u e. ( ( Base ` A ) X. ( Base ` C ) ) , v e. ( ( Base ` A ) X. ( Base ` C ) ) |-> ( ( ( 1st ` u ) ( Hom ` A ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` C ) ( 2nd ` v ) ) ) ) )
21 eqidd 
 |-  ( ph -> ( x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) , y e. ( ( Base ` A ) X. ( Base ` C ) ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) , f e. ( ( Hom ` ( A Xc. C ) ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` A ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` C ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) = ( x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) , y e. ( ( Base ` A ) X. ( Base ` C ) ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) , f e. ( ( Hom ` ( A Xc. C ) ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` A ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` C ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) )
22 9 10 11 12 13 14 15 5 7 16 20 21 xpcval 
 |-  ( ph -> ( A Xc. C ) = { <. ( Base ` ndx ) , ( ( Base ` A ) X. ( Base ` C ) ) >. , <. ( Hom ` ndx ) , ( Hom ` ( A Xc. C ) ) >. , <. ( comp ` ndx ) , ( x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) , y e. ( ( Base ` A ) X. ( Base ` C ) ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) , f e. ( ( Hom ` ( A Xc. C ) ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` A ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` C ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. } )
23 eqid 
 |-  ( B Xc. D ) = ( B Xc. D )
24 eqid 
 |-  ( Base ` B ) = ( Base ` B )
25 eqid 
 |-  ( Base ` D ) = ( Base ` D )
26 eqid 
 |-  ( Hom ` B ) = ( Hom ` B )
27 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
28 eqid 
 |-  ( comp ` B ) = ( comp ` B )
29 eqid 
 |-  ( comp ` D ) = ( comp ` D )
30 1 homfeqbas 
 |-  ( ph -> ( Base ` A ) = ( Base ` B ) )
31 3 homfeqbas 
 |-  ( ph -> ( Base ` C ) = ( Base ` D ) )
32 30 31 xpeq12d 
 |-  ( ph -> ( ( Base ` A ) X. ( Base ` C ) ) = ( ( Base ` B ) X. ( Base ` D ) ) )
33 1 3ad2ant1 
 |-  ( ( ph /\ u e. ( ( Base ` A ) X. ( Base ` C ) ) /\ v e. ( ( Base ` A ) X. ( Base ` C ) ) ) -> ( Homf ` A ) = ( Homf ` B ) )
34 xp1st 
 |-  ( u e. ( ( Base ` A ) X. ( Base ` C ) ) -> ( 1st ` u ) e. ( Base ` A ) )
35 34 3ad2ant2 
 |-  ( ( ph /\ u e. ( ( Base ` A ) X. ( Base ` C ) ) /\ v e. ( ( Base ` A ) X. ( Base ` C ) ) ) -> ( 1st ` u ) e. ( Base ` A ) )
36 xp1st 
 |-  ( v e. ( ( Base ` A ) X. ( Base ` C ) ) -> ( 1st ` v ) e. ( Base ` A ) )
37 36 3ad2ant3 
 |-  ( ( ph /\ u e. ( ( Base ` A ) X. ( Base ` C ) ) /\ v e. ( ( Base ` A ) X. ( Base ` C ) ) ) -> ( 1st ` v ) e. ( Base ` A ) )
38 10 12 26 33 35 37 homfeqval 
 |-  ( ( ph /\ u e. ( ( Base ` A ) X. ( Base ` C ) ) /\ v e. ( ( Base ` A ) X. ( Base ` C ) ) ) -> ( ( 1st ` u ) ( Hom ` A ) ( 1st ` v ) ) = ( ( 1st ` u ) ( Hom ` B ) ( 1st ` v ) ) )
39 3 3ad2ant1 
 |-  ( ( ph /\ u e. ( ( Base ` A ) X. ( Base ` C ) ) /\ v e. ( ( Base ` A ) X. ( Base ` C ) ) ) -> ( Homf ` C ) = ( Homf ` D ) )
40 xp2nd 
 |-  ( u e. ( ( Base ` A ) X. ( Base ` C ) ) -> ( 2nd ` u ) e. ( Base ` C ) )
41 40 3ad2ant2 
 |-  ( ( ph /\ u e. ( ( Base ` A ) X. ( Base ` C ) ) /\ v e. ( ( Base ` A ) X. ( Base ` C ) ) ) -> ( 2nd ` u ) e. ( Base ` C ) )
42 xp2nd 
 |-  ( v e. ( ( Base ` A ) X. ( Base ` C ) ) -> ( 2nd ` v ) e. ( Base ` C ) )
43 42 3ad2ant3 
 |-  ( ( ph /\ u e. ( ( Base ` A ) X. ( Base ` C ) ) /\ v e. ( ( Base ` A ) X. ( Base ` C ) ) ) -> ( 2nd ` v ) e. ( Base ` C ) )
44 11 13 27 39 41 43 homfeqval 
 |-  ( ( ph /\ u e. ( ( Base ` A ) X. ( Base ` C ) ) /\ v e. ( ( Base ` A ) X. ( Base ` C ) ) ) -> ( ( 2nd ` u ) ( Hom ` C ) ( 2nd ` v ) ) = ( ( 2nd ` u ) ( Hom ` D ) ( 2nd ` v ) ) )
45 38 44 xpeq12d 
 |-  ( ( ph /\ u e. ( ( Base ` A ) X. ( Base ` C ) ) /\ v e. ( ( Base ` A ) X. ( Base ` C ) ) ) -> ( ( ( 1st ` u ) ( Hom ` A ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` C ) ( 2nd ` v ) ) ) = ( ( ( 1st ` u ) ( Hom ` B ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` D ) ( 2nd ` v ) ) ) )
46 45 mpoeq3dva 
 |-  ( ph -> ( u e. ( ( Base ` A ) X. ( Base ` C ) ) , v e. ( ( Base ` A ) X. ( Base ` C ) ) |-> ( ( ( 1st ` u ) ( Hom ` A ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` C ) ( 2nd ` v ) ) ) ) = ( u e. ( ( Base ` A ) X. ( Base ` C ) ) , v e. ( ( Base ` A ) X. ( Base ` C ) ) |-> ( ( ( 1st ` u ) ( Hom ` B ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` D ) ( 2nd ` v ) ) ) ) )
47 19 46 syl5eq 
 |-  ( ph -> ( Hom ` ( A Xc. C ) ) = ( u e. ( ( Base ` A ) X. ( Base ` C ) ) , v e. ( ( Base ` A ) X. ( Base ` C ) ) |-> ( ( ( 1st ` u ) ( Hom ` B ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` D ) ( 2nd ` v ) ) ) ) )
48 1 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> ( Homf ` A ) = ( Homf ` B ) )
49 2 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> ( comf ` A ) = ( comf ` B ) )
50 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) )
51 xp1st 
 |-  ( x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) -> ( 1st ` x ) e. ( ( Base ` A ) X. ( Base ` C ) ) )
52 50 51 syl 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> ( 1st ` x ) e. ( ( Base ` A ) X. ( Base ` C ) ) )
53 xp1st 
 |-  ( ( 1st ` x ) e. ( ( Base ` A ) X. ( Base ` C ) ) -> ( 1st ` ( 1st ` x ) ) e. ( Base ` A ) )
54 52 53 syl 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> ( 1st ` ( 1st ` x ) ) e. ( Base ` A ) )
55 xp2nd 
 |-  ( x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) -> ( 2nd ` x ) e. ( ( Base ` A ) X. ( Base ` C ) ) )
56 50 55 syl 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> ( 2nd ` x ) e. ( ( Base ` A ) X. ( Base ` C ) ) )
57 xp1st 
 |-  ( ( 2nd ` x ) e. ( ( Base ` A ) X. ( Base ` C ) ) -> ( 1st ` ( 2nd ` x ) ) e. ( Base ` A ) )
58 56 57 syl 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> ( 1st ` ( 2nd ` x ) ) e. ( Base ` A ) )
59 simpllr 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> y e. ( ( Base ` A ) X. ( Base ` C ) ) )
60 xp1st 
 |-  ( y e. ( ( Base ` A ) X. ( Base ` C ) ) -> ( 1st ` y ) e. ( Base ` A ) )
61 59 60 syl 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> ( 1st ` y ) e. ( Base ` A ) )
62 simpr 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> f e. ( ( Hom ` ( A Xc. C ) ) ` x ) )
63 1st2nd2 
 |-  ( x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
64 50 63 syl 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
65 64 fveq2d 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> ( ( Hom ` ( A Xc. C ) ) ` x ) = ( ( Hom ` ( A Xc. C ) ) ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
66 df-ov 
 |-  ( ( 1st ` x ) ( Hom ` ( A Xc. C ) ) ( 2nd ` x ) ) = ( ( Hom ` ( A Xc. C ) ) ` <. ( 1st ` x ) , ( 2nd ` x ) >. )
67 65 66 eqtr4di 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> ( ( Hom ` ( A Xc. C ) ) ` x ) = ( ( 1st ` x ) ( Hom ` ( A Xc. C ) ) ( 2nd ` x ) ) )
68 9 17 12 13 18 52 56 xpchom 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> ( ( 1st ` x ) ( Hom ` ( A Xc. C ) ) ( 2nd ` x ) ) = ( ( ( 1st ` ( 1st ` x ) ) ( Hom ` A ) ( 1st ` ( 2nd ` x ) ) ) X. ( ( 2nd ` ( 1st ` x ) ) ( Hom ` C ) ( 2nd ` ( 2nd ` x ) ) ) ) )
69 67 68 eqtrd 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> ( ( Hom ` ( A Xc. C ) ) ` x ) = ( ( ( 1st ` ( 1st ` x ) ) ( Hom ` A ) ( 1st ` ( 2nd ` x ) ) ) X. ( ( 2nd ` ( 1st ` x ) ) ( Hom ` C ) ( 2nd ` ( 2nd ` x ) ) ) ) )
70 62 69 eleqtrd 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> f e. ( ( ( 1st ` ( 1st ` x ) ) ( Hom ` A ) ( 1st ` ( 2nd ` x ) ) ) X. ( ( 2nd ` ( 1st ` x ) ) ( Hom ` C ) ( 2nd ` ( 2nd ` x ) ) ) ) )
71 xp1st 
 |-  ( f e. ( ( ( 1st ` ( 1st ` x ) ) ( Hom ` A ) ( 1st ` ( 2nd ` x ) ) ) X. ( ( 2nd ` ( 1st ` x ) ) ( Hom ` C ) ( 2nd ` ( 2nd ` x ) ) ) ) -> ( 1st ` f ) e. ( ( 1st ` ( 1st ` x ) ) ( Hom ` A ) ( 1st ` ( 2nd ` x ) ) ) )
72 70 71 syl 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> ( 1st ` f ) e. ( ( 1st ` ( 1st ` x ) ) ( Hom ` A ) ( 1st ` ( 2nd ` x ) ) ) )
73 simplr 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) )
74 9 17 12 13 18 56 59 xpchom 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) = ( ( ( 1st ` ( 2nd ` x ) ) ( Hom ` A ) ( 1st ` y ) ) X. ( ( 2nd ` ( 2nd ` x ) ) ( Hom ` C ) ( 2nd ` y ) ) ) )
75 73 74 eleqtrd 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> g e. ( ( ( 1st ` ( 2nd ` x ) ) ( Hom ` A ) ( 1st ` y ) ) X. ( ( 2nd ` ( 2nd ` x ) ) ( Hom ` C ) ( 2nd ` y ) ) ) )
76 xp1st 
 |-  ( g e. ( ( ( 1st ` ( 2nd ` x ) ) ( Hom ` A ) ( 1st ` y ) ) X. ( ( 2nd ` ( 2nd ` x ) ) ( Hom ` C ) ( 2nd ` y ) ) ) -> ( 1st ` g ) e. ( ( 1st ` ( 2nd ` x ) ) ( Hom ` A ) ( 1st ` y ) ) )
77 75 76 syl 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> ( 1st ` g ) e. ( ( 1st ` ( 2nd ` x ) ) ( Hom ` A ) ( 1st ` y ) ) )
78 10 12 14 28 48 49 54 58 61 72 77 comfeqval 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` A ) ( 1st ` y ) ) ( 1st ` f ) ) = ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` B ) ( 1st ` y ) ) ( 1st ` f ) ) )
79 3 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> ( Homf ` C ) = ( Homf ` D ) )
80 4 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> ( comf ` C ) = ( comf ` D ) )
81 xp2nd 
 |-  ( ( 1st ` x ) e. ( ( Base ` A ) X. ( Base ` C ) ) -> ( 2nd ` ( 1st ` x ) ) e. ( Base ` C ) )
82 52 81 syl 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> ( 2nd ` ( 1st ` x ) ) e. ( Base ` C ) )
83 xp2nd 
 |-  ( ( 2nd ` x ) e. ( ( Base ` A ) X. ( Base ` C ) ) -> ( 2nd ` ( 2nd ` x ) ) e. ( Base ` C ) )
84 56 83 syl 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> ( 2nd ` ( 2nd ` x ) ) e. ( Base ` C ) )
85 xp2nd 
 |-  ( y e. ( ( Base ` A ) X. ( Base ` C ) ) -> ( 2nd ` y ) e. ( Base ` C ) )
86 59 85 syl 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> ( 2nd ` y ) e. ( Base ` C ) )
87 xp2nd 
 |-  ( f e. ( ( ( 1st ` ( 1st ` x ) ) ( Hom ` A ) ( 1st ` ( 2nd ` x ) ) ) X. ( ( 2nd ` ( 1st ` x ) ) ( Hom ` C ) ( 2nd ` ( 2nd ` x ) ) ) ) -> ( 2nd ` f ) e. ( ( 2nd ` ( 1st ` x ) ) ( Hom ` C ) ( 2nd ` ( 2nd ` x ) ) ) )
88 70 87 syl 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> ( 2nd ` f ) e. ( ( 2nd ` ( 1st ` x ) ) ( Hom ` C ) ( 2nd ` ( 2nd ` x ) ) ) )
89 xp2nd 
 |-  ( g e. ( ( ( 1st ` ( 2nd ` x ) ) ( Hom ` A ) ( 1st ` y ) ) X. ( ( 2nd ` ( 2nd ` x ) ) ( Hom ` C ) ( 2nd ` y ) ) ) -> ( 2nd ` g ) e. ( ( 2nd ` ( 2nd ` x ) ) ( Hom ` C ) ( 2nd ` y ) ) )
90 75 89 syl 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> ( 2nd ` g ) e. ( ( 2nd ` ( 2nd ` x ) ) ( Hom ` C ) ( 2nd ` y ) ) )
91 11 13 15 29 79 80 82 84 86 88 90 comfeqval 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` C ) ( 2nd ` y ) ) ( 2nd ` f ) ) = ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` D ) ( 2nd ` y ) ) ( 2nd ` f ) ) )
92 78 91 opeq12d 
 |-  ( ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` A ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` C ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. = <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` B ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` D ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. )
93 92 3impa 
 |-  ( ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) /\ f e. ( ( Hom ` ( A Xc. C ) ) ` x ) ) -> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` A ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` C ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. = <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` B ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` D ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. )
94 93 mpoeq3dva 
 |-  ( ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) -> ( g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) , f e. ( ( Hom ` ( A Xc. C ) ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` A ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` C ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) = ( g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) , f e. ( ( Hom ` ( A Xc. C ) ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` B ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` D ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) )
95 94 3impa 
 |-  ( ( ph /\ x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) /\ y e. ( ( Base ` A ) X. ( Base ` C ) ) ) -> ( g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) , f e. ( ( Hom ` ( A Xc. C ) ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` A ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` C ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) = ( g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) , f e. ( ( Hom ` ( A Xc. C ) ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` B ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` D ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) )
96 95 mpoeq3dva 
 |-  ( ph -> ( x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) , y e. ( ( Base ` A ) X. ( Base ` C ) ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) , f e. ( ( Hom ` ( A Xc. C ) ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` A ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` C ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) = ( x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) , y e. ( ( Base ` A ) X. ( Base ` C ) ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) , f e. ( ( Hom ` ( A Xc. C ) ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` B ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` D ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) )
97 23 24 25 26 27 28 29 6 8 32 47 96 xpcval 
 |-  ( ph -> ( B Xc. D ) = { <. ( Base ` ndx ) , ( ( Base ` A ) X. ( Base ` C ) ) >. , <. ( Hom ` ndx ) , ( Hom ` ( A Xc. C ) ) >. , <. ( comp ` ndx ) , ( x e. ( ( ( Base ` A ) X. ( Base ` C ) ) X. ( ( Base ` A ) X. ( Base ` C ) ) ) , y e. ( ( Base ` A ) X. ( Base ` C ) ) |-> ( g e. ( ( 2nd ` x ) ( Hom ` ( A Xc. C ) ) y ) , f e. ( ( Hom ` ( A Xc. C ) ) ` x ) |-> <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` A ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` C ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. } )
98 22 97 eqtr4d 
 |-  ( ph -> ( A Xc. C ) = ( B Xc. D ) )