Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
2 |
|
eqid |
|- ( UnifSet ` W ) = ( UnifSet ` W ) |
3 |
1 2
|
ussval |
|- ( ( UnifSet ` W ) |`t ( ( Base ` W ) X. ( Base ` W ) ) ) = ( UnifSt ` W ) |
4 |
3
|
oveq1i |
|- ( ( ( UnifSet ` W ) |`t ( ( Base ` W ) X. ( Base ` W ) ) ) |`t ( A X. A ) ) = ( ( UnifSt ` W ) |`t ( A X. A ) ) |
5 |
|
fvex |
|- ( UnifSet ` W ) e. _V |
6 |
|
fvex |
|- ( Base ` W ) e. _V |
7 |
6 6
|
xpex |
|- ( ( Base ` W ) X. ( Base ` W ) ) e. _V |
8 |
|
sqxpexg |
|- ( A e. V -> ( A X. A ) e. _V ) |
9 |
|
restco |
|- ( ( ( UnifSet ` W ) e. _V /\ ( ( Base ` W ) X. ( Base ` W ) ) e. _V /\ ( A X. A ) e. _V ) -> ( ( ( UnifSet ` W ) |`t ( ( Base ` W ) X. ( Base ` W ) ) ) |`t ( A X. A ) ) = ( ( UnifSet ` W ) |`t ( ( ( Base ` W ) X. ( Base ` W ) ) i^i ( A X. A ) ) ) ) |
10 |
5 7 8 9
|
mp3an12i |
|- ( A e. V -> ( ( ( UnifSet ` W ) |`t ( ( Base ` W ) X. ( Base ` W ) ) ) |`t ( A X. A ) ) = ( ( UnifSet ` W ) |`t ( ( ( Base ` W ) X. ( Base ` W ) ) i^i ( A X. A ) ) ) ) |
11 |
4 10
|
eqtr3id |
|- ( A e. V -> ( ( UnifSt ` W ) |`t ( A X. A ) ) = ( ( UnifSet ` W ) |`t ( ( ( Base ` W ) X. ( Base ` W ) ) i^i ( A X. A ) ) ) ) |
12 |
|
inxp |
|- ( ( ( Base ` W ) X. ( Base ` W ) ) i^i ( A X. A ) ) = ( ( ( Base ` W ) i^i A ) X. ( ( Base ` W ) i^i A ) ) |
13 |
|
incom |
|- ( A i^i ( Base ` W ) ) = ( ( Base ` W ) i^i A ) |
14 |
|
eqid |
|- ( W |`s A ) = ( W |`s A ) |
15 |
14 1
|
ressbas |
|- ( A e. V -> ( A i^i ( Base ` W ) ) = ( Base ` ( W |`s A ) ) ) |
16 |
13 15
|
eqtr3id |
|- ( A e. V -> ( ( Base ` W ) i^i A ) = ( Base ` ( W |`s A ) ) ) |
17 |
16
|
sqxpeqd |
|- ( A e. V -> ( ( ( Base ` W ) i^i A ) X. ( ( Base ` W ) i^i A ) ) = ( ( Base ` ( W |`s A ) ) X. ( Base ` ( W |`s A ) ) ) ) |
18 |
12 17
|
syl5eq |
|- ( A e. V -> ( ( ( Base ` W ) X. ( Base ` W ) ) i^i ( A X. A ) ) = ( ( Base ` ( W |`s A ) ) X. ( Base ` ( W |`s A ) ) ) ) |
19 |
18
|
oveq2d |
|- ( A e. V -> ( ( UnifSet ` W ) |`t ( ( ( Base ` W ) X. ( Base ` W ) ) i^i ( A X. A ) ) ) = ( ( UnifSet ` W ) |`t ( ( Base ` ( W |`s A ) ) X. ( Base ` ( W |`s A ) ) ) ) ) |
20 |
14 2
|
ressunif |
|- ( A e. V -> ( UnifSet ` W ) = ( UnifSet ` ( W |`s A ) ) ) |
21 |
20
|
oveq1d |
|- ( A e. V -> ( ( UnifSet ` W ) |`t ( ( Base ` ( W |`s A ) ) X. ( Base ` ( W |`s A ) ) ) ) = ( ( UnifSet ` ( W |`s A ) ) |`t ( ( Base ` ( W |`s A ) ) X. ( Base ` ( W |`s A ) ) ) ) ) |
22 |
|
eqid |
|- ( Base ` ( W |`s A ) ) = ( Base ` ( W |`s A ) ) |
23 |
|
eqid |
|- ( UnifSet ` ( W |`s A ) ) = ( UnifSet ` ( W |`s A ) ) |
24 |
22 23
|
ussval |
|- ( ( UnifSet ` ( W |`s A ) ) |`t ( ( Base ` ( W |`s A ) ) X. ( Base ` ( W |`s A ) ) ) ) = ( UnifSt ` ( W |`s A ) ) |
25 |
24
|
a1i |
|- ( A e. V -> ( ( UnifSet ` ( W |`s A ) ) |`t ( ( Base ` ( W |`s A ) ) X. ( Base ` ( W |`s A ) ) ) ) = ( UnifSt ` ( W |`s A ) ) ) |
26 |
19 21 25
|
3eqtrd |
|- ( A e. V -> ( ( UnifSet ` W ) |`t ( ( ( Base ` W ) X. ( Base ` W ) ) i^i ( A X. A ) ) ) = ( UnifSt ` ( W |`s A ) ) ) |
27 |
11 26
|
eqtr2d |
|- ( A e. V -> ( UnifSt ` ( W |`s A ) ) = ( ( UnifSt ` W ) |`t ( A X. A ) ) ) |