Metamath Proof Explorer


Theorem ntropn

Description: The interior of a subset of a topology's underlying set is open. (Contributed by NM, 11-Sep-2006) (Revised by Mario Carneiro, 11-Nov-2013)

Ref Expression
Hypothesis clscld.1 𝑋 = 𝐽
Assertion ntropn ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ∈ 𝐽 )

Proof

Step Hyp Ref Expression
1 clscld.1 𝑋 = 𝐽
2 1 ntrval ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ( 𝐽 ∩ 𝒫 𝑆 ) )
3 inss1 ( 𝐽 ∩ 𝒫 𝑆 ) ⊆ 𝐽
4 uniopn ( ( 𝐽 ∈ Top ∧ ( 𝐽 ∩ 𝒫 𝑆 ) ⊆ 𝐽 ) → ( 𝐽 ∩ 𝒫 𝑆 ) ∈ 𝐽 )
5 3 4 mpan2 ( 𝐽 ∈ Top → ( 𝐽 ∩ 𝒫 𝑆 ) ∈ 𝐽 )
6 5 adantr ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( 𝐽 ∩ 𝒫 𝑆 ) ∈ 𝐽 )
7 2 6 eqeltrd ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ∈ 𝐽 )