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 ⊢ X = ⋃ J
Assertion iscld ⊢ J ∈ Top → S ∈ Clsd ⁡ J ↔ S ⊆ X ∧ X ∖ S ∈ J

Proof

Step Hyp Ref Expression
1 iscld.1 ⊢ X = ⋃ J
2 1 cldval ⊢ J ∈ Top → Clsd ⁡ J = x ∈ 𝒫 X | X ∖ x ∈ J
3 2 eleq2d ⊢ J ∈ Top → S ∈ Clsd ⁡ J ↔ S ∈ x ∈ 𝒫 X | X ∖ x ∈ J
4 difeq2 ⊢ x = S → X ∖ x = X ∖ S
5 4 eleq1d ⊢ x = S → X ∖ x ∈ J ↔ X ∖ S ∈ J
6 5 elrab ⊢ S ∈ x ∈ 𝒫 X | X ∖ x ∈ J ↔ S ∈ 𝒫 X ∧ X ∖ S ∈ J
7 3 6 bitrdi ⊢ J ∈ Top → S ∈ Clsd ⁡ J ↔ S ∈ 𝒫 X ∧ X ∖ S ∈ J
8 1 topopn ⊢ J ∈ Top → X ∈ J
9 elpw2g ⊢ X ∈ J → S ∈ 𝒫 X ↔ S ⊆ X
10 8 9 syl ⊢ J ∈ Top → S ∈ 𝒫 X ↔ S ⊆ X
11 10 anbi1d ⊢ J ∈ Top → S ∈ 𝒫 X ∧ X ∖ S ∈ J ↔ S ⊆ X ∧ X ∖ S ∈ J
12 7 11 bitrd ⊢ J ∈ Top → S ∈ Clsd ⁡ J ↔ S ⊆ X ∧ X ∖ S ∈ J