clsslem

Description: The closure of a subclass is a subclass of the closure. (Contributed by RP, 16-May-2020)

		Ref	Expression
	Assertion	clsslem	$⊢ R \subseteq S \to ⋂ \{r \| (R \subseteq r \land φ)\} \subseteq ⋂ \{r \| (S \subseteq r \land φ)\}$

Step	Hyp	Ref	Expression
1		sstr2	$⊢ R \subseteq S \to (S \subseteq r \to R \subseteq r)$
2	1	anim1d	$⊢ R \subseteq S \to ((S \subseteq r \land φ) \to (R \subseteq r \land φ))$
3	2	ss2abdv	$⊢ R \subseteq S \to \{r \| (S \subseteq r \land φ)\} \subseteq \{r \| (R \subseteq r \land φ)\}$
4		intss	$⊢ \{r \| (S \subseteq r \land φ)\} \subseteq \{r \| (R \subseteq r \land φ)\} \to ⋂ \{r \| (R \subseteq r \land φ)\} \subseteq ⋂ \{r \| (S \subseteq r \land φ)\}$
5	3 4	syl	$⊢ R \subseteq S \to ⋂ \{r \| (R \subseteq r \land φ)\} \subseteq ⋂ \{r \| (S \subseteq r \land φ)\}$

Metamath Proof Explorer