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