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

Metamath Proof Explorer

Theorem mrccls

Description: Moore closure generalizes closure in a topology. (Contributed by Stefan O'Rear, 31-Jan-2015)

Ref Expression
Hypothesis mrccls.f ⊢ F = mrCls ⁡ Clsd ⁡ J
Assertion mrccls ⊢ J ∈ Top → cls ⁡ J = F

Proof

Step Hyp Ref Expression
1 mrccls.f ⊢ F = mrCls ⁡ Clsd ⁡ J
2 eqid ⊢ ⋃ J = ⋃ J
3 2 clsfval ⊢ J ∈ Top → cls ⁡ J = a ∈ 𝒫 ⋃ J ⟼ ⋂ b ∈ Clsd ⁡ J | a ⊆ b
4 2 cldmre ⊢ J ∈ Top → Clsd ⁡ J ∈ Moore ⁡ ⋃ J
5 1 mrcfval ⊢ Clsd ⁡ J ∈ Moore ⁡ ⋃ J → F = a ∈ 𝒫 ⋃ J ⟼ ⋂ b ∈ Clsd ⁡ J | a ⊆ b
6 4 5 syl ⊢ J ∈ Top → F = a ∈ 𝒫 ⋃ J ⟼ ⋂ b ∈ Clsd ⁡ J | a ⊆ b
7 3 6 eqtr4d ⊢ J ∈ Top → cls ⁡ J = F