Metamath Proof Explorer


Theorem cldval

Description: The set of closed sets of a topology. (Note that the set of open sets is just the topology itself, so we don't have a separate definition.) (Contributed by NM, 2-Oct-2006) (Revised by Mario Carneiro, 11-Nov-2013)

Ref Expression
Hypothesis cldval.1 X = J
Assertion cldval J Top Clsd J = x 𝒫 X | X x J

Proof

Step Hyp Ref Expression
1 cldval.1 X = J
2 1 topopn J Top X J
3 pwexg X J 𝒫 X V
4 rabexg 𝒫 X V x 𝒫 X | X x J V
5 2 3 4 3syl J Top x 𝒫 X | X x J V
6 unieq j = J j = J
7 6 1 syl6eqr j = J j = X
8 7 pweqd j = J 𝒫 j = 𝒫 X
9 7 difeq1d j = J j x = X x
10 eleq12 j x = X x j = J j x j X x J
11 9 10 mpancom j = J j x j X x J
12 8 11 rabeqbidv j = J x 𝒫 j | j x j = x 𝒫 X | X x J
13 df-cld Clsd = j Top x 𝒫 j | j x j
14 12 13 fvmptg J Top x 𝒫 X | X x J V Clsd J = x 𝒫 X | X x J
15 5 14 mpdan J Top Clsd J = x 𝒫 X | X x J