Theorem mrcssv

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

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

Proof

Step	Hyp	Ref	Expression
1		mrcfval.f	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2		fvssunirn	⊢ ( 𝐹 ‘ 𝑈 ) ⊆ ∪ ran 𝐹
3	1	mrcf	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐹 : 𝒫 𝑋 ⟶ 𝐶 )
4		frn	⊢ ( 𝐹 : 𝒫 𝑋 ⟶ 𝐶 → ran 𝐹 ⊆ 𝐶 )
5		uniss	⊢ ( ran 𝐹 ⊆ 𝐶 → ∪ ran 𝐹 ⊆ ∪ 𝐶 )
6	3 4 5	3syl	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ∪ ran 𝐹 ⊆ ∪ 𝐶 )
7		mreuni	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ∪ 𝐶 = 𝑋 )
8	6 7	sseqtrd	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ∪ ran 𝐹 ⊆ 𝑋 )
9	2 8	sstrid	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝐹 ‘ 𝑈 ) ⊆ 𝑋 )