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 ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } )