Theorem topcld

Description: The underlying set of a topology is closed. Part of Theorem 6.1(1) of Munkres p. 93. (Contributed by NM, 3-Oct-2006)

	Ref	Expression
Hypothesis	iscld.1	|- X = U. J
Assertion	topcld	|- ( J e. Top -> X e. ( Clsd ` J ) )

Proof

Step	Hyp	Ref	Expression
1		iscld.1	|- X = U. J
2		difid	|- ( X \ X ) = (/)
3		0opn	|- ( J e. Top -> (/) e. J )
4	2 3	eqeltrid	|- ( J e. Top -> ( X \ X ) e. J )
5		ssid	|- X C_ X
6	4 5	jctil	|- ( J e. Top -> ( X C_ X /\ ( X \ X ) e. J ) )
7	1	iscld	|- ( J e. Top -> ( X e. ( Clsd ` J ) <-> ( X C_ X /\ ( X \ X ) e. J ) ) )
8	6 7	mpbird	|- ( J e. Top -> X e. ( Clsd ` J ) )