Step |
Hyp |
Ref |
Expression |
1 |
|
df-tus |
|- toUnifSp = ( u e. U. ran UnifOn |-> ( { <. ( Base ` ndx ) , dom U. u >. , <. ( UnifSet ` ndx ) , u >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` u ) >. ) ) |
2 |
|
simpr |
|- ( ( U e. ( UnifOn ` X ) /\ u = U ) -> u = U ) |
3 |
2
|
unieqd |
|- ( ( U e. ( UnifOn ` X ) /\ u = U ) -> U. u = U. U ) |
4 |
3
|
dmeqd |
|- ( ( U e. ( UnifOn ` X ) /\ u = U ) -> dom U. u = dom U. U ) |
5 |
4
|
opeq2d |
|- ( ( U e. ( UnifOn ` X ) /\ u = U ) -> <. ( Base ` ndx ) , dom U. u >. = <. ( Base ` ndx ) , dom U. U >. ) |
6 |
2
|
opeq2d |
|- ( ( U e. ( UnifOn ` X ) /\ u = U ) -> <. ( UnifSet ` ndx ) , u >. = <. ( UnifSet ` ndx ) , U >. ) |
7 |
5 6
|
preq12d |
|- ( ( U e. ( UnifOn ` X ) /\ u = U ) -> { <. ( Base ` ndx ) , dom U. u >. , <. ( UnifSet ` ndx ) , u >. } = { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } ) |
8 |
2
|
fveq2d |
|- ( ( U e. ( UnifOn ` X ) /\ u = U ) -> ( unifTop ` u ) = ( unifTop ` U ) ) |
9 |
8
|
opeq2d |
|- ( ( U e. ( UnifOn ` X ) /\ u = U ) -> <. ( TopSet ` ndx ) , ( unifTop ` u ) >. = <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) |
10 |
7 9
|
oveq12d |
|- ( ( U e. ( UnifOn ` X ) /\ u = U ) -> ( { <. ( Base ` ndx ) , dom U. u >. , <. ( UnifSet ` ndx ) , u >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` u ) >. ) = ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) ) |
11 |
|
elrnust |
|- ( U e. ( UnifOn ` X ) -> U e. U. ran UnifOn ) |
12 |
|
ovexd |
|- ( U e. ( UnifOn ` X ) -> ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) e. _V ) |
13 |
1 10 11 12
|
fvmptd2 |
|- ( U e. ( UnifOn ` X ) -> ( toUnifSp ` U ) = ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. ( TopSet ` ndx ) , ( unifTop ` U ) >. ) ) |