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 )