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

Metamath Proof Explorer

Theorem clsval

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

Ref Expression
Hypothesis iscld.1 ⊢ 𝑋 = ∪ 𝐽
Assertion clsval ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } )

Proof

Step Hyp Ref Expression
1 iscld.1 ⊢ 𝑋 = ∪ 𝐽
2 1 clsfval ⊢ ( 𝐽 ∈ Top → ( cls ‘ 𝐽 ) = ( 𝑦 ∈ 𝒫 𝑋 ↦ ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑦 ⊆ 𝑥 } ) )
3 2 fveq1d ⊢ ( 𝐽 ∈ Top → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = ( ( 𝑦 ∈ 𝒫 𝑋 ↦ ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑦 ⊆ 𝑥 } ) ‘ 𝑆 ) )
4 3 adantr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = ( ( 𝑦 ∈ 𝒫 𝑋 ↦ ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑦 ⊆ 𝑥 } ) ‘ 𝑆 ) )
5 eqid ⊢ ( 𝑦 ∈ 𝒫 𝑋 ↦ ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑦 ⊆ 𝑥 } ) = ( 𝑦 ∈ 𝒫 𝑋 ↦ ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑦 ⊆ 𝑥 } )
6 sseq1 ⊢ ( 𝑦 = 𝑆 → ( 𝑦 ⊆ 𝑥 ↔ 𝑆 ⊆ 𝑥 ) )
7 6 rabbidv ⊢ ( 𝑦 = 𝑆 → { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑦 ⊆ 𝑥 } = { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } )
8 7 inteqd ⊢ ( 𝑦 = 𝑆 → ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑦 ⊆ 𝑥 } = ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } )
9 1 topopn ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
10 elpw2g ⊢ ( 𝑋 ∈ 𝐽 → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
11 9 10 syl ⊢ ( 𝐽 ∈ Top → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
12 11 biimpar ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ∈ 𝒫 𝑋 )
13 1 topcld ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ ( Clsd ‘ 𝐽 ) )
14 sseq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑆 ⊆ 𝑥 ↔ 𝑆 ⊆ 𝑋 ) )
15 14 rspcev ⊢ ( ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ 𝑋 ) → ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) 𝑆 ⊆ 𝑥 )
16 13 15 sylan ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) 𝑆 ⊆ 𝑥 )
17 intexrab ⊢ ( ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) 𝑆 ⊆ 𝑥 ↔ ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } ∈ V )
18 16 17 sylib ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } ∈ V )
19 5 8 12 18 fvmptd3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝑦 ∈ 𝒫 𝑋 ↦ ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑦 ⊆ 𝑥 } ) ‘ 𝑆 ) = ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } )
20 4 19 eqtrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } )