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