Description: The closed sets of a topology comprise a Moore system on the points of the topology. (Contributed by Stefan O'Rear, 31-Jan-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | clscld.1 | ⊢ 𝑋 = ∪ 𝐽 | |
| Assertion | cldmre | ⊢ ( 𝐽 ∈ Top → ( Clsd ‘ 𝐽 ) ∈ ( Moore ‘ 𝑋 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | clscld.1 | ⊢ 𝑋 = ∪ 𝐽 | |
| 2 | 1 | cldss2 | ⊢ ( Clsd ‘ 𝐽 ) ⊆ 𝒫 𝑋 |
| 3 | 2 | a1i | ⊢ ( 𝐽 ∈ Top → ( Clsd ‘ 𝐽 ) ⊆ 𝒫 𝑋 ) |
| 4 | 1 | topcld | ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ ( Clsd ‘ 𝐽 ) ) |
| 5 | intcld | ⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ( Clsd ‘ 𝐽 ) ) → ∩ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) | |
| 6 | 5 | ancoms | ⊢ ( ( 𝑥 ⊆ ( Clsd ‘ 𝐽 ) ∧ 𝑥 ≠ ∅ ) → ∩ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) |
| 7 | 6 | 3adant1 | ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ ( Clsd ‘ 𝐽 ) ∧ 𝑥 ≠ ∅ ) → ∩ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) |
| 8 | 3 4 7 | ismred | ⊢ ( 𝐽 ∈ Top → ( Clsd ‘ 𝐽 ) ∈ ( Moore ‘ 𝑋 ) ) |