Theorem fineqvpow

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

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

Proof

Step	Hyp	Ref	Expression
1		df-pw	$$⊢𝒫x=\left\{v|v\subseteq x\right\}$$
2		vex	$$⊢x\in \mathrm{V}$$
3		eleq2w2	$$⊢\mathrm{Fin}=\mathrm{V}\to \left(x\in \mathrm{Fin}\leftrightarrow x\in \mathrm{V}\right)$$
4		pwfi	$$⊢x\in \mathrm{Fin}\leftrightarrow 𝒫x\in \mathrm{Fin}$$
5	3 4	bitr3di	$$⊢\mathrm{Fin}=\mathrm{V}\to \left(x\in \mathrm{V}\leftrightarrow 𝒫x\in \mathrm{Fin}\right)$$
6	2 5	mpbii	$$⊢\mathrm{Fin}=\mathrm{V}\to 𝒫x\in \mathrm{Fin}$$
7	6	elexd	$$⊢\mathrm{Fin}=\mathrm{V}\to 𝒫x\in \mathrm{V}$$
8	1 7	eqeltrrid	$$⊢\mathrm{Fin}=\mathrm{V}\to \left\{v|v\subseteq x\right\}\in \mathrm{V}$$
9		elisset	$$⊢\left\{v|v\subseteq x\right\}\in \mathrm{V}\to \exists yy=\left\{v|v\subseteq x\right\}$$
10	8 9	syl	$$⊢\mathrm{Fin}=\mathrm{V}\to \exists yy=\left\{v|v\subseteq x\right\}$$
11		sseq1	$$⊢v=z\to \left(v\subseteq x\leftrightarrow z\subseteq x\right)$$
12	11	eqabbw	$$⊢y=\left\{v|v\subseteq x\right\}\leftrightarrow \forall z\left(z\in y\leftrightarrow z\subseteq x\right)$$
13	12	exbii	$$⊢\exists yy=\left\{v|v\subseteq x\right\}\leftrightarrow \exists y\forall z\left(z\in y\leftrightarrow z\subseteq x\right)$$
14	10 13	sylib	$$⊢\mathrm{Fin}=\mathrm{V}\to \exists y\forall z\left(z\in y\leftrightarrow z\subseteq x\right)$$
15		biimpr	$$⊢\left(z\in y\leftrightarrow z\subseteq x\right)\to \left(z\subseteq x\to z\in y\right)$$
16	15	alimi	$$⊢\forall z\left(z\in y\leftrightarrow z\subseteq x\right)\to \forall z\left(z\subseteq x\to z\in y\right)$$
17	16	eximi	$$⊢\exists y\forall z\left(z\in y\leftrightarrow z\subseteq x\right)\to \exists y\forall z\left(z\subseteq x\to z\in y\right)$$
18	14 17	syl	$$⊢\mathrm{Fin}=\mathrm{V}\to \exists y\forall z\left(z\subseteq x\to z\in y\right)$$
19		dfss2	$$⊢z\subseteq x\leftrightarrow \forall w\left(w\in z\to w\in x\right)$$
20	19	imbi1i	$$⊢\left(z\subseteq x\to z\in y\right)\leftrightarrow \left(\forall w\left(w\in z\to w\in x\right)\to z\in y\right)$$
21	20	albii	$$⊢\forall z\left(z\subseteq x\to z\in y\right)\leftrightarrow \forall z\left(\forall w\left(w\in z\to w\in x\right)\to z\in y\right)$$
22	21	exbii	$$⊢\exists y\forall z\left(z\subseteq x\to z\in y\right)\leftrightarrow \exists y\forall z\left(\forall w\left(w\in z\to w\in x\right)\to z\in y\right)$$
23	18 22	sylib	$$⊢\mathrm{Fin}=\mathrm{V}\to \exists y\forall z\left(\forall w\left(w\in z\to w\in x\right)\to z\in y\right)$$