Theorem axpowndlem3

Description: Lemma for the Axiom of Power Sets with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 4-Jan-2002) (Revised by Mario Carneiro, 10-Dec-2016) (Proof shortened by Wolf Lammen, 10-Jun-2019) (New usage is discouraged.)

	Ref	Expression
Assertion	axpowndlem3	$$⊢\neg x=y\to \exists x\forall y\left(\forall x\left(\exists zx\in y\to \forall yx\in z\right)\to y\in x\right)$$

Proof

Step	Hyp	Ref	Expression
1		sp	$$⊢\forall xx=y\to x=y$$
2		p0ex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
3		eleq2	$$⊢x=\left\{\varnothing \right\}\to \left(w\in x\leftrightarrow w\in \left\{\varnothing \right\}\right)$$
4	3	imbi2d	$$⊢x=\left\{\varnothing \right\}\to \left(\left(w=\varnothing \to w\in x\right)\leftrightarrow \left(w=\varnothing \to w\in \left\{\varnothing \right\}\right)\right)$$
5	4	albidv	$$⊢x=\left\{\varnothing \right\}\to \left(\forall w\left(w=\varnothing \to w\in x\right)\leftrightarrow \forall w\left(w=\varnothing \to w\in \left\{\varnothing \right\}\right)\right)$$
6	2 5	spcev	$$⊢\forall w\left(w=\varnothing \to w\in \left\{\varnothing \right\}\right)\to \exists x\forall w\left(w=\varnothing \to w\in x\right)$$
7		0ex	$$⊢\varnothing \in \mathrm{V}$$
8	7	snid	$$⊢\varnothing \in \left\{\varnothing \right\}$$
9		eleq1	$$⊢w=\varnothing \to \left(w\in \left\{\varnothing \right\}\leftrightarrow \varnothing \in \left\{\varnothing \right\}\right)$$
10	8 9	mpbiri	$$⊢w=\varnothing \to w\in \left\{\varnothing \right\}$$
11	6 10	mpg	$$⊢\exists x\forall w\left(w=\varnothing \to w\in x\right)$$
12		neq0	$$⊢\neg w=\varnothing \leftrightarrow \exists xx\in w$$
13	12	con1bii	$$⊢\neg \exists xx\in w\leftrightarrow w=\varnothing$$
14	13	imbi1i	$$⊢\left(\neg \exists xx\in w\to w\in x\right)\leftrightarrow \left(w=\varnothing \to w\in x\right)$$
15	14	albii	$$⊢\forall w\left(\neg \exists xx\in w\to w\in x\right)\leftrightarrow \forall w\left(w=\varnothing \to w\in x\right)$$
16	15	exbii	$$⊢\exists x\forall w\left(\neg \exists xx\in w\to w\in x\right)\leftrightarrow \exists x\forall w\left(w=\varnothing \to w\in x\right)$$
17	11 16	mpbir	$$⊢\exists x\forall w\left(\neg \exists xx\in w\to w\in x\right)$$
18		nfnae	$$⊢Ⅎx\neg \forall xx=y$$
19		nfnae	$$⊢Ⅎy\neg \forall xx=y$$
20		nfcvf2	$$⊢\neg \forall xx=y\to \underset{\_}{Ⅎ}yx$$
21		nfcvd	$$⊢\neg \forall xx=y\to \underset{\_}{Ⅎ}yw$$
22	20 21	nfeld	$$⊢\neg \forall xx=y\to Ⅎyx\in w$$
23	18 22	nfexd	$$⊢\neg \forall xx=y\to Ⅎy\exists xx\in w$$
24	23	nfnd	$$⊢\neg \forall xx=y\to Ⅎy\neg \exists xx\in w$$
25	21 20	nfeld	$$⊢\neg \forall xx=y\to Ⅎyw\in x$$
26	24 25	nfimd	$$⊢\neg \forall xx=y\to Ⅎy\left(\neg \exists xx\in w\to w\in x\right)$$
27		nfeqf2	$$⊢\neg \forall xx=y\to Ⅎxw=y$$
28	18 27	nfan1	$$⊢Ⅎx\left(\neg \forall xx=y\wedge w=y\right)$$
29		elequ2	$$⊢w=y\to \left(x\in w\leftrightarrow x\in y\right)$$
30	29	adantl	$$⊢\left(\neg \forall xx=y\wedge w=y\right)\to \left(x\in w\leftrightarrow x\in y\right)$$
31	28 30	exbid	$$⊢\left(\neg \forall xx=y\wedge w=y\right)\to \left(\exists xx\in w\leftrightarrow \exists xx\in y\right)$$
32	31	notbid	$$⊢\left(\neg \forall xx=y\wedge w=y\right)\to \left(\neg \exists xx\in w\leftrightarrow \neg \exists xx\in y\right)$$
33		elequ1	$$⊢w=y\to \left(w\in x\leftrightarrow y\in x\right)$$
34	33	adantl	$$⊢\left(\neg \forall xx=y\wedge w=y\right)\to \left(w\in x\leftrightarrow y\in x\right)$$
35	32 34	imbi12d	$$⊢\left(\neg \forall xx=y\wedge w=y\right)\to \left(\left(\neg \exists xx\in w\to w\in x\right)\leftrightarrow \left(\neg \exists xx\in y\to y\in x\right)\right)$$
36	35	ex	$$⊢\neg \forall xx=y\to \left(w=y\to \left(\left(\neg \exists xx\in w\to w\in x\right)\leftrightarrow \left(\neg \exists xx\in y\to y\in x\right)\right)\right)$$
37	19 26 36	cbvald	$$⊢\neg \forall xx=y\to \left(\forall w\left(\neg \exists xx\in w\to w\in x\right)\leftrightarrow \forall y\left(\neg \exists xx\in y\to y\in x\right)\right)$$
38	18 37	exbid	$$⊢\neg \forall xx=y\to \left(\exists x\forall w\left(\neg \exists xx\in w\to w\in x\right)\leftrightarrow \exists x\forall y\left(\neg \exists xx\in y\to y\in x\right)\right)$$
39	17 38	mpbii	$$⊢\neg \forall xx=y\to \exists x\forall y\left(\neg \exists xx\in y\to y\in x\right)$$
40		nfae	$$⊢Ⅎx\forall xx=z$$
41		nfae	$$⊢Ⅎy\forall xx=z$$
42		axc11r	$$⊢\forall xx=z\to \left(\forall z\neg x\in y\to \forall x\neg x\in y\right)$$
43		alnex	$$⊢\forall z\neg x\in y\leftrightarrow \neg \exists zx\in y$$
44		alnex	$$⊢\forall x\neg x\in y\leftrightarrow \neg \exists xx\in y$$
45	42 43 44	3imtr3g	$$⊢\forall xx=z\to \left(\neg \exists zx\in y\to \neg \exists xx\in y\right)$$
46		nd3	$$⊢\forall xx=z\to \neg \forall yx\in z$$
47	46	pm2.21d	$$⊢\forall xx=z\to \left(\forall yx\in z\to \neg \exists xx\in y\right)$$
48	45 47	jad	$$⊢\forall xx=z\to \left(\left(\exists zx\in y\to \forall yx\in z\right)\to \neg \exists xx\in y\right)$$
49	48	spsd	$$⊢\forall xx=z\to \left(\forall x\left(\exists zx\in y\to \forall yx\in z\right)\to \neg \exists xx\in y\right)$$
50	49	imim1d	$$⊢\forall xx=z\to \left(\left(\neg \exists xx\in y\to y\in x\right)\to \left(\forall x\left(\exists zx\in y\to \forall yx\in z\right)\to y\in x\right)\right)$$
51	41 50	alimd	$$⊢\forall xx=z\to \left(\forall y\left(\neg \exists xx\in y\to y\in x\right)\to \forall y\left(\forall x\left(\exists zx\in y\to \forall yx\in z\right)\to y\in x\right)\right)$$
52	40 51	eximd	$$⊢\forall xx=z\to \left(\exists x\forall y\left(\neg \exists xx\in y\to y\in x\right)\to \exists x\forall y\left(\forall x\left(\exists zx\in y\to \forall yx\in z\right)\to y\in x\right)\right)$$
53	39 52	syl5com	$$⊢\neg \forall xx=y\to \left(\forall xx=z\to \exists x\forall y\left(\forall x\left(\exists zx\in y\to \forall yx\in z\right)\to y\in x\right)\right)$$
54		axpowndlem2	$$⊢\neg \forall xx=y\to \left(\neg \forall xx=z\to \exists x\forall y\left(\forall x\left(\exists zx\in y\to \forall yx\in z\right)\to y\in x\right)\right)$$
55	53 54	pm2.61d	$$⊢\neg \forall xx=y\to \exists x\forall y\left(\forall x\left(\exists zx\in y\to \forall yx\in z\right)\to y\in x\right)$$
56	1 55	nsyl5	$$⊢\neg x=y\to \exists x\forall y\left(\forall x\left(\exists zx\in y\to \forall yx\in z\right)\to y\in x\right)$$