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\left(\forall z\neg z\in y\to y\in x\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax-pow	$$⊢\exists x\forall y\left(\forall z\left(z\in y\to z\in w\right)\to y\in x\right)$$
2		pm2.21	$$⊢\neg z\in y\to \left(z\in y\to z\in w\right)$$
3	2	alimi	$$⊢\forall z\neg z\in y\to \forall z\left(z\in y\to z\in w\right)$$
4	3	a1i	$$⊢\forall z\neg z\in w\to \left(\forall z\neg z\in y\to \forall z\left(z\in y\to z\in w\right)\right)$$
5	4	imim1d	$$⊢\forall z\neg z\in w\to \left(\left(\forall z\left(z\in y\to z\in w\right)\to y\in x\right)\to \left(\forall z\neg z\in y\to y\in x\right)\right)$$
6	5	alimdv	$$⊢\forall z\neg z\in w\to \left(\forall y\left(\forall z\left(z\in y\to z\in w\right)\to y\in x\right)\to \forall y\left(\forall z\neg z\in y\to y\in x\right)\right)$$
7	6	eximdv	$$⊢\forall z\neg z\in w\to \left(\exists x\forall y\left(\forall z\left(z\in y\to z\in w\right)\to y\in x\right)\to \exists x\forall y\left(\forall z\neg z\in y\to y\in x\right)\right)$$
8	1 7	mpi	$$⊢\forall z\neg z\in w\to \exists x\forall y\left(\forall z\neg z\in y\to y\in x\right)$$
9		ax-nul	$$⊢\exists w\forall z\neg z\in w$$
10	8 9	exlimiiv	$$⊢\exists x\forall y\left(\forall z\neg z\in y\to y\in x\right)$$