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