Theorem mrcidm

Description: The closure operation is idempotent. (Contributed by Stefan O'Rear, 31-Jan-2015)

	Ref	Expression
Hypothesis	mrcfval.f	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
Assertion	mrcidm	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑈 ) ) = ( 𝐹 ‘ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2	1	mrccl	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑈 ) ∈ 𝐶 )
3	1	mrcid	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑈 ) ∈ 𝐶 ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑈 ) ) = ( 𝐹 ‘ 𝑈 ) )
4	2 3	syldan	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → ( 𝐹 ‘ ( 𝐹 ‘ 𝑈 ) ) = ( 𝐹 ‘ 𝑈 ) )