This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )