Step |
Hyp |
Ref |
Expression |
1 |
|
clscld.1 |
|- X = U. J |
2 |
1
|
ntropn |
|- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) e. J ) |
3 |
1
|
ntrss3 |
|- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) C_ X ) |
4 |
1
|
isopn3 |
|- ( ( J e. Top /\ ( ( int ` J ) ` S ) C_ X ) -> ( ( ( int ` J ) ` S ) e. J <-> ( ( int ` J ) ` ( ( int ` J ) ` S ) ) = ( ( int ` J ) ` S ) ) ) |
5 |
3 4
|
syldan |
|- ( ( J e. Top /\ S C_ X ) -> ( ( ( int ` J ) ` S ) e. J <-> ( ( int ` J ) ` ( ( int ` J ) ` S ) ) = ( ( int ` J ) ` S ) ) ) |
6 |
2 5
|
mpbid |
|- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` ( ( int ` J ) ` S ) ) = ( ( int ` J ) ` S ) ) |