Step |
Hyp |
Ref |
Expression |
1 |
|
ussval.1 |
|- B = ( Base ` W ) |
2 |
|
ussval.2 |
|- U = ( UnifSet ` W ) |
3 |
|
oveq2 |
|- ( ( B X. B ) = U. U -> ( U |`t ( B X. B ) ) = ( U |`t U. U ) ) |
4 |
|
id |
|- ( ( B X. B ) = U. U -> ( B X. B ) = U. U ) |
5 |
1
|
fvexi |
|- B e. _V |
6 |
5 5
|
xpex |
|- ( B X. B ) e. _V |
7 |
4 6
|
eqeltrrdi |
|- ( ( B X. B ) = U. U -> U. U e. _V ) |
8 |
|
uniexb |
|- ( U e. _V <-> U. U e. _V ) |
9 |
7 8
|
sylibr |
|- ( ( B X. B ) = U. U -> U e. _V ) |
10 |
|
eqid |
|- U. U = U. U |
11 |
10
|
restid |
|- ( U e. _V -> ( U |`t U. U ) = U ) |
12 |
9 11
|
syl |
|- ( ( B X. B ) = U. U -> ( U |`t U. U ) = U ) |
13 |
3 12
|
eqtr2d |
|- ( ( B X. B ) = U. U -> U = ( U |`t ( B X. B ) ) ) |
14 |
1 2
|
ussval |
|- ( U |`t ( B X. B ) ) = ( UnifSt ` W ) |
15 |
13 14
|
eqtrdi |
|- ( ( B X. B ) = U. U -> U = ( UnifSt ` W ) ) |