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 e. Top
	unicls.2	|- X = U. J
Assertion	unicls	|- U. ( Clsd ` J ) = X

Proof

Step	Hyp	Ref	Expression
1		unicls.1	|- J e. Top
2		unicls.2	|- X = U. J
3	2	cldss2	|- ( Clsd ` J ) C_ ~P X
4		sspwuni	|- ( ( Clsd ` J ) C_ ~P X <-> U. ( Clsd ` J ) C_ X )
5	3 4	mpbi	|- U. ( Clsd ` J ) C_ X
6	2	topcld	|- ( J e. Top -> X e. ( Clsd ` J ) )
7	1 6	ax-mp	|- X e. ( Clsd ` J )
8		unissel	|- ( ( U. ( Clsd ` J ) C_ X /\ X e. ( Clsd ` J ) ) -> U. ( Clsd ` J ) = X )
9	5 7 8	mp2an	|- U. ( Clsd ` J ) = X