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 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 )