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	|- ( Fin = _V -> E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y ) )

Proof

Step	Hyp	Ref	Expression
1		df-pw	|- ~P x = { v | v C_ x }
2		vex	|- x e. _V
3		eleq2w2	|- ( Fin = _V -> ( x e. Fin <-> x e. _V ) )
4		pwfi	|- ( x e. Fin <-> ~P x e. Fin )
5	3 4	bitr3di	|- ( Fin = _V -> ( x e. _V <-> ~P x e. Fin ) )
6	2 5	mpbii	|- ( Fin = _V -> ~P x e. Fin )
7	6	elexd	|- ( Fin = _V -> ~P x e. _V )
8	1 7	eqeltrrid	|- ( Fin = _V -> { v | v C_ x } e. _V )
9		elisset	|- ( { v | v C_ x } e. _V -> E. y y = { v | v C_ x } )
10	8 9	syl	|- ( Fin = _V -> E. y y = { v | v C_ x } )
11		sseq1	|- ( v = z -> ( v C_ x <-> z C_ x ) )
12	11	abeq2w	|- ( y = { v | v C_ x } <-> A. z ( z e. y <-> z C_ x ) )
13	12	exbii	|- ( E. y y = { v | v C_ x } <-> E. y A. z ( z e. y <-> z C_ x ) )
14	10 13	sylib	|- ( Fin = _V -> E. y A. z ( z e. y <-> z C_ x ) )
15		biimpr	|- ( ( z e. y <-> z C_ x ) -> ( z C_ x -> z e. y ) )
16	15	alimi	|- ( A. z ( z e. y <-> z C_ x ) -> A. z ( z C_ x -> z e. y ) )
17	16	eximi	|- ( E. y A. z ( z e. y <-> z C_ x ) -> E. y A. z ( z C_ x -> z e. y ) )
18	14 17	syl	|- ( Fin = _V -> E. y A. z ( z C_ x -> z e. y ) )
19		dfss2	|- ( z C_ x <-> A. w ( w e. z -> w e. x ) )
20	19	imbi1i	|- ( ( z C_ x -> z e. y ) <-> ( A. w ( w e. z -> w e. x ) -> z e. y ) )
21	20	albii	|- ( A. z ( z C_ x -> z e. y ) <-> A. z ( A. w ( w e. z -> w e. x ) -> z e. y ) )
22	21	exbii	|- ( E. y A. z ( z C_ x -> z e. y ) <-> E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y ) )
23	18 22	sylib	|- ( Fin = _V -> E. y A. z ( A. w ( w e. z -> w e. x ) -> z e. y ) )