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

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 ‘ 𝐽 ) ‘ ( 𝑋 ∖ 𝑆 ) ) ) )