Metamath Proof Explorer

Theorem mrcidb

Description: A set is closed iff it is equal to its closure. (Contributed by Stefan O'Rear, 31-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 mrcfval.f 
 |-  F = ( mrCls ` C )
2 1 mrcid 
 |-  ( ( C e. ( Moore ` X ) /\ U e. C ) -> ( F ` U ) = U )
3 simpr 
 |-  ( ( C e. ( Moore ` X ) /\ ( F ` U ) = U ) -> ( F ` U ) = U )
4 1 mrcssv 
 |-  ( C e. ( Moore ` X ) -> ( F ` U ) C_ X )
5 4 adantr 
 |-  ( ( C e. ( Moore ` X ) /\ ( F ` U ) = U ) -> ( F ` U ) C_ X )
6 3 5 eqsstrrd 
 |-  ( ( C e. ( Moore ` X ) /\ ( F ` U ) = U ) -> U C_ X )
7 1 mrccl 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ X ) -> ( F ` U ) e. C )
8 6 7 syldan 
 |-  ( ( C e. ( Moore ` X ) /\ ( F ` U ) = U ) -> ( F ` U ) e. C )
9 3 8 eqeltrrd 
 |-  ( ( C e. ( Moore ` X ) /\ ( F ` U ) = U ) -> U e. C )
10 2 9 impbida 
 |-  ( C e. ( Moore ` X ) -> ( U e. C <-> ( F ` U ) = U ) )