Metamath Proof Explorer

Theorem clublem

Description: If a superset Y of X possesses the property parameterized in x in ps , then Y is a superset of the closure of that property for the set X . (Contributed by RP, 23-Jul-2020)

		Ref	Expression
	Hypotheses	clublem.y	$⊢ φ \to Y \in V$
		clublem.sub	$⊢ x = Y \to (ψ \leftrightarrow χ)$
		clublem.sup	$⊢ φ \to X \subseteq Y$
		clublem.maj	$⊢ φ \to χ$
	Assertion	clublem	$⊢ φ \to ⋂ \{x \| (X \subseteq x \land ψ)\} \subseteq Y$

Proof

Step	Hyp	Ref	Expression
1		clublem.y	$⊢ φ \to Y \in V$
2		clublem.sub	$⊢ x = Y \to (ψ \leftrightarrow χ)$
3		clublem.sup	$⊢ φ \to X \subseteq Y$
4		clublem.maj	$⊢ φ \to χ$
5	1	a1d	$⊢ φ \to ((X \subseteq Y \land χ) \to Y \in V)$
6	2	cleq2lem	$⊢ x = Y \to ((X \subseteq x \land ψ) \leftrightarrow (X \subseteq Y \land χ))$
7	6	elab3g	$⊢ ((X \subseteq Y \land χ) \to Y \in V) \to (Y \in \{x \| (X \subseteq x \land ψ)\} \leftrightarrow (X \subseteq Y \land χ))$
8	5 7	syl	$⊢ φ \to (Y \in \{x \| (X \subseteq x \land ψ)\} \leftrightarrow (X \subseteq Y \land χ))$
9	3 4 8	mpbir2and	$⊢ φ \to Y \in \{x \| (X \subseteq x \land ψ)\}$
10		intss1	$⊢ Y \in \{x \| (X \subseteq x \land ψ)\} \to ⋂ \{x \| (X \subseteq x \land ψ)\} \subseteq Y$
11	9 10	syl	$⊢ φ \to ⋂ \{x \| (X \subseteq x \land ψ)\} \subseteq Y$