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 e. Top -> ( cls ` J ) = F )

Proof

Step Hyp Ref Expression
1 mrccls.f
 |-  F = ( mrCls ` ( Clsd ` J ) )
2 eqid
 |-  U. J = U. J
3 2 clsfval
 |-  ( J e. Top -> ( cls ` J ) = ( a e. ~P U. J |-> |^| { b e. ( Clsd ` J ) | a C_ b } ) )
4 2 cldmre
 |-  ( J e. Top -> ( Clsd ` J ) e. ( Moore ` U. J ) )
5 1 mrcfval
 |-  ( ( Clsd ` J ) e. ( Moore ` U. J ) -> F = ( a e. ~P U. J |-> |^| { b e. ( Clsd ` J ) | a C_ b } ) )
6 4 5 syl
 |-  ( J e. Top -> F = ( a e. ~P U. J |-> |^| { b e. ( Clsd ` J ) | a C_ b } ) )
7 3 6 eqtr4d
 |-  ( J e. Top -> ( cls ` J ) = F )