Description: An open subset equals its own interior. (Contributed by Mario Carneiro, 30-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | isopn3i | |- ( ( J e. Top /\ S e. J ) -> ( ( int ` J ) ` S ) = S ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr | |- ( ( J e. Top /\ S e. J ) -> S e. J ) |
|
2 | elssuni | |- ( S e. J -> S C_ U. J ) |
|
3 | eqid | |- U. J = U. J |
|
4 | 3 | isopn3 | |- ( ( J e. Top /\ S C_ U. J ) -> ( S e. J <-> ( ( int ` J ) ` S ) = S ) ) |
5 | 2 4 | sylan2 | |- ( ( J e. Top /\ S e. J ) -> ( S e. J <-> ( ( int ` J ) ` S ) = S ) ) |
6 | 1 5 | mpbid | |- ( ( J e. Top /\ S e. J ) -> ( ( int ` J ) ` S ) = S ) |