Metamath Proof Explorer


Theorem unicls

Description: The union of the closed set is the underlying set of the topology. (Contributed by Thierry Arnoux, 21-Sep-2017)

Ref Expression
Hypotheses unicls.1 J Top
unicls.2 X = J
Assertion unicls Clsd J = X

Proof

Step Hyp Ref Expression
1 unicls.1 J Top
2 unicls.2 X = J
3 2 cldss2 Clsd J 𝒫 X
4 sspwuni Clsd J 𝒫 X Clsd J X
5 3 4 mpbi Clsd J X
6 2 topcld J Top X Clsd J
7 1 6 ax-mp X Clsd J
8 unissel Clsd J X X Clsd J Clsd J = X
9 5 7 8 mp2an Clsd J = X