ssclaxsep

Description: A class that is closed under subsets models the Axiom of Separation ax-sep . Lemma II.2.4(3) of Kunen2 p. 111.

Note that, to obtain the relativization of an instance of Separation to M , the formula ph would need to be replaced with its relativization to M . However, this new formula is a valid substitution for ph , so this theorem does establish that all instances of Separation hold in M . (Contributed by Eric Schmidt, 29-Sep-2025)

		Ref	Expression
	Assertion	ssclaxsep	$⊢ \forall z \in M 𝒫 z \subseteq M \to \forall z \in M \exists y \in M \forall x \in M (x \in y \leftrightarrow (x \in z \land φ))$

Proof

Step	Hyp	Ref	Expression
1		ax-sep	$⊢ \exists y \forall x (x \in y \leftrightarrow (x \in z \land φ))$
2		biimp	$⊢ (x \in y \leftrightarrow (x \in z \land φ)) \to (x \in y \to (x \in z \land φ))$
3		simpl	$⊢ (x \in z \land φ) \to x \in z$
4	2 3	syl6	$⊢ (x \in y \leftrightarrow (x \in z \land φ)) \to (x \in y \to x \in z)$
5	4	alimi	$⊢ \forall x (x \in y \leftrightarrow (x \in z \land φ)) \to \forall x (x \in y \to x \in z)$
6		velpw	$⊢ y \in 𝒫 z \leftrightarrow y \subseteq z$
7		df-ss	$⊢ y \subseteq z \leftrightarrow \forall x (x \in y \to x \in z)$
8	6 7	bitr2i	$⊢ \forall x (x \in y \to x \in z) \leftrightarrow y \in 𝒫 z$
9	5 8	sylib	$⊢ \forall x (x \in y \leftrightarrow (x \in z \land φ)) \to y \in 𝒫 z$
10		ssel	$⊢ 𝒫 z \subseteq M \to (y \in 𝒫 z \to y \in M)$
11	9 10	syl5	$⊢ 𝒫 z \subseteq M \to (\forall x (x \in y \leftrightarrow (x \in z \land φ)) \to y \in M)$
12		alral	$⊢ \forall x (x \in y \leftrightarrow (x \in z \land φ)) \to \forall x \in M (x \in y \leftrightarrow (x \in z \land φ))$
13	11 12	jca2	$⊢ 𝒫 z \subseteq M \to (\forall x (x \in y \leftrightarrow (x \in z \land φ)) \to (y \in M \land \forall x \in M (x \in y \leftrightarrow (x \in z \land φ))))$
14	13	eximdv	$⊢ 𝒫 z \subseteq M \to (\exists y \forall x (x \in y \leftrightarrow (x \in z \land φ)) \to \exists y (y \in M \land \forall x \in M (x \in y \leftrightarrow (x \in z \land φ))))$
15	1 14	mpi	$⊢ 𝒫 z \subseteq M \to \exists y (y \in M \land \forall x \in M (x \in y \leftrightarrow (x \in z \land φ)))$
16		df-rex	$⊢ \exists y \in M \forall x \in M (x \in y \leftrightarrow (x \in z \land φ)) \leftrightarrow \exists y (y \in M \land \forall x \in M (x \in y \leftrightarrow (x \in z \land φ)))$
17	15 16	sylibr	$⊢ 𝒫 z \subseteq M \to \exists y \in M \forall x \in M (x \in y \leftrightarrow (x \in z \land φ))$
18	17	ralimi	$⊢ \forall z \in M 𝒫 z \subseteq M \to \forall z \in M \exists y \in M \forall x \in M (x \in y \leftrightarrow (x \in z \land φ))$

Metamath Proof Explorer

Theorem ssclaxsep

Proof