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	$⊢ F = mrCls (C)$
	Assertion	mrcssv	$⊢ C \in Moore (X) \to F (U) \subseteq X$

Step	Hyp	Ref	Expression
1		mrcfval.f	$⊢ F = mrCls (C)$
2		fvssunirn	$⊢ F (U) \subseteq ⋃ ran F$
3	1	mrcf	$⊢ C \in Moore (X) \to F : 𝒫 X ⟶ C$
4		frn	$⊢ F : 𝒫 X ⟶ C \to ran F \subseteq C$
5		uniss	$⊢ ran F \subseteq C \to ⋃ ran F \subseteq ⋃ C$
6	3 4 5	3syl	$⊢ C \in Moore (X) \to ⋃ ran F \subseteq ⋃ C$
7		mreuni	$⊢ C \in Moore (X) \to ⋃ C = X$
8	6 7	sseqtrd	$⊢ C \in Moore (X) \to ⋃ ran F \subseteq X$
9	2 8	sstrid	$⊢ C \in Moore (X) \to F (U) \subseteq X$

Metamath Proof Explorer