Theorem mrcid

Description: The closure of a closed set is itself. (Contributed by Stefan O'Rear, 31-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2		mress	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐶 ) → 𝑈 ⊆ 𝑋 )
3	1	mrcval	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑈 ) = ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } )
4	2 3	syldan	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑈 ) = ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } )
5		intmin	⊢ ( 𝑈 ∈ 𝐶 → ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } = 𝑈 )
6	5	adantl	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐶 ) → ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } = 𝑈 )
7	4 6	eqtrd	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑈 ) = 𝑈 )