Step |
Hyp |
Ref |
Expression |
1 |
|
tuslem.k |
|- K = ( toUnifSp ` U ) |
2 |
|
id |
|- ( U e. ( UnifOn ` X ) -> U e. ( UnifOn ` X ) ) |
3 |
1
|
tususs |
|- ( U e. ( UnifOn ` X ) -> U = ( UnifSt ` K ) ) |
4 |
1
|
tusbas |
|- ( U e. ( UnifOn ` X ) -> X = ( Base ` K ) ) |
5 |
4
|
fveq2d |
|- ( U e. ( UnifOn ` X ) -> ( UnifOn ` X ) = ( UnifOn ` ( Base ` K ) ) ) |
6 |
2 3 5
|
3eltr3d |
|- ( U e. ( UnifOn ` X ) -> ( UnifSt ` K ) e. ( UnifOn ` ( Base ` K ) ) ) |
7 |
1
|
tusunif |
|- ( U e. ( UnifOn ` X ) -> U = ( UnifSet ` K ) ) |
8 |
7
|
fveq2d |
|- ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) = ( unifTop ` ( UnifSet ` K ) ) ) |
9 |
1
|
tuslem |
|- ( U e. ( UnifOn ` X ) -> ( X = ( Base ` K ) /\ U = ( UnifSet ` K ) /\ ( unifTop ` U ) = ( TopOpen ` K ) ) ) |
10 |
9
|
simp3d |
|- ( U e. ( UnifOn ` X ) -> ( unifTop ` U ) = ( TopOpen ` K ) ) |
11 |
7 3
|
eqtr3d |
|- ( U e. ( UnifOn ` X ) -> ( UnifSet ` K ) = ( UnifSt ` K ) ) |
12 |
11
|
fveq2d |
|- ( U e. ( UnifOn ` X ) -> ( unifTop ` ( UnifSet ` K ) ) = ( unifTop ` ( UnifSt ` K ) ) ) |
13 |
8 10 12
|
3eqtr3d |
|- ( U e. ( UnifOn ` X ) -> ( TopOpen ` K ) = ( unifTop ` ( UnifSt ` K ) ) ) |
14 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
15 |
|
eqid |
|- ( UnifSt ` K ) = ( UnifSt ` K ) |
16 |
|
eqid |
|- ( TopOpen ` K ) = ( TopOpen ` K ) |
17 |
14 15 16
|
isusp |
|- ( K e. UnifSp <-> ( ( UnifSt ` K ) e. ( UnifOn ` ( Base ` K ) ) /\ ( TopOpen ` K ) = ( unifTop ` ( UnifSt ` K ) ) ) ) |
18 |
6 13 17
|
sylanbrc |
|- ( U e. ( UnifOn ` X ) -> K e. UnifSp ) |