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

Metamath Proof Explorer

Theorem ntrval

Description: The interior of a subset of a topology's base set is the union of all the open sets it includes. Definition of interior of Munkres p. 94. (Contributed by NM, 10-Sep-2006) (Revised by Mario Carneiro, 11-Nov-2013)

Ref Expression
Hypothesis iscld.1 ⊢ 𝑋 = ∪ 𝐽
Assertion ntrval ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∪ ( 𝐽 ∩ 𝒫 𝑆 ) )

Proof

Step Hyp Ref Expression
1 iscld.1 ⊢ 𝑋 = ∪ 𝐽
2 1 ntrfval ⊢ ( 𝐽 ∈ Top → ( int ‘ 𝐽 ) = ( 𝑥 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑥 ) ) )
3 2 fveq1d ⊢ ( 𝐽 ∈ Top → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ( ( 𝑥 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑥 ) ) ‘ 𝑆 ) )
4 3 adantr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ( ( 𝑥 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑥 ) ) ‘ 𝑆 ) )
5 eqid ⊢ ( 𝑥 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑥 ) ) = ( 𝑥 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑥 ) )
6 pweq ⊢ ( 𝑥 = 𝑆 → 𝒫 𝑥 = 𝒫 𝑆 )
7 6 ineq2d ⊢ ( 𝑥 = 𝑆 → ( 𝐽 ∩ 𝒫 𝑥 ) = ( 𝐽 ∩ 𝒫 𝑆 ) )
8 7 unieqd ⊢ ( 𝑥 = 𝑆 → ∪ ( 𝐽 ∩ 𝒫 𝑥 ) = ∪ ( 𝐽 ∩ 𝒫 𝑆 ) )
9 1 topopn ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
10 elpw2g ⊢ ( 𝑋 ∈ 𝐽 → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
11 9 10 syl ⊢ ( 𝐽 ∈ Top → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
12 11 biimpar ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ∈ 𝒫 𝑋 )
13 inex1g ⊢ ( 𝐽 ∈ Top → ( 𝐽 ∩ 𝒫 𝑆 ) ∈ V )
14 13 adantr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐽 ∩ 𝒫 𝑆 ) ∈ V )
15 14 uniexd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ∪ ( 𝐽 ∩ 𝒫 𝑆 ) ∈ V )
16 5 8 12 15 fvmptd3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝑥 ∈ 𝒫 𝑋 ↦ ∪ ( 𝐽 ∩ 𝒫 𝑥 ) ) ‘ 𝑆 ) = ∪ ( 𝐽 ∩ 𝒫 𝑆 ) )
17 4 16 eqtrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑆 ) = ∪ ( 𝐽 ∩ 𝒫 𝑆 ) )