Theorem axrepndlem2

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

	Ref	Expression
Assertion	axrepndlem2	$$⊢\left(\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\wedge \neg \forall yy=z\right)\to \exists x\left(\exists y\forall z\left(\phi \to z=y\right)\to \forall z\left(z\in x\leftrightarrow \exists x\left(x\in y\wedge \forall y\phi \right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		axrepndlem1	$$⊢\neg \forall yy=z\to \exists w\left(\exists y\forall z\left(\left[w/x\right]\phi \to z=y\right)\to \forall z\left(z\in w\leftrightarrow \exists w\left(w\in y\wedge \forall y\left[w/x\right]\phi \right)\right)\right)$$
2		nfnae	$$⊢Ⅎx\neg \forall xx=y$$
3		nfnae	$$⊢Ⅎx\neg \forall xx=z$$
4	2 3	nfan	$$⊢Ⅎx\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)$$
5		nfnae	$$⊢Ⅎy\neg \forall xx=y$$
6		nfnae	$$⊢Ⅎy\neg \forall xx=z$$
7	5 6	nfan	$$⊢Ⅎy\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)$$
8		nfnae	$$⊢Ⅎz\neg \forall xx=y$$
9		nfnae	$$⊢Ⅎz\neg \forall xx=z$$
10	8 9	nfan	$$⊢Ⅎz\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)$$
11		nfs1v	$$⊢Ⅎx\left[w/x\right]\phi$$
12	11	a1i	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎx\left[w/x\right]\phi$$
13		nfcvf	$$⊢\neg \forall xx=z\to \underset{\_}{Ⅎ}xz$$
14	13	adantl	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \underset{\_}{Ⅎ}xz$$
15		nfcvf	$$⊢\neg \forall xx=y\to \underset{\_}{Ⅎ}xy$$
16	15	adantr	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \underset{\_}{Ⅎ}xy$$
17	14 16	nfeqd	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎxz=y$$
18	12 17	nfimd	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎx\left(\left[w/x\right]\phi \to z=y\right)$$
19	10 18	nfald	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎx\forall z\left(\left[w/x\right]\phi \to z=y\right)$$
20	7 19	nfexd	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎx\exists y\forall z\left(\left[w/x\right]\phi \to z=y\right)$$
21		nfcvd	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \underset{\_}{Ⅎ}xw$$
22	14 21	nfeld	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎxz\in w$$
23		nfv	$$⊢Ⅎw\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)$$
24	21 16	nfeld	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎxw\in y$$
25	7 12	nfald	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎx\forall y\left[w/x\right]\phi$$
26	24 25	nfand	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎx\left(w\in y\wedge \forall y\left[w/x\right]\phi \right)$$
27	23 26	nfexd	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎx\exists w\left(w\in y\wedge \forall y\left[w/x\right]\phi \right)$$
28	22 27	nfbid	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎx\left(z\in w\leftrightarrow \exists w\left(w\in y\wedge \forall y\left[w/x\right]\phi \right)\right)$$
29	10 28	nfald	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎx\forall z\left(z\in w\leftrightarrow \exists w\left(w\in y\wedge \forall y\left[w/x\right]\phi \right)\right)$$
30	20 29	nfimd	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎx\left(\exists y\forall z\left(\left[w/x\right]\phi \to z=y\right)\to \forall z\left(z\in w\leftrightarrow \exists w\left(w\in y\wedge \forall y\left[w/x\right]\phi \right)\right)\right)$$
31		nfcvd	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \underset{\_}{Ⅎ}yw$$
32		nfcvf2	$$⊢\neg \forall xx=y\to \underset{\_}{Ⅎ}yx$$
33	32	adantr	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \underset{\_}{Ⅎ}yx$$
34	31 33	nfeqd	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎyw=x$$
35	7 34	nfan1	$$⊢Ⅎy\left(\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\wedge w=x\right)$$
36		nfcvd	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \underset{\_}{Ⅎ}zw$$
37		nfcvf2	$$⊢\neg \forall xx=z\to \underset{\_}{Ⅎ}zx$$
38	37	adantl	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \underset{\_}{Ⅎ}zx$$
39	36 38	nfeqd	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎzw=x$$
40	10 39	nfan1	$$⊢Ⅎz\left(\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\wedge w=x\right)$$
41		sbequ12r	$$⊢w=x\to \left(\left[w/x\right]\phi \leftrightarrow \phi \right)$$
42	41	imbi1d	$$⊢w=x\to \left(\left(\left[w/x\right]\phi \to z=y\right)\leftrightarrow \left(\phi \to z=y\right)\right)$$
43	42	adantl	$$⊢\left(\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\wedge w=x\right)\to \left(\left(\left[w/x\right]\phi \to z=y\right)\leftrightarrow \left(\phi \to z=y\right)\right)$$
44	40 43	albid	$$⊢\left(\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\wedge w=x\right)\to \left(\forall z\left(\left[w/x\right]\phi \to z=y\right)\leftrightarrow \forall z\left(\phi \to z=y\right)\right)$$
45	35 44	exbid	$$⊢\left(\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\wedge w=x\right)\to \left(\exists y\forall z\left(\left[w/x\right]\phi \to z=y\right)\leftrightarrow \exists y\forall z\left(\phi \to z=y\right)\right)$$
46		elequ2	$$⊢w=x\to \left(z\in w\leftrightarrow z\in x\right)$$
47	46	adantl	$$⊢\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)$$
48		elequ1	$$⊢w=x\to \left(w\in y\leftrightarrow x\in y\right)$$
49	48	adantl	$$⊢\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)$$
50	41	adantl	$$⊢\left(\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\wedge w=x\right)\to \left(\left[w/x\right]\phi \leftrightarrow \phi \right)$$
51	35 50	albid	$$⊢\left(\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\wedge w=x\right)\to \left(\forall y\left[w/x\right]\phi \leftrightarrow \forall y\phi \right)$$
52	49 51	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 y\left[w/x\right]\phi \right)\leftrightarrow \left(x\in y\wedge \forall y\phi \right)\right)$$
53	52	ex	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \left(w=x\to \left(\left(w\in y\wedge \forall y\left[w/x\right]\phi \right)\leftrightarrow \left(x\in y\wedge \forall y\phi \right)\right)\right)$$
54	4 26 53	cbvexd	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \left(\exists w\left(w\in y\wedge \forall y\left[w/x\right]\phi \right)\leftrightarrow \exists x\left(x\in y\wedge \forall y\phi \right)\right)$$
55	54	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 y\left[w/x\right]\phi \right)\leftrightarrow \exists x\left(x\in y\wedge \forall y\phi \right)\right)$$
56	47 55	bibi12d	$$⊢\left(\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\wedge w=x\right)\to \left(\left(z\in w\leftrightarrow \exists w\left(w\in y\wedge \forall y\left[w/x\right]\phi \right)\right)\leftrightarrow \left(z\in x\leftrightarrow \exists x\left(x\in y\wedge \forall y\phi \right)\right)\right)$$
57	40 56	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\leftrightarrow \exists w\left(w\in y\wedge \forall y\left[w/x\right]\phi \right)\right)\leftrightarrow \forall z\left(z\in x\leftrightarrow \exists x\left(x\in y\wedge \forall y\phi \right)\right)\right)$$
58	45 57	imbi12d	$$⊢\left(\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\wedge w=x\right)\to \left(\left(\exists y\forall z\left(\left[w/x\right]\phi \to z=y\right)\to \forall z\left(z\in w\leftrightarrow \exists w\left(w\in y\wedge \forall y\left[w/x\right]\phi \right)\right)\right)\leftrightarrow \left(\exists y\forall z\left(\phi \to z=y\right)\to \forall z\left(z\in x\leftrightarrow \exists x\left(x\in y\wedge \forall y\phi \right)\right)\right)\right)$$
59	58	ex	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \left(w=x\to \left(\left(\exists y\forall z\left(\left[w/x\right]\phi \to z=y\right)\to \forall z\left(z\in w\leftrightarrow \exists w\left(w\in y\wedge \forall y\left[w/x\right]\phi \right)\right)\right)\leftrightarrow \left(\exists y\forall z\left(\phi \to z=y\right)\to \forall z\left(z\in x\leftrightarrow \exists x\left(x\in y\wedge \forall y\phi \right)\right)\right)\right)\right)$$
60	4 30 59	cbvexd	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \left(\exists w\left(\exists y\forall z\left(\left[w/x\right]\phi \to z=y\right)\to \forall z\left(z\in w\leftrightarrow \exists w\left(w\in y\wedge \forall y\left[w/x\right]\phi \right)\right)\right)\leftrightarrow \exists x\left(\exists y\forall z\left(\phi \to z=y\right)\to \forall z\left(z\in x\leftrightarrow \exists x\left(x\in y\wedge \forall y\phi \right)\right)\right)\right)$$
61	1 60	syl5ib	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \left(\neg \forall yy=z\to \exists x\left(\exists y\forall z\left(\phi \to z=y\right)\to \forall z\left(z\in x\leftrightarrow \exists x\left(x\in y\wedge \forall y\phi \right)\right)\right)\right)$$
62	61	imp	$$⊢\left(\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\wedge \neg \forall yy=z\right)\to \exists x\left(\exists y\forall z\left(\phi \to z=y\right)\to \forall z\left(z\in x\leftrightarrow \exists x\left(x\in y\wedge \forall y\phi \right)\right)\right)$$