Theorem clscld

Description: The closure of a subset of a topology's underlying set is closed. (Contributed by NM, 4-Oct-2006)

	Ref	Expression
Hypothesis	clscld.1	⊢ 𝑋 = ∪ 𝐽
Assertion	clscld	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		clscld.1	⊢ 𝑋 = ∪ 𝐽
2	1	clsval	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } )
3	1	topcld	⊢ ( 𝐽 ∈ Top → 𝑋 ∈ ( Clsd ‘ 𝐽 ) )
4	3	anim1i	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ 𝑋 ) )
5		sseq2	⊢ ( 𝑥 = 𝑋 → ( 𝑆 ⊆ 𝑥 ↔ 𝑆 ⊆ 𝑋 ) )
6	5	elrab	⊢ ( 𝑋 ∈ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } ↔ ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ 𝑋 ) )
7	4 6	sylibr	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑋 ∈ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } )
8	7	ne0d	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } ≠ ∅ )
9		ssrab2	⊢ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } ⊆ ( Clsd ‘ 𝐽 )
10		intcld	⊢ ( ( { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } ≠ ∅ ∧ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } ⊆ ( Clsd ‘ 𝐽 ) ) → ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } ∈ ( Clsd ‘ 𝐽 ) )
11	8 9 10	sylancl	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ∩ { 𝑥 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑆 ⊆ 𝑥 } ∈ ( Clsd ‘ 𝐽 ) )
12	2 11	eqeltrd	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) )