clss2lem

Description: The closure of a property is a superset of the closure of a less restrictive property. (Contributed by RP, 24-Jul-2020)

		Ref	Expression
	Hypothesis	clss2lem.1	$⊢ φ \to (χ \to ψ)$
	Assertion	clss2lem	$⊢ φ \to ⋂ \{x \| (X \subseteq x \land ψ)\} \subseteq ⋂ \{x \| (X \subseteq x \land χ)\}$

Step	Hyp	Ref	Expression
1		clss2lem.1	$⊢ φ \to (χ \to ψ)$
2	1	adantld	$⊢ φ \to ((X \subseteq x \land χ) \to ψ)$
3	2	alrimiv	$⊢ φ \to \forall x ((X \subseteq x \land χ) \to ψ)$
4		pm5.3	$⊢ ((X \subseteq x \land χ) \to ψ) \leftrightarrow ((X \subseteq x \land χ) \to (X \subseteq x \land ψ))$
5	4	albii	$⊢ \forall x ((X \subseteq x \land χ) \to ψ) \leftrightarrow \forall x ((X \subseteq x \land χ) \to (X \subseteq x \land ψ))$
6		ss2ab	$⊢ \{x \| (X \subseteq x \land χ)\} \subseteq \{x \| (X \subseteq x \land ψ)\} \leftrightarrow \forall x ((X \subseteq x \land χ) \to (X \subseteq x \land ψ))$
7	5 6	bitr4i	$⊢ \forall x ((X \subseteq x \land χ) \to ψ) \leftrightarrow \{x \| (X \subseteq x \land χ)\} \subseteq \{x \| (X \subseteq x \land ψ)\}$
8	3 7	sylib	$⊢ φ \to \{x \| (X \subseteq x \land χ)\} \subseteq \{x \| (X \subseteq x \land ψ)\}$
9		intss	$⊢ \{x \| (X \subseteq x \land χ)\} \subseteq \{x \| (X \subseteq x \land ψ)\} \to ⋂ \{x \| (X \subseteq x \land ψ)\} \subseteq ⋂ \{x \| (X \subseteq x \land χ)\}$
10	8 9	syl	$⊢ φ \to ⋂ \{x \| (X \subseteq x \land ψ)\} \subseteq ⋂ \{x \| (X \subseteq x \land χ)\}$

Metamath Proof Explorer