axprlem1

Description: Lemma for axpr . There exists a set to which all empty sets belong. (Contributed by Rohan Ridenour, 10-Aug-2023) (Revised by BJ, 13-Aug-2023) (Proof shortened by Matthew House, 6-Apr-2026)

		Ref	Expression
	Assertion	axprlem1	$⊢ \exists x \forall y (\forall z \neg z \in y \to y \in x)$

Proof

Step	Hyp	Ref	Expression
1		ax-pow	$⊢ \exists x \forall y (\forall z (z \in y \to z \in w) \to y \in x)$
2		pm2.21	$⊢ \neg z \in y \to (z \in y \to z \in w)$
3	2	alimi	$⊢ \forall z \neg z \in y \to \forall z (z \in y \to z \in w)$
4	3	imim1i	$⊢ (\forall z (z \in y \to z \in w) \to y \in x) \to (\forall z \neg z \in y \to y \in x)$
5	4	alimi	$⊢ \forall y (\forall z (z \in y \to z \in w) \to y \in x) \to \forall y (\forall z \neg z \in y \to y \in x)$
6	1 5	eximii	$⊢ \exists x \forall y (\forall z \neg z \in y \to y \in x)$

Metamath Proof Explorer

Theorem axprlem1

Proof