Metamath Proof Explorer


Theorem isopn3i

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 )

Proof

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 )