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)

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

Proof

Step	Hyp	Ref	Expression
1		isfi	|- ( A e. Fin <-> E. m e. _om A ~~ m )
2		pweq	|- ( m = (/) -> ~P m = ~P (/) )
3	2	eleq1d	|- ( m = (/) -> ( ~P m e. Fin <-> ~P (/) e. Fin ) )
4		pweq	|- ( m = k -> ~P m = ~P k )
5	4	eleq1d	|- ( m = k -> ( ~P m e. Fin <-> ~P k e. Fin ) )
6		pweq	|- ( m = suc k -> ~P m = ~P suc k )
7		df-suc	|- suc k = ( k u. { k } )
8	7	pweqi	|- ~P suc k = ~P ( k u. { k } )
9	6 8	syl6eq	|- ( m = suc k -> ~P m = ~P ( k u. { k } ) )
10	9	eleq1d	|- ( m = suc k -> ( ~P m e. Fin <-> ~P ( k u. { k } ) e. Fin ) )
11		pw0	|- ~P (/) = { (/) }
12		df1o2	|- 1o = { (/) }
13	11 12	eqtr4i	|- ~P (/) = 1o
14		1onn	|- 1o e. _om
15		ssid	|- 1o C_ 1o
16		ssnnfi	|- ( ( 1o e. _om /\ 1o C_ 1o ) -> 1o e. Fin )
17	14 15 16	mp2an	|- 1o e. Fin
18	13 17	eqeltri	|- ~P (/) e. Fin
19		eqid	|- ( c e. ~P k |-> ( c u. { k } ) ) = ( c e. ~P k |-> ( c u. { k } ) )
20	19	pwfilem	|- ( ~P k e. Fin -> ~P ( k u. { k } ) e. Fin )
21	20	a1i	|- ( k e. _om -> ( ~P k e. Fin -> ~P ( k u. { k } ) e. Fin ) )
22	3 5 10 18 21	finds1	|- ( m e. _om -> ~P m e. Fin )
23		pwen	|- ( A ~~ m -> ~P A ~~ ~P m )
24		enfii	|- ( ( ~P m e. Fin /\ ~P A ~~ ~P m ) -> ~P A e. Fin )
25	22 23 24	syl2an	|- ( ( m e. _om /\ A ~~ m ) -> ~P A e. Fin )
26	25	rexlimiva	|- ( E. m e. _om A ~~ m -> ~P A e. Fin )
27	1 26	sylbi	|- ( A e. Fin -> ~P A e. Fin )
28		pwexr	|- ( ~P A e. Fin -> A e. _V )
29		canth2g	|- ( A e. _V -> A ~< ~P A )
30		sdomdom	|- ( A ~< ~P A -> A ~<_ ~P A )
31	28 29 30	3syl	|- ( ~P A e. Fin -> A ~<_ ~P A )
32		domfi	|- ( ( ~P A e. Fin /\ A ~<_ ~P A ) -> A e. Fin )
33	31 32	mpdan	|- ( ~P A e. Fin -> A e. Fin )
34	27 33	impbii	|- ( A e. Fin <-> ~P A e. Fin )