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 𝑋 = 𝐽
Assertion isopn3 ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( 𝑆𝐽 ↔ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ) )

Proof

Step Hyp Ref Expression
1 clscld.1 𝑋 = 𝐽
2 1 ntrval ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ( 𝐽 ∩ 𝒫 𝑆 ) )
3 inss2 ( 𝐽 ∩ 𝒫 𝑆 ) ⊆ 𝒫 𝑆
4 3 unissi ( 𝐽 ∩ 𝒫 𝑆 ) ⊆ 𝒫 𝑆
5 unipw 𝒫 𝑆 = 𝑆
6 4 5 sseqtri ( 𝐽 ∩ 𝒫 𝑆 ) ⊆ 𝑆
7 6 a1i ( 𝑆𝐽 ( 𝐽 ∩ 𝒫 𝑆 ) ⊆ 𝑆 )
8 id ( 𝑆𝐽𝑆𝐽 )
9 pwidg ( 𝑆𝐽𝑆 ∈ 𝒫 𝑆 )
10 8 9 elind ( 𝑆𝐽𝑆 ∈ ( 𝐽 ∩ 𝒫 𝑆 ) )
11 elssuni ( 𝑆 ∈ ( 𝐽 ∩ 𝒫 𝑆 ) → 𝑆 ( 𝐽 ∩ 𝒫 𝑆 ) )
12 10 11 syl ( 𝑆𝐽𝑆 ( 𝐽 ∩ 𝒫 𝑆 ) )
13 7 12 eqssd ( 𝑆𝐽 ( 𝐽 ∩ 𝒫 𝑆 ) = 𝑆 )
14 2 13 sylan9eq ( ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) ∧ 𝑆𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 )
15 14 ex ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( 𝑆𝐽 → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ) )
16 1 ntropn ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ∈ 𝐽 )
17 eleq1 ( ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 → ( ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ∈ 𝐽𝑆𝐽 ) )
18 16 17 syl5ibcom ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆𝑆𝐽 ) )
19 15 18 impbid ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( 𝑆𝐽 ↔ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ) )