Theorem pwfi 7596

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.)

Assertion

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

Proof of Theorem pwfi

Dummy variables m k c are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isfi 7323	. . 3 |- ( A e. Fin <-> E. m e. om A ~~ m )
2		pweq 3853	. . . . . . 7 |- ( m = (/) -> ~P m = ~P (/) )
3	2	eleq1d 2501	. . . . . 6 |- ( m = (/) -> ( ~P m e. Fin <-> ~P (/) e. Fin ) )
4		pweq 3853	. . . . . . 7 |- ( m = k -> ~P m = ~P k )
5	4	eleq1d 2501	. . . . . 6 |- ( m = k -> ( ~P m e. Fin <-> ~P k e. Fin ) )
6		pweq 3853	. . . . . . . 8 |- ( m = suc k -> ~P m = ~P suc k )
7		df-suc 4714	. . . . . . . . 9 |- suc k = ( k u. { k } )
8	7	pweqi 3854	. . . . . . . 8 |- ~P suc k = ~P ( k u. { k } )
9	6, 8	syl6eq 2483	. . . . . . 7 |- ( m = suc k -> ~P m = ~P ( k u. { k } ) )
10	9	eleq1d 2501	. . . . . 6 |- ( m = suc k -> ( ~P m e. Fin <-> ~P ( k u. { k } ) e. Fin ) )
11		pw0 4010	. . . . . . . 8 |- ~P (/) = { (/) }
12		df1o2 6922	. . . . . . . 8 |- 1o = { (/) }
13	11, 12	eqtr4i 2458	. . . . . . 7 |- ~P (/) = 1o
14		1onn 7068	. . . . . . . 8 |- 1o e. om
15		ssid 3365	. . . . . . . 8 |- 1o C_ 1o
16		ssnnfi 7522	. . . . . . . 8 |- ( ( 1o e. om /\ 1o C_ 1o ) -> 1o e. Fin )
17	14, 15, 16	mp2an 667	. . . . . . 7 |- 1o e. Fin
18	13, 17	eqeltri 2505	. . . . . 6 |- ~P (/) e. Fin
19		eqid 2435	. . . . . . . 8 |- ( c e. ~P k |-> ( c u. { k } ) ) = ( c e. ~P k |-> ( c u. { k } ) )
20	19	pwfilem 7595	. . . . . . 7 |- ( ~P k e. Fin -> ~P ( k u. { k } ) e. Fin )
21	20	a1i 11	. . . . . 6 |- ( k e. om -> ( ~P k e. Fin -> ~P ( k u. { k } ) e. Fin ) )
22	3, 5, 10, 18, 21	finds1 6496	. . . . 5 |- ( m e. om -> ~P m e. Fin )
23		pwen 7474	. . . . 5 |- ( A ~~ m -> ~P A ~~ ~P m )
24		enfii 7520	. . . . 5 |- ( ( ~P m e. Fin /\ ~P A ~~ ~P m ) -> ~P A e. Fin )
25	22, 23, 24	syl2an 474	. . . 4 |- ( ( m e. om /\ A ~~ m ) -> ~P A e. Fin )
26	25	rexlimiva 2828	. . 3 |- ( E. m e. om A ~~ m -> ~P A e. Fin )
27	1, 26	sylbi 195	. 2 |- ( A e. Fin -> ~P A e. Fin )
28		elex 2973	. . . . 5 |- ( ~P A e. Fin -> ~P A e. _V )
29		pwexb 6378	. . . . 5 |- ( A e. _V <-> ~P A e. _V )
30	28, 29	sylibr 212	. . . 4 |- ( ~P A e. Fin -> A e. _V )
31		canth2g 7455	. . . 4 |- ( A e. _V -> A ~< ~P A )
32		sdomdom 7327	. . . 4 |- ( A ~< ~P A -> A ~<_ ~P A )
33	30, 31, 32	3syl 20	. . 3 |- ( ~P A e. Fin -> A ~<_ ~P A )
34		domfi 7524	. . 3 |- ( ( ~P A e. Fin /\ A ~<_ ~P A ) -> A e. Fin )
35	33, 34	mpdan 663	. 2 |- ( ~P A e. Fin -> A e. Fin )
36	27, 35	impbii 188	1 |- ( A e. Fin <-> ~P A e. Fin )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1364   e. wcel 1757   E.wrex 2708   _Vcvv 2964   u. cun 3316   C_ wss 3318   (/)c0 3627   ~Pcpw 3850   {csn 3867   class class class wbr 4282   e. cmpt 4340   suc csuc 4710   omcom 6467   1oc1o 6903   ~~ cen 7297   ~<_ cdom 7298   ~< csdm 7299   Fincfn 7300

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2966  df-sbc 3178  df-csb 3279  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-pss 3334  df-nul 3628  df-if 3782  df-pw 3852  df-sn 3868  df-pr 3870  df-tp 3872  df-op 3874  df-uni 4082  df-int 4119  df-iun 4163  df-br 4283  df-opab 4341  df-mpt 4342  df-tr 4376  df-eprel 4621  df-id 4625  df-po 4630  df-so 4631  df-fr 4668  df-we 4670  df-ord 4711  df-on 4712  df-lim 4713  df-suc 4714  df-xp 4835  df-rel 4836  df-cnv 4837  df-co 4838  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842  df-iota 5371  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-om 6468  df-1st 6568  df-2nd 6569  df-recs 6820  df-rdg 6854  df-1o 6910  df-2o 6911  df-oadd 6914  df-er 7091  df-map 7206  df-en 7301  df-dom 7302  df-sdom 7303  df-fin 7304

This theorem is referenced by:  mapfi  7597  r1fin  7970  dfac12k  8306  pwsdompw  8363  ackbij1lem5  8383  ackbij1lem9  8387  ackbij1lem10  8388  ackbij1lem14  8392  ackbij1b  8398  isfin1-2  8544  isfin1-3  8545  domtriomlem  8601  dominf  8604  dominfac  8727  gchhar  8836  omina  8848  gchina  8856  hashpw  12184  hashbclem  12191  qshash  13275  ackbijnn  13276  incexclem  13284  incexc  13285  incexc2  13286  hashbccl  14049  lagsubg2  15724  lagsubg  15725  orbsta2  15814  sylow1lem3  16081  sylow1lem5  16083  sylow2alem2  16099  sylow2a  16100  sylow2blem2  16102  sylow2blem3  16103  sylow3lem3  16110  sylow3lem4  16111  sylow3lem6  16113  pgpfac1lem5  16556  discmp  18845  cmpfi  18855  dis1stc  18947  1stckgenlem  18970  ptcmpfi  19230  fiufl  19333  musum  22418  hasheuni  26390  coinfliplem  26711  ballotth  26770  erdszelem2  26930  kelac2lem  29264  qerclwwlknfi  30351