Theorem fineqvrep

Description: If the Axiom of Infinity is negated, then the Axiom of Replacement becomes redundant. (Contributed by BTernaryTau, 12-Sep-2024)

	Ref	Expression
Assertion	fineqvrep	$$⊢\mathrm{Fin}=\mathrm{V}\to \left(\forall w\exists y\forall z\left(\forall y\phi \to z=y\right)\to \exists y\forall z\left(z\in y\leftrightarrow \exists w\left(w\in x\wedge \forall y\phi \right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		funopab	$$⊢\mathrm{Fun}\left\{⟨w,z⟩|\forall y\phi \right\}\leftrightarrow \forall w{\exists }^{*}z\forall y\phi$$
2		nfa1	$$⊢Ⅎy\forall y\phi$$
3	2	mof	$$⊢{\exists }^{*}z\forall y\phi \leftrightarrow \exists y\forall z\left(\forall y\phi \to z=y\right)$$
4	3	albii	$$⊢\forall w{\exists }^{*}z\forall y\phi \leftrightarrow \forall w\exists y\forall z\left(\forall y\phi \to z=y\right)$$
5	1 4	bitr2i	$$⊢\forall w\exists y\forall z\left(\forall y\phi \to z=y\right)\leftrightarrow \mathrm{Fun}\left\{⟨w,z⟩|\forall y\phi \right\}$$
6		vex	$$⊢x\in \mathrm{V}$$
7		eleq2w2	$$⊢\mathrm{Fin}=\mathrm{V}\to \left(x\in \mathrm{Fin}\leftrightarrow x\in \mathrm{V}\right)$$
8	6 7	mpbiri	$$⊢\mathrm{Fin}=\mathrm{V}\to x\in \mathrm{Fin}$$
9		imafi	$$⊢\left(\mathrm{Fun}\left\{⟨w,z⟩|\forall y\phi \right\}\wedge x\in \mathrm{Fin}\right)\to \left\{⟨w,z⟩|\forall y\phi \right\}\left[x\right]\in \mathrm{Fin}$$
10	8 9	sylan2	$$⊢\left(\mathrm{Fun}\left\{⟨w,z⟩|\forall y\phi \right\}\wedge \mathrm{Fin}=\mathrm{V}\right)\to \left\{⟨w,z⟩|\forall y\phi \right\}\left[x\right]\in \mathrm{Fin}$$
11	10	elexd	$$⊢\left(\mathrm{Fun}\left\{⟨w,z⟩|\forall y\phi \right\}\wedge \mathrm{Fin}=\mathrm{V}\right)\to \left\{⟨w,z⟩|\forall y\phi \right\}\left[x\right]\in \mathrm{V}$$
12		nfv	$$⊢Ⅎyw\in x$$
13	2	nfopab	$$⊢\underset{\_}{Ⅎ}y\left\{⟨w,z⟩|\forall y\phi \right\}$$
14	13	nfel2	$$⊢Ⅎy⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}$$
15	12 14	nfan	$$⊢Ⅎy\left(w\in x\wedge ⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)$$
16	15	nfex	$$⊢Ⅎy\exists w\left(w\in x\wedge ⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)$$
17	16	nfab	$$⊢\underset{\_}{Ⅎ}y\left\{z|\exists w\left(w\in x\wedge ⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\right\}$$
18	17	issetf	$$⊢\left\{z|\exists w\left(w\in x\wedge ⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\right\}\in \mathrm{V}\leftrightarrow \exists yy=\left\{z|\exists w\left(w\in x\wedge ⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\right\}$$
19		eqabb	$$⊢y=\left\{z|\exists w\left(w\in x\wedge ⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\right\}\leftrightarrow \forall z\left(z\in y\leftrightarrow \exists w\left(w\in x\wedge ⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\right)$$
20	19	exbii	$$⊢\exists yy=\left\{z|\exists w\left(w\in x\wedge ⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\right\}\leftrightarrow \exists y\forall z\left(z\in y\leftrightarrow \exists w\left(w\in x\wedge ⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\right)$$
21		opabidw	$$⊢⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\leftrightarrow \forall y\phi$$
22	21	anbi2i	$$⊢\left(w\in x\wedge ⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\leftrightarrow \left(w\in x\wedge \forall y\phi \right)$$
23	22	exbii	$$⊢\exists w\left(w\in x\wedge ⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\leftrightarrow \exists w\left(w\in x\wedge \forall y\phi \right)$$
24	23	bibi2i	$$⊢\left(z\in y\leftrightarrow \exists w\left(w\in x\wedge ⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\right)\leftrightarrow \left(z\in y\leftrightarrow \exists w\left(w\in x\wedge \forall y\phi \right)\right)$$
25	24	albii	$$⊢\forall z\left(z\in y\leftrightarrow \exists w\left(w\in x\wedge ⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\right)\leftrightarrow \forall z\left(z\in y\leftrightarrow \exists w\left(w\in x\wedge \forall y\phi \right)\right)$$
26	25	exbii	$$⊢\exists y\forall z\left(z\in y\leftrightarrow \exists w\left(w\in x\wedge ⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\right)\leftrightarrow \exists y\forall z\left(z\in y\leftrightarrow \exists w\left(w\in x\wedge \forall y\phi \right)\right)$$
27	18 20 26	3bitrri	$$⊢\exists y\forall z\left(z\in y\leftrightarrow \exists w\left(w\in x\wedge \forall y\phi \right)\right)\leftrightarrow \left\{z|\exists w\left(w\in x\wedge ⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\right\}\in \mathrm{V}$$
28		dfima3	$$⊢\left\{⟨w,z⟩|\forall y\phi \right\}\left[x\right]=\left\{v|\exists u\left(u\in x\wedge ⟨u,v⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\right\}$$
29		nfv	$$⊢Ⅎzu\in x$$
30		nfopab2	$$⊢\underset{\_}{Ⅎ}z\left\{⟨w,z⟩|\forall y\phi \right\}$$
31	30	nfel2	$$⊢Ⅎz⟨u,v⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}$$
32	29 31	nfan	$$⊢Ⅎz\left(u\in x\wedge ⟨u,v⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)$$
33	32	nfex	$$⊢Ⅎz\exists u\left(u\in x\wedge ⟨u,v⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)$$
34		nfv	$$⊢Ⅎv\exists w\left(w\in x\wedge ⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)$$
35		nfv	$$⊢Ⅎwu\in x$$
36		nfopab1	$$⊢\underset{\_}{Ⅎ}w\left\{⟨w,z⟩|\forall y\phi \right\}$$
37	36	nfel2	$$⊢Ⅎw⟨u,v⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}$$
38	35 37	nfan	$$⊢Ⅎw\left(u\in x\wedge ⟨u,v⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)$$
39		nfv	$$⊢Ⅎu\left(w\in x\wedge ⟨w,v⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)$$
40		elequ1	$$⊢u=w\to \left(u\in x\leftrightarrow w\in x\right)$$
41		opeq1	$$⊢u=w\to ⟨u,v⟩=⟨w,v⟩$$
42	41	eleq1d	$$⊢u=w\to \left(⟨u,v⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\leftrightarrow ⟨w,v⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)$$
43	40 42	anbi12d	$$⊢u=w\to \left(\left(u\in x\wedge ⟨u,v⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\leftrightarrow \left(w\in x\wedge ⟨w,v⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\right)$$
44	38 39 43	cbvexv1	$$⊢\exists u\left(u\in x\wedge ⟨u,v⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\leftrightarrow \exists w\left(w\in x\wedge ⟨w,v⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)$$
45		opeq2	$$⊢v=z\to ⟨w,v⟩=⟨w,z⟩$$
46	45	eleq1d	$$⊢v=z\to \left(⟨w,v⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\leftrightarrow ⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)$$
47	46	anbi2d	$$⊢v=z\to \left(\left(w\in x\wedge ⟨w,v⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\leftrightarrow \left(w\in x\wedge ⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\right)$$
48	47	exbidv	$$⊢v=z\to \left(\exists w\left(w\in x\wedge ⟨w,v⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\leftrightarrow \exists w\left(w\in x\wedge ⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\right)$$
49	44 48	bitrid	$$⊢v=z\to \left(\exists u\left(u\in x\wedge ⟨u,v⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\leftrightarrow \exists w\left(w\in x\wedge ⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\right)$$
50	33 34 49	cbvabw	$$⊢\left\{v|\exists u\left(u\in x\wedge ⟨u,v⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\right\}=\left\{z|\exists w\left(w\in x\wedge ⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\right\}$$
51	28 50	eqtri	$$⊢\left\{⟨w,z⟩|\forall y\phi \right\}\left[x\right]=\left\{z|\exists w\left(w\in x\wedge ⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\right\}$$
52	51	eleq1i	$$⊢\left\{⟨w,z⟩|\forall y\phi \right\}\left[x\right]\in \mathrm{V}\leftrightarrow \left\{z|\exists w\left(w\in x\wedge ⟨w,z⟩\in \left\{⟨w,z⟩|\forall y\phi \right\}\right)\right\}\in \mathrm{V}$$
53	27 52	bitr4i	$$⊢\exists y\forall z\left(z\in y\leftrightarrow \exists w\left(w\in x\wedge \forall y\phi \right)\right)\leftrightarrow \left\{⟨w,z⟩|\forall y\phi \right\}\left[x\right]\in \mathrm{V}$$
54	11 53	sylibr	$$⊢\left(\mathrm{Fun}\left\{⟨w,z⟩|\forall y\phi \right\}\wedge \mathrm{Fin}=\mathrm{V}\right)\to \exists y\forall z\left(z\in y\leftrightarrow \exists w\left(w\in x\wedge \forall y\phi \right)\right)$$
55	5 54	sylanb	$$⊢\left(\forall w\exists y\forall z\left(\forall y\phi \to z=y\right)\wedge \mathrm{Fin}=\mathrm{V}\right)\to \exists y\forall z\left(z\in y\leftrightarrow \exists w\left(w\in x\wedge \forall y\phi \right)\right)$$
56	55	expcom	$$⊢\mathrm{Fin}=\mathrm{V}\to \left(\forall w\exists y\forall z\left(\forall y\phi \to z=y\right)\to \exists y\forall z\left(z\in y\leftrightarrow \exists w\left(w\in x\wedge \forall y\phi \right)\right)\right)$$