Metamath Proof Explorer


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 ) )