Theorem axregndlem2

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

	Ref	Expression
Assertion	axregndlem2	$$⊢x\in y\to \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		axreg2	$$⊢w\in y\to \exists w\left(w\in y\wedge \forall z\left(z\in w\to \neg z\in y\right)\right)$$
2	1	ax-gen	$$⊢\forall w\left(w\in y\to \exists w\left(w\in y\wedge \forall z\left(z\in w\to \neg z\in y\right)\right)\right)$$
3		nfnae	$$⊢Ⅎx\neg \forall xx=y$$
4		nfnae	$$⊢Ⅎx\neg \forall xx=z$$
5	3 4	nfan	$$⊢Ⅎx\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)$$
6		nfcvd	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \underset{\_}{Ⅎ}xw$$
7		nfcvf	$$⊢\neg \forall xx=y\to \underset{\_}{Ⅎ}xy$$
8	7	adantr	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \underset{\_}{Ⅎ}xy$$
9	6 8	nfeld	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎxw\in y$$
10		nfv	$$⊢Ⅎw\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)$$
11		nfnae	$$⊢Ⅎz\neg \forall xx=y$$
12		nfnae	$$⊢Ⅎz\neg \forall xx=z$$
13	11 12	nfan	$$⊢Ⅎz\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)$$
14		nfcvf	$$⊢\neg \forall xx=z\to \underset{\_}{Ⅎ}xz$$
15	14	adantl	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \underset{\_}{Ⅎ}xz$$
16	15 6	nfeld	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎxz\in w$$
17	15 8	nfeld	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎxz\in y$$
18	17	nfnd	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎx\neg z\in y$$
19	16 18	nfimd	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎx\left(z\in w\to \neg z\in y\right)$$
20	13 19	nfald	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎx\forall z\left(z\in w\to \neg z\in y\right)$$
21	9 20	nfand	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎx\left(w\in y\wedge \forall z\left(z\in w\to \neg z\in y\right)\right)$$
22	10 21	nfexd	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎx\exists w\left(w\in y\wedge \forall z\left(z\in w\to \neg z\in y\right)\right)$$
23	9 22	nfimd	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎx\left(w\in y\to \exists w\left(w\in y\wedge \forall z\left(z\in w\to \neg z\in y\right)\right)\right)$$
24		simpr	$$⊢\left(\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\wedge w=x\right)\to w=x$$
25	24	eleq1d	$$⊢\left(\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\wedge w=x\right)\to \left(w\in y\leftrightarrow x\in y\right)$$
26		nfcvd	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \underset{\_}{Ⅎ}zw$$
27		nfcvf2	$$⊢\neg \forall xx=z\to \underset{\_}{Ⅎ}zx$$
28	27	adantl	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \underset{\_}{Ⅎ}zx$$
29	26 28	nfeqd	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎzw=x$$
30	13 29	nfan1	$$⊢Ⅎz\left(\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\wedge w=x\right)$$
31	24	eleq2d	$$⊢\left(\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\wedge w=x\right)\to \left(z\in w\leftrightarrow z\in x\right)$$
32	31	imbi1d	$$⊢\left(\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\wedge w=x\right)\to \left(\left(z\in w\to \neg z\in y\right)\leftrightarrow \left(z\in x\to \neg z\in y\right)\right)$$
33	30 32	albid	$$⊢\left(\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\wedge w=x\right)\to \left(\forall z\left(z\in w\to \neg z\in y\right)\leftrightarrow \forall z\left(z\in x\to \neg z\in y\right)\right)$$
34	25 33	anbi12d	$$⊢\left(\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\wedge w=x\right)\to \left(\left(w\in y\wedge \forall z\left(z\in w\to \neg z\in y\right)\right)\leftrightarrow \left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)\right)$$
35	34	ex	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \left(w=x\to \left(\left(w\in y\wedge \forall z\left(z\in w\to \neg z\in y\right)\right)\leftrightarrow \left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)\right)\right)$$
36	5 21 35	cbvexd	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \left(\exists w\left(w\in y\wedge \forall z\left(z\in w\to \neg z\in y\right)\right)\leftrightarrow \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)\right)$$
37	36	adantr	$$⊢\left(\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\wedge w=x\right)\to \left(\exists w\left(w\in y\wedge \forall z\left(z\in w\to \neg z\in y\right)\right)\leftrightarrow \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)\right)$$
38	25 37	imbi12d	$$⊢\left(\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\wedge w=x\right)\to \left(\left(w\in y\to \exists w\left(w\in y\wedge \forall z\left(z\in w\to \neg z\in y\right)\right)\right)\leftrightarrow \left(x\in y\to \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)\right)\right)$$
39	38	ex	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \left(w=x\to \left(\left(w\in y\to \exists w\left(w\in y\wedge \forall z\left(z\in w\to \neg z\in y\right)\right)\right)\leftrightarrow \left(x\in y\to \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)\right)\right)\right)$$
40	5 23 39	cbvald	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \left(\forall w\left(w\in y\to \exists w\left(w\in y\wedge \forall z\left(z\in w\to \neg z\in y\right)\right)\right)\leftrightarrow \forall x\left(x\in y\to \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)\right)\right)$$
41	2 40	mpbii	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \forall x\left(x\in y\to \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)\right)$$
42	41	19.21bi	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \left(x\in y\to \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)\right)$$
43	42	ex	$$⊢\neg \forall xx=y\to \left(\neg \forall xx=z\to \left(x\in y\to \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)\right)\right)$$
44		elirrv	$$⊢\neg x\in x$$
45		elequ2	$$⊢x=y\to \left(x\in x\leftrightarrow x\in y\right)$$
46	44 45	mtbii	$$⊢x=y\to \neg x\in y$$
47	46	sps	$$⊢\forall xx=y\to \neg x\in y$$
48	47	pm2.21d	$$⊢\forall xx=y\to \left(x\in y\to \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)\right)$$
49		axregndlem1	$$⊢\forall xx=z\to \left(x\in y\to \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)\right)$$
50	43 48 49	pm2.61ii	$$⊢x\in y\to \exists x\left(x\in y\wedge \forall z\left(z\in x\to \neg z\in y\right)\right)$$