This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mrcssid

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

		Ref	Expression
	Hypothesis	mrcfval.f	$⊢ F = mrCls (C)$
	Assertion	mrcssid	$⊢ (C \in Moore (X) \land U \subseteq X) \to U \subseteq F (U)$

Step	Hyp	Ref	Expression
1		mrcfval.f	$⊢ F = mrCls (C)$
2		ssintub	$⊢ U \subseteq ⋂ \{s \in C \| U \subseteq s\}$
3	1	mrcval	$⊢ (C \in Moore (X) \land U \subseteq X) \to F (U) = ⋂ \{s \in C \| U \subseteq s\}$
4	2 3	sseqtrrid	$⊢ (C \in Moore (X) \land U \subseteq X) \to U \subseteq F (U)$