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 𝐹 = ( mrCls ‘ ( Clsd ‘ 𝐽 ) )
Assertion mrccls ( 𝐽 ∈ Top → ( cls ‘ 𝐽 ) = 𝐹 )

Proof

Step Hyp Ref Expression
1 mrccls.f 𝐹 = ( mrCls ‘ ( Clsd ‘ 𝐽 ) )
2 eqid 𝐽 = 𝐽
3 2 clsfval ( 𝐽 ∈ Top → ( cls ‘ 𝐽 ) = ( 𝑎 ∈ 𝒫 𝐽 { 𝑏 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑎𝑏 } ) )
4 2 cldmre ( 𝐽 ∈ Top → ( Clsd ‘ 𝐽 ) ∈ ( Moore ‘ 𝐽 ) )
5 1 mrcfval ( ( Clsd ‘ 𝐽 ) ∈ ( Moore ‘ 𝐽 ) → 𝐹 = ( 𝑎 ∈ 𝒫 𝐽 { 𝑏 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑎𝑏 } ) )
6 4 5 syl ( 𝐽 ∈ Top → 𝐹 = ( 𝑎 ∈ 𝒫 𝐽 { 𝑏 ∈ ( Clsd ‘ 𝐽 ) ∣ 𝑎𝑏 } ) )
7 3 6 eqtr4d ( 𝐽 ∈ Top → ( cls ‘ 𝐽 ) = 𝐹 )