Metamath Proof Explorer


Theorem ntrval2

Description: Interior expressed in terms of closure. (Contributed by NM, 1-Oct-2007)

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

Proof

Step Hyp Ref Expression
1 clscld.1 𝑋 = 𝐽
2 difss ( 𝑋𝑆 ) ⊆ 𝑋
3 1 clsval2 ( ( 𝐽 ∈ Top ∧ ( 𝑋𝑆 ) ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋𝑆 ) ) = ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋𝑆 ) ) ) ) )
4 2 3 mpan2 ( 𝐽 ∈ Top → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋𝑆 ) ) = ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋𝑆 ) ) ) ) )
5 4 adantr ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋𝑆 ) ) = ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋𝑆 ) ) ) ) )
6 dfss4 ( 𝑆𝑋 ↔ ( 𝑋 ∖ ( 𝑋𝑆 ) ) = 𝑆 )
7 6 biimpi ( 𝑆𝑋 → ( 𝑋 ∖ ( 𝑋𝑆 ) ) = 𝑆 )
8 7 fveq2d ( 𝑆𝑋 → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋𝑆 ) ) ) = ( ( int ‘ 𝐽 ) ‘ 𝑆 ) )
9 8 adantl ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋𝑆 ) ) ) = ( ( int ‘ 𝐽 ) ‘ 𝑆 ) )
10 9 difeq2d ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ ( 𝑋 ∖ ( 𝑋𝑆 ) ) ) ) = ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) )
11 5 10 eqtrd ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑋𝑆 ) ) = ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) )
12 11 difeq2d ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋𝑆 ) ) ) = ( 𝑋 ∖ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
13 1 ntropn ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ∈ 𝐽 )
14 1 eltopss ( ( 𝐽 ∈ Top ∧ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ∈ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 )
15 13 14 syldan ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 )
16 dfss4 ( ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 ↔ ( 𝑋 ∖ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ) = ( ( int ‘ 𝐽 ) ‘ 𝑆 ) )
17 15 16 sylib ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( 𝑋 ∖ ( 𝑋 ∖ ( ( int ‘ 𝐽 ) ‘ 𝑆 ) ) ) = ( ( int ‘ 𝐽 ) ‘ 𝑆 ) )
18 12 17 eqtr2d ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ ( 𝑋𝑆 ) ) ) )