Theorem mrcssid

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

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

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2		ssintub	⊢ 𝑈 ⊆ ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 }
3	1	mrcval	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → ( 𝐹 ‘ 𝑈 ) = ∩ { 𝑠 ∈ 𝐶 ∣ 𝑈 ⊆ 𝑠 } )
4	2 3	sseqtrrid	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝑋 ) → 𝑈 ⊆ ( 𝐹 ‘ 𝑈 ) )