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 ⊢ 𝑋 = ∪ 𝐽
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 ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ) )