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

Metamath Proof Explorer

Theorem pwfi

Description: The power set of a finite set is finite and vice-versa. Theorem 38 of Suppes p. 104 and its converse, Theorem 40 of Suppes p. 105. (Contributed by NM, 26-Mar-2007) Avoid ax-pow . (Revised by BTernaryTau, 7-Sep-2024)

Ref Expression
Assertion pwfi 
|- ( A e. Fin <-> ~P A e. Fin )

Proof

Step Hyp Ref Expression
1 pweq 
 |-  ( x = (/) -> ~P x = ~P (/) )
2 1 eleq1d 
 |-  ( x = (/) -> ( ~P x e. Fin <-> ~P (/) e. Fin ) )
3 pweq 
 |-  ( x = y -> ~P x = ~P y )
4 3 eleq1d 
 |-  ( x = y -> ( ~P x e. Fin <-> ~P y e. Fin ) )
5 pweq 
 |-  ( x = ( y u. { z } ) -> ~P x = ~P ( y u. { z } ) )
6 5 eleq1d 
 |-  ( x = ( y u. { z } ) -> ( ~P x e. Fin <-> ~P ( y u. { z } ) e. Fin ) )
7 pweq 
 |-  ( x = A -> ~P x = ~P A )
8 7 eleq1d 
 |-  ( x = A -> ( ~P x e. Fin <-> ~P A e. Fin ) )
9 pw0 
 |-  ~P (/) = { (/) }
10 snfi 
 |-  { (/) } e. Fin
11 9 10 eqeltri 
 |-  ~P (/) e. Fin
12 eqid 
 |-  ( c e. ~P y |-> ( c u. { z } ) ) = ( c e. ~P y |-> ( c u. { z } ) )
13 12 pwfilem 
 |-  ( ~P y e. Fin -> ~P ( y u. { z } ) e. Fin )
14 13 a1i 
 |-  ( y e. Fin -> ( ~P y e. Fin -> ~P ( y u. { z } ) e. Fin ) )
15 2 4 6 8 11 14 findcard2 
 |-  ( A e. Fin -> ~P A e. Fin )
16 pwfir 
 |-  ( ~P A e. Fin -> A e. Fin )
17 15 16 impbii 
 |-  ( A e. Fin <-> ~P A e. Fin )