This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: A subset of the underlying set of a topology is closed iff its
complement is open. (Contributed by NM, 4-Oct-2006)
|
|
Ref |
Expression |
|
Hypothesis |
iscld.1 |
⊢ 𝑋 = ∪ 𝐽 |
|
Assertion |
iscld2 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
iscld.1 |
⊢ 𝑋 = ∪ 𝐽 |
| 2 |
1
|
iscld |
⊢ ( 𝐽 ∈ Top → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑆 ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 ) ) ) |
| 3 |
2
|
baibd |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 ) ) |