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 )