This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cldmreon

Description: The closed sets of a topology over a set are a Moore collection over the same set. (Contributed by Stefan O'Rear, 31-Jan-2015)

Ref Expression
Assertion cldmreon ⊢ J ∈ TopOn ⁡ B → Clsd ⁡ J ∈ Moore ⁡ B

Proof

Step Hyp Ref Expression
1 topontop ⊢ J ∈ TopOn ⁡ B → J ∈ Top
2 eqid ⊢ ⋃ J = ⋃ J
3 2 cldmre ⊢ J ∈ Top → Clsd ⁡ J ∈ Moore ⁡ ⋃ J
4 1 3 syl ⊢ J ∈ TopOn ⁡ B → Clsd ⁡ J ∈ Moore ⁡ ⋃ J
5 toponuni ⊢ J ∈ TopOn ⁡ B → B = ⋃ J
6 5 fveq2d ⊢ J ∈ TopOn ⁡ B → Moore ⁡ B = Moore ⁡ ⋃ J
7 4 6 eleqtrrd ⊢ J ∈ TopOn ⁡ B → Clsd ⁡ J ∈ Moore ⁡ B