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 | ⊢ 𝑋 = ∪ 𝐽 | |
| Assertion | topcld | ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ ( Clsd ‘ 𝐽 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iscld.1 | ⊢ 𝑋 = ∪ 𝐽 | |
| 2 | difid | ⊢ ( 𝑋 ∖ 𝑋 ) = ∅ | |
| 3 | 0opn | ⊢ ( 𝐽 ∈ Top → ∅ ∈ 𝐽 ) | |
| 4 | 2 3 | eqeltrid | ⊢ ( 𝐽 ∈ Top → ( 𝑋 ∖ 𝑋 ) ∈ 𝐽 ) |
| 5 | ssid | ⊢ 𝑋 ⊆ 𝑋 | |
| 6 | 4 5 | jctil | ⊢ ( 𝐽 ∈ Top → ( 𝑋 ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑋 ) ∈ 𝐽 ) ) |
| 7 | 1 | iscld | ⊢ ( 𝐽 ∈ Top → ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑋 ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑋 ) ∈ 𝐽 ) ) ) |
| 8 | 6 7 | mpbird | ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ ( Clsd ‘ 𝐽 ) ) |