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 )