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

Metamath Proof Explorer

Theorem mrcidb2

Description: A set is closed iff it contains its closure. (Contributed by Stefan O'Rear, 2-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 mrcfval.f 
 |-  F = ( mrCls ` C )
2 1 mrcidb 
 |-  ( C e. ( Moore ` X ) -> ( U e. C <-> ( F ` U ) = U ) )
3 2 adantr 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ X ) -> ( U e. C <-> ( F ` U ) = U ) )
4 eqss 
 |-  ( ( F ` U ) = U <-> ( ( F ` U ) C_ U /\ U C_ ( F ` U ) ) )
5 1 mrcssid 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ X ) -> U C_ ( F ` U ) )
6 5 biantrud 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ X ) -> ( ( F ` U ) C_ U <-> ( ( F ` U ) C_ U /\ U C_ ( F ` U ) ) ) )
7 4 6 bitr4id 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ X ) -> ( ( F ` U ) = U <-> ( F ` U ) C_ U ) )
8 3 7 bitrd 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ X ) -> ( U e. C <-> ( F ` U ) C_ U ) )