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