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

Metamath Proof Explorer

Theorem iscld

Description: The predicate "the class S is a closed set". (Contributed by NM, 2-Oct-2006) (Revised by Mario Carneiro, 11-Nov-2013)

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

Proof

Step Hyp Ref Expression
1 iscld.1 ⊢ 𝑋 = ∪ 𝐽
2 1 cldval ⊢ ( 𝐽 ∈ Top → ( Clsd ‘ 𝐽 ) = { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ∈ 𝐽 } )
3 2 eleq2d ⊢ ( 𝐽 ∈ Top → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ 𝑆 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ∈ 𝐽 } ) )
4 difeq2 ⊢ ( 𝑥 = 𝑆 → ( 𝑋 ∖ 𝑥 ) = ( 𝑋 ∖ 𝑆 ) )
5 4 eleq1d ⊢ ( 𝑥 = 𝑆 → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐽 ↔ ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 ) )
6 5 elrab ⊢ ( 𝑆 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝑋 ∖ 𝑥 ) ∈ 𝐽 } ↔ ( 𝑆 ∈ 𝒫 𝑋 ∧ ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 ) )
7 3 6 bitrdi ⊢ ( 𝐽 ∈ Top → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑆 ∈ 𝒫 𝑋 ∧ ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 ) ) )
8 1 topopn ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
9 elpw2g ⊢ ( 𝑋 ∈ 𝐽 → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
10 8 9 syl ⊢ ( 𝐽 ∈ Top → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
11 10 anbi1d ⊢ ( 𝐽 ∈ Top → ( ( 𝑆 ∈ 𝒫 𝑋 ∧ ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 ) ↔ ( 𝑆 ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 ) ) )
12 7 11 bitrd ⊢ ( 𝐽 ∈ Top → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑆 ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 ) ) )