Step 
Hyp 
Ref 
Expression 
1 

xpcval.t 
 T = ( C Xc. D ) 
2 

xpcval.x 
 X = ( Base ` C ) 
3 

xpcval.y 
 Y = ( Base ` D ) 
4 

xpcval.h 
 H = ( Hom ` C ) 
5 

xpcval.j 
 J = ( Hom ` D ) 
6 

xpcval.o1 
 .x. = ( comp ` C ) 
7 

xpcval.o2 
 .xb = ( comp ` D ) 
8 

xpcval.c 
 ( ph > C e. V ) 
9 

xpcval.d 
 ( ph > D e. W ) 
10 

xpcval.b 
 ( ph > B = ( X X. Y ) ) 
11 

xpcval.k 
 ( ph > K = ( u e. B , v e. B > ( ( ( 1st ` u ) H ( 1st ` v ) ) X. ( ( 2nd ` u ) J ( 2nd ` v ) ) ) ) ) 
12 

xpcval.o 
 ( ph > 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 ) ) >. ) ) ) 
13 

dfxpc 
 Xc. = ( r e. _V , s e. _V > [_ ( ( Base ` r ) X. ( Base ` s ) ) / b ]_ [_ ( u e. b , v e. b > ( ( ( 1st ` u ) ( Hom ` r ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` s ) ( 2nd ` v ) ) ) ) / h ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , h >. , <. ( comp ` ndx ) , ( x e. ( b X. b ) , y e. b > ( g e. ( ( 2nd ` x ) h y ) , f e. ( h ` x ) > <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` r ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` s ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. } ) 
14 
13

a1i 
 ( ph > Xc. = ( r e. _V , s e. _V > [_ ( ( Base ` r ) X. ( Base ` s ) ) / b ]_ [_ ( u e. b , v e. b > ( ( ( 1st ` u ) ( Hom ` r ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` s ) ( 2nd ` v ) ) ) ) / h ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , h >. , <. ( comp ` ndx ) , ( x e. ( b X. b ) , y e. b > ( g e. ( ( 2nd ` x ) h y ) , f e. ( h ` x ) > <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` r ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` s ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. } ) ) 
15 

fvex 
 ( Base ` r ) e. _V 
16 

fvex 
 ( Base ` s ) e. _V 
17 
15 16

xpex 
 ( ( Base ` r ) X. ( Base ` s ) ) e. _V 
18 
17

a1i 
 ( ( ph /\ ( r = C /\ s = D ) ) > ( ( Base ` r ) X. ( Base ` s ) ) e. _V ) 
19 

simprl 
 ( ( ph /\ ( r = C /\ s = D ) ) > r = C ) 
20 
19

fveq2d 
 ( ( ph /\ ( r = C /\ s = D ) ) > ( Base ` r ) = ( Base ` C ) ) 
21 
20 2

eqtr4di 
 ( ( ph /\ ( r = C /\ s = D ) ) > ( Base ` r ) = X ) 
22 

simprr 
 ( ( ph /\ ( r = C /\ s = D ) ) > s = D ) 
23 
22

fveq2d 
 ( ( ph /\ ( r = C /\ s = D ) ) > ( Base ` s ) = ( Base ` D ) ) 
24 
23 3

eqtr4di 
 ( ( ph /\ ( r = C /\ s = D ) ) > ( Base ` s ) = Y ) 
25 
21 24

xpeq12d 
 ( ( ph /\ ( r = C /\ s = D ) ) > ( ( Base ` r ) X. ( Base ` s ) ) = ( X X. Y ) ) 
26 
10

adantr 
 ( ( ph /\ ( r = C /\ s = D ) ) > B = ( X X. Y ) ) 
27 
25 26

eqtr4d 
 ( ( ph /\ ( r = C /\ s = D ) ) > ( ( Base ` r ) X. ( Base ` s ) ) = B ) 
28 

vex 
 b e. _V 
29 
28 28

mpoex 
 ( u e. b , v e. b > ( ( ( 1st ` u ) ( Hom ` r ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` s ) ( 2nd ` v ) ) ) ) e. _V 
30 
29

a1i 
 ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) > ( u e. b , v e. b > ( ( ( 1st ` u ) ( Hom ` r ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` s ) ( 2nd ` v ) ) ) ) e. _V ) 
31 

simpr 
 ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) > b = B ) 
32 

simplrl 
 ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) > r = C ) 
33 
32

fveq2d 
 ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) > ( Hom ` r ) = ( Hom ` C ) ) 
34 
33 4

eqtr4di 
 ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) > ( Hom ` r ) = H ) 
35 
34

oveqd 
 ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) > ( ( 1st ` u ) ( Hom ` r ) ( 1st ` v ) ) = ( ( 1st ` u ) H ( 1st ` v ) ) ) 
36 

simplrr 
 ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) > s = D ) 
37 
36

fveq2d 
 ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) > ( Hom ` s ) = ( Hom ` D ) ) 
38 
37 5

eqtr4di 
 ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) > ( Hom ` s ) = J ) 
39 
38

oveqd 
 ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) > ( ( 2nd ` u ) ( Hom ` s ) ( 2nd ` v ) ) = ( ( 2nd ` u ) J ( 2nd ` v ) ) ) 
40 
35 39

xpeq12d 
 ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) > ( ( ( 1st ` u ) ( Hom ` r ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` s ) ( 2nd ` v ) ) ) = ( ( ( 1st ` u ) H ( 1st ` v ) ) X. ( ( 2nd ` u ) J ( 2nd ` v ) ) ) ) 
41 
31 31 40

mpoeq123dv 
 ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) > ( u e. b , v e. b > ( ( ( 1st ` u ) ( Hom ` r ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` s ) ( 2nd ` v ) ) ) ) = ( u e. B , v e. B > ( ( ( 1st ` u ) H ( 1st ` v ) ) X. ( ( 2nd ` u ) J ( 2nd ` v ) ) ) ) ) 
42 
11

ad2antrr 
 ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) > K = ( u e. B , v e. B > ( ( ( 1st ` u ) H ( 1st ` v ) ) X. ( ( 2nd ` u ) J ( 2nd ` v ) ) ) ) ) 
43 
41 42

eqtr4d 
 ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) > ( u e. b , v e. b > ( ( ( 1st ` u ) ( Hom ` r ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` s ) ( 2nd ` v ) ) ) ) = K ) 
44 

simplr 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > b = B ) 
45 
44

opeq2d 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > <. ( Base ` ndx ) , b >. = <. ( Base ` ndx ) , B >. ) 
46 

simpr 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > h = K ) 
47 
46

opeq2d 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > <. ( Hom ` ndx ) , h >. = <. ( Hom ` ndx ) , K >. ) 
48 
44 44

xpeq12d 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > ( b X. b ) = ( B X. B ) ) 
49 
46

oveqd 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > ( ( 2nd ` x ) h y ) = ( ( 2nd ` x ) K y ) ) 
50 
46

fveq1d 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > ( h ` x ) = ( K ` x ) ) 
51 
32

adantr 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > r = C ) 
52 
51

fveq2d 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > ( comp ` r ) = ( comp ` C ) ) 
53 
52 6

eqtr4di 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > ( comp ` r ) = .x. ) 
54 
53

oveqd 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` r ) ( 1st ` y ) ) = ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ) 
55 
54

oveqd 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` r ) ( 1st ` y ) ) ( 1st ` f ) ) = ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. .x. ( 1st ` y ) ) ( 1st ` f ) ) ) 
56 
36

adantr 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > s = D ) 
57 
56

fveq2d 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > ( comp ` s ) = ( comp ` D ) ) 
58 
57 7

eqtr4di 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > ( comp ` s ) = .xb ) 
59 
58

oveqd 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` s ) ( 2nd ` y ) ) = ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ) 
60 
59

oveqd 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` s ) ( 2nd ` y ) ) ( 2nd ` f ) ) = ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. .xb ( 2nd ` y ) ) ( 2nd ` f ) ) ) 
61 
55 60

opeq12d 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` r ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` s ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. = <. ( ( 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 ) ) >. ) 
62 
49 50 61

mpoeq123dv 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > ( g e. ( ( 2nd ` x ) h y ) , f e. ( h ` x ) > <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` r ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` s ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) = ( 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 ) ) >. ) ) 
63 
48 44 62

mpoeq123dv 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > ( x e. ( b X. b ) , y e. b > ( g e. ( ( 2nd ` x ) h y ) , f e. ( h ` x ) > <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` r ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` s ) ( 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 ) ) >. ) ) ) 
64 
12

ad3antrrr 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > 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 ) ) >. ) ) ) 
65 
63 64

eqtr4d 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > ( x e. ( b X. b ) , y e. b > ( g e. ( ( 2nd ` x ) h y ) , f e. ( h ` x ) > <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` r ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` s ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) = O ) 
66 
65

opeq2d 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > <. ( comp ` ndx ) , ( x e. ( b X. b ) , y e. b > ( g e. ( ( 2nd ` x ) h y ) , f e. ( h ` x ) > <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` r ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` s ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. = <. ( comp ` ndx ) , O >. ) 
67 
45 47 66

tpeq123d 
 ( ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) /\ h = K ) > { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , h >. , <. ( comp ` ndx ) , ( x e. ( b X. b ) , y e. b > ( g e. ( ( 2nd ` x ) h y ) , f e. ( h ` x ) > <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` r ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` s ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. } = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , K >. , <. ( comp ` ndx ) , O >. } ) 
68 
30 43 67

csbied2 
 ( ( ( ph /\ ( r = C /\ s = D ) ) /\ b = B ) > [_ ( u e. b , v e. b > ( ( ( 1st ` u ) ( Hom ` r ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` s ) ( 2nd ` v ) ) ) ) / h ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , h >. , <. ( comp ` ndx ) , ( x e. ( b X. b ) , y e. b > ( g e. ( ( 2nd ` x ) h y ) , f e. ( h ` x ) > <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` r ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` s ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. } = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , K >. , <. ( comp ` ndx ) , O >. } ) 
69 
18 27 68

csbied2 
 ( ( ph /\ ( r = C /\ s = D ) ) > [_ ( ( Base ` r ) X. ( Base ` s ) ) / b ]_ [_ ( u e. b , v e. b > ( ( ( 1st ` u ) ( Hom ` r ) ( 1st ` v ) ) X. ( ( 2nd ` u ) ( Hom ` s ) ( 2nd ` v ) ) ) ) / h ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , h >. , <. ( comp ` ndx ) , ( x e. ( b X. b ) , y e. b > ( g e. ( ( 2nd ` x ) h y ) , f e. ( h ` x ) > <. ( ( 1st ` g ) ( <. ( 1st ` ( 1st ` x ) ) , ( 1st ` ( 2nd ` x ) ) >. ( comp ` r ) ( 1st ` y ) ) ( 1st ` f ) ) , ( ( 2nd ` g ) ( <. ( 2nd ` ( 1st ` x ) ) , ( 2nd ` ( 2nd ` x ) ) >. ( comp ` s ) ( 2nd ` y ) ) ( 2nd ` f ) ) >. ) ) >. } = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , K >. , <. ( comp ` ndx ) , O >. } ) 
70 
8

elexd 
 ( ph > C e. _V ) 
71 
9

elexd 
 ( ph > D e. _V ) 
72 

tpex 
 { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , K >. , <. ( comp ` ndx ) , O >. } e. _V 
73 
72

a1i 
 ( ph > { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , K >. , <. ( comp ` ndx ) , O >. } e. _V ) 
74 
14 69 70 71 73

ovmpod 
 ( ph > ( C Xc. D ) = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , K >. , <. ( comp ` ndx ) , O >. } ) 
75 
1 74

syl5eq 
 ( ph > T = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , K >. , <. ( comp ` ndx ) , O >. } ) 