Metamath Proof Explorer

Theorem xpcval

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

Ref Expression
Hypotheses xpcval.t 
|- T = ( C Xc. D )
xpcval.x 
|- X = ( Base ` C )
xpcval.y 
|- Y = ( Base ` D )
xpcval.h 
|- H = ( Hom ` C )
xpcval.j 
|- J = ( Hom ` D )
xpcval.o1 
|- .x. = ( comp ` C )
xpcval.o2 
|- .xb = ( comp ` D )
xpcval.c 
|- ( ph -> C e. V )
xpcval.d 
|- ( ph -> D e. W )
xpcval.b 
|- ( ph -> B = ( X X. Y ) )
xpcval.k 
|- ( ph -> K = ( u e. B , v e. B |-> ( ( ( 1st ` u ) H ( 1st ` v ) ) X. ( ( 2nd ` u ) J ( 2nd ` v ) ) ) ) )
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 ) ) >. ) ) )
Assertion xpcval 
|- ( ph -> T = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , K >. , <. ( comp ` ndx ) , O >. } )

Proof

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 df-xpc 
 |-  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 >. } )