Metamath Proof Explorer


Theorem clsfval

Description: The closure function on the subsets of a topology's base set. (Contributed by NM, 3-Oct-2006) (Revised by Mario Carneiro, 11-Nov-2013)

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

Proof

Step Hyp Ref Expression
1 cldval.1 X = J
2 1 topopn J Top X J
3 pwexg X J 𝒫 X V
4 mptexg 𝒫 X V x 𝒫 X y Clsd J | x y V
5 2 3 4 3syl J Top x 𝒫 X y Clsd J | x y V
6 unieq j = J j = J
7 6 1 eqtr4di j = J j = X
8 7 pweqd j = J 𝒫 j = 𝒫 X
9 fveq2 j = J Clsd j = Clsd J
10 9 rabeqdv j = J y Clsd j | x y = y Clsd J | x y
11 10 inteqd j = J y Clsd j | x y = y Clsd J | x y
12 8 11 mpteq12dv j = J x 𝒫 j y Clsd j | x y = x 𝒫 X y Clsd J | x y
13 df-cls cls = j Top x 𝒫 j y Clsd j | x y
14 12 13 fvmptg J Top x 𝒫 X y Clsd J | x y V cls J = x 𝒫 X y Clsd J | x y
15 5 14 mpdan J Top cls J = x 𝒫 X y Clsd J | x y