This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )