Metamath Proof Explorer


Theorem clsf2

Description: The closure function is a map from the powerset of the base set to itself. This is less precise than clsf . (Contributed by RP, 22-Apr-2021)

Ref Expression
Hypotheses clselmap.x X = J
clselmap.k K = cls J
Assertion clsf2 J Top K : 𝒫 X 𝒫 X

Proof

Step Hyp Ref Expression
1 clselmap.x X = J
2 clselmap.k K = cls J
3 1 clsf J Top cls J : 𝒫 X Clsd J
4 2 feq1i K : 𝒫 X Clsd J cls J : 𝒫 X Clsd J
5 df-f K : 𝒫 X Clsd J K Fn 𝒫 X ran K Clsd J
6 4 5 sylbb1 cls J : 𝒫 X Clsd J K Fn 𝒫 X ran K Clsd J
7 1 cldss2 Clsd J 𝒫 X
8 sstr2 ran K Clsd J Clsd J 𝒫 X ran K 𝒫 X
9 7 8 mpi ran K Clsd J ran K 𝒫 X
10 9 anim2i K Fn 𝒫 X ran K Clsd J K Fn 𝒫 X ran K 𝒫 X
11 3 6 10 3syl J Top K Fn 𝒫 X ran K 𝒫 X
12 df-f K : 𝒫 X 𝒫 X K Fn 𝒫 X ran K 𝒫 X
13 11 12 sylibr J Top K : 𝒫 X 𝒫 X