Theorem pwfir

Description: If the power set of a set is finite, then the set itself is finite. (Contributed by BTernaryTau, 7-Sep-2024)

	Ref	Expression
Assertion	pwfir	|- ( ~P B e. Fin -> B e. Fin )

Proof

Step	Hyp	Ref	Expression
1		df-ima	|- ( { <. x , y >. | ( x e. ~P B /\ { y } = x ) } " ~P B ) = ran ( { <. x , y >. | ( x e. ~P B /\ { y } = x ) } |` ~P B )
2		relopab	|- Rel { <. x , y >. | ( x e. ~P B /\ { y } = x ) }
3		dmopabss	|- dom { <. x , y >. | ( x e. ~P B /\ { y } = x ) } C_ ~P B
4		relssres	|- ( ( Rel { <. x , y >. | ( x e. ~P B /\ { y } = x ) } /\ dom { <. x , y >. | ( x e. ~P B /\ { y } = x ) } C_ ~P B ) -> ( { <. x , y >. | ( x e. ~P B /\ { y } = x ) } |` ~P B ) = { <. x , y >. | ( x e. ~P B /\ { y } = x ) } )
5	2 3 4	mp2an	|- ( { <. x , y >. | ( x e. ~P B /\ { y } = x ) } |` ~P B ) = { <. x , y >. | ( x e. ~P B /\ { y } = x ) }
6	5	rneqi	|- ran ( { <. x , y >. | ( x e. ~P B /\ { y } = x ) } |` ~P B ) = ran { <. x , y >. | ( x e. ~P B /\ { y } = x ) }
7		rnopab	|- ran { <. x , y >. | ( x e. ~P B /\ { y } = x ) } = { y | E. x ( x e. ~P B /\ { y } = x ) }
8		eleq1	|- ( { y } = x -> ( { y } e. ~P B <-> x e. ~P B ) )
9	8	biimparc	|- ( ( x e. ~P B /\ { y } = x ) -> { y } e. ~P B )
10		vex	|- y e. _V
11	10	snelpw	|- ( y e. B <-> { y } e. ~P B )
12	9 11	sylibr	|- ( ( x e. ~P B /\ { y } = x ) -> y e. B )
13	12	exlimiv	|- ( E. x ( x e. ~P B /\ { y } = x ) -> y e. B )
14		snelpwi	|- ( y e. B -> { y } e. ~P B )
15		eqid	|- { y } = { y }
16		eqeq2	|- ( x = { y } -> ( { y } = x <-> { y } = { y } ) )
17	16	rspcev	|- ( ( { y } e. ~P B /\ { y } = { y } ) -> E. x e. ~P B { y } = x )
18	14 15 17	sylancl	|- ( y e. B -> E. x e. ~P B { y } = x )
19		df-rex	|- ( E. x e. ~P B { y } = x <-> E. x ( x e. ~P B /\ { y } = x ) )
20	18 19	sylib	|- ( y e. B -> E. x ( x e. ~P B /\ { y } = x ) )
21	13 20	impbii	|- ( E. x ( x e. ~P B /\ { y } = x ) <-> y e. B )
22	21	abbii	|- { y | E. x ( x e. ~P B /\ { y } = x ) } = { y | y e. B }
23		abid2	|- { y | y e. B } = B
24	7 22 23	3eqtri	|- ran { <. x , y >. | ( x e. ~P B /\ { y } = x ) } = B
25	1 6 24	3eqtri	|- ( { <. x , y >. | ( x e. ~P B /\ { y } = x ) } " ~P B ) = B
26		funopab	|- ( Fun { <. x , y >. | ( x e. ~P B /\ { y } = x ) } <-> A. x E* y ( x e. ~P B /\ { y } = x ) )
27		mosneq	|- E* y { y } = x
28	27	moani	|- E* y ( x e. ~P B /\ { y } = x )
29	26 28	mpgbir	|- Fun { <. x , y >. | ( x e. ~P B /\ { y } = x ) }
30		imafi	|- ( ( Fun { <. x , y >. | ( x e. ~P B /\ { y } = x ) } /\ ~P B e. Fin ) -> ( { <. x , y >. | ( x e. ~P B /\ { y } = x ) } " ~P B ) e. Fin )
31	29 30	mpan	|- ( ~P B e. Fin -> ( { <. x , y >. | ( x e. ~P B /\ { y } = x ) } " ~P B ) e. Fin )
32	25 31	eqeltrrid	|- ( ~P B e. Fin -> B e. Fin )