Theorem isopn3

Description: A subset is open iff it equals its own interior. (Contributed by NM, 9-Oct-2006) (Revised by Mario Carneiro, 11-Nov-2013)

	Ref	Expression
Hypothesis	clscld.1	|- X = U. J
Assertion	isopn3	|- ( ( J e. Top /\ S C_ X ) -> ( S e. J <-> ( ( int ` J ) ` S ) = S ) )

Proof

Step	Hyp	Ref	Expression
1		clscld.1	|- X = U. J
2	1	ntrval	|- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) = U. ( J i^i ~P S ) )
3		inss2	|- ( J i^i ~P S ) C_ ~P S
4	3	unissi	|- U. ( J i^i ~P S ) C_ U. ~P S
5		unipw	|- U. ~P S = S
6	4 5	sseqtri	|- U. ( J i^i ~P S ) C_ S
7	6	a1i	|- ( S e. J -> U. ( J i^i ~P S ) C_ S )
8		id	|- ( S e. J -> S e. J )
9		pwidg	|- ( S e. J -> S e. ~P S )
10	8 9	elind	|- ( S e. J -> S e. ( J i^i ~P S ) )
11		elssuni	|- ( S e. ( J i^i ~P S ) -> S C_ U. ( J i^i ~P S ) )
12	10 11	syl	|- ( S e. J -> S C_ U. ( J i^i ~P S ) )
13	7 12	eqssd	|- ( S e. J -> U. ( J i^i ~P S ) = S )
14	2 13	sylan9eq	|- ( ( ( J e. Top /\ S C_ X ) /\ S e. J ) -> ( ( int ` J ) ` S ) = S )
15	14	ex	|- ( ( J e. Top /\ S C_ X ) -> ( S e. J -> ( ( int ` J ) ` S ) = S ) )
16	1	ntropn	|- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) e. J )
17		eleq1	|- ( ( ( int ` J ) ` S ) = S -> ( ( ( int ` J ) ` S ) e. J <-> S e. J ) )
18	16 17	syl5ibcom	|- ( ( J e. Top /\ S C_ X ) -> ( ( ( int ` J ) ` S ) = S -> S e. J ) )
19	15 18	impbid	|- ( ( J e. Top /\ S C_ X ) -> ( S e. J <-> ( ( int ` J ) ` S ) = S ) )