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