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	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
Assertion	mrcidb	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝑈 ∈ 𝐶 ↔ ( 𝐹 ‘ 𝑈 ) = 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2	1	mrcid	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑈 ) = 𝑈 )
3		simpr	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑈 ) = 𝑈 ) → ( 𝐹 ‘ 𝑈 ) = 𝑈 )
4	1	mrcssv	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝐹 ‘ 𝑈 ) ⊆ 𝑋 )
5	4	adantr	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑈 ) = 𝑈 ) → ( 𝐹 ‘ 𝑈 ) ⊆ 𝑋 )
6	3 5	eqsstrrd	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑈 ) = 𝑈 ) → 𝑈 ⊆ 𝑋 )
7	1	mrccl	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑈 ) ∈ 𝐶 )
8	6 7	syldan	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑈 ) = 𝑈 ) → ( 𝐹 ‘ 𝑈 ) ∈ 𝐶 )
9	3 8	eqeltrrd	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑈 ) = 𝑈 ) → 𝑈 ∈ 𝐶 )
10	2 9	impbida	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝑈 ∈ 𝐶 ↔ ( 𝐹 ‘ 𝑈 ) = 𝑈 ) )