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

Metamath Proof Explorer

Theorem mrcid

Description: The closure of a closed set is itself. (Contributed by Stefan O'Rear, 31-Jan-2015)

Ref Expression
Hypothesis mrcfval.f 
|- F = ( mrCls ` C )
Assertion mrcid 
|- ( ( C e. ( Moore ` X ) /\ U e. C ) -> ( F ` U ) = U )

Proof

Step Hyp Ref Expression
1 mrcfval.f 
 |-  F = ( mrCls ` C )
2 mress 
 |-  ( ( C e. ( Moore ` X ) /\ U e. C ) -> U C_ X )
3 1 mrcval 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ X ) -> ( F ` U ) = |^| { s e. C | U C_ s } )
4 2 3 syldan 
 |-  ( ( C e. ( Moore ` X ) /\ U e. C ) -> ( F ` U ) = |^| { s e. C | U C_ s } )
5 intmin 
 |-  ( U e. C -> |^| { s e. C | U C_ s } = U )
6 5 adantl 
 |-  ( ( C e. ( Moore ` X ) /\ U e. C ) -> |^| { s e. C | U C_ s } = U )
7 4 6 eqtrd 
 |-  ( ( C e. ( Moore ` X ) /\ U e. C ) -> ( F ` U ) = U )