This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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)

		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	a1i	$⊢ \forall z \neg z \in w \to (\forall z \neg z \in y \to \forall z (z \in y \to z \in w))$
5	4	imim1d	$⊢ \forall z \neg z \in w \to ((\forall z (z \in y \to z \in w) \to y \in x) \to (\forall z \neg z \in y \to y \in x))$
6	5	alimdv	$⊢ \forall z \neg z \in w \to (\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))$
7	6	eximdv	$⊢ \forall z \neg z \in w \to (\exists x \forall y (\forall z (z \in y \to z \in w) \to y \in x) \to \exists x \forall y (\forall z \neg z \in y \to y \in x))$
8	1 7	mpi	$⊢ \forall z \neg z \in w \to \exists x \forall y (\forall z \neg z \in y \to y \in x)$
9		ax-nul	$⊢ \exists w \forall z \neg z \in w$
10	8 9	exlimiiv	$⊢ \exists x \forall y (\forall z \neg z \in y \to y \in x)$