Theorem pwfi 7807

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 7532	. . 3 |- ( A e. Fin <-> E. m e. om A ~~ m )
2		pweq 4002	. . . . . . 7 |- ( m = (/) -> ~P m = ~P (/) )
3	2	eleq1d 2523	. . . . . 6 |- ( m = (/) -> ( ~P m e. Fin <-> ~P (/) e. Fin ) )
4		pweq 4002	. . . . . . 7 |- ( m = k -> ~P m = ~P k )
5	4	eleq1d 2523	. . . . . 6 |- ( m = k -> ( ~P m e. Fin <-> ~P k e. Fin ) )
6		pweq 4002	. . . . . . . 8 |- ( m = suc k -> ~P m = ~P suc k )
7		df-suc 4873	. . . . . . . . 9 |- suc k = ( k u. { k } )
8	7	pweqi 4003	. . . . . . . 8 |- ~P suc k = ~P ( k u. { k } )
9	6, 8	syl6eq 2511	. . . . . . 7 |- ( m = suc k -> ~P m = ~P ( k u. { k } ) )
10	9	eleq1d 2523	. . . . . 6 |- ( m = suc k -> ( ~P m e. Fin <-> ~P ( k u. { k } ) e. Fin ) )
11		pw0 4163	. . . . . . . 8 |- ~P (/) = { (/) }
12		df1o2 7134	. . . . . . . 8 |- 1o = { (/) }
13	11, 12	eqtr4i 2486	. . . . . . 7 |- ~P (/) = 1o
14		1onn 7280	. . . . . . . 8 |- 1o e. om
15		ssid 3508	. . . . . . . 8 |- 1o C_ 1o
16		ssnnfi 7732	. . . . . . . 8 |- ( ( 1o e. om /\ 1o C_ 1o ) -> 1o e. Fin )
17	14, 15, 16	mp2an 670	. . . . . . 7 |- 1o e. Fin
18	13, 17	eqeltri 2538	. . . . . 6 |- ~P (/) e. Fin
19		eqid 2454	. . . . . . . 8 |- ( c e. ~P k |-> ( c u. { k } ) ) = ( c e. ~P k |-> ( c u. { k } ) )
20	19	pwfilem 7806	. . . . . . 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 6702	. . . . 5 |- ( m e. om -> ~P m e. Fin )
23		pwen 7683	. . . . 5 |- ( A ~~ m -> ~P A ~~ ~P m )
24		enfii 7730	. . . . 5 |- ( ( ~P m e. Fin /\ ~P A ~~ ~P m ) -> ~P A e. Fin )
25	22, 23, 24	syl2an 475	. . . 4 |- ( ( m e. om /\ A ~~ m ) -> ~P A e. Fin )
26	25	rexlimiva 2942	. . 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 3115	. . . . 5 |- ( ~P A e. Fin -> ~P A e. _V )
29		pwexb 6584	. . . . 5 |- ( A e. _V <-> ~P A e. _V )
30	28, 29	sylibr 212	. . . 4 |- ( ~P A e. Fin -> A e. _V )
31		canth2g 7664	. . . 4 |- ( A e. _V -> A ~< ~P A )
32		sdomdom 7536	. . . 4 |- ( A ~< ~P A -> A ~<_ ~P A )
33	30, 31, 32	3syl 20	. . 3 |- ( ~P A e. Fin -> A ~<_ ~P A )
34		domfi 7734	. . 3 |- ( ( ~P A e. Fin /\ A ~<_ ~P A ) -> A e. Fin )
35	33, 34	mpdan 666	. 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 1398   e. wcel 1823   E.wrex 2805   _Vcvv 3106   u. cun 3459   C_ wss 3461   (/)c0 3783   ~Pcpw 3999   {csn 4016   class class class wbr 4439   |-> cmpt 4497   suc csuc 4869   omcom 6673   1oc1o 7115   ~~ cen 7506   ~<_ cdom 7507   ~< csdm 7508   Fincfn 7509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-int 4272  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-om 6674  df-1st 6773  df-2nd 6774  df-recs 7034  df-rdg 7068  df-1o 7122  df-2o 7123  df-oadd 7126  df-er 7303  df-map 7414  df-en 7510  df-dom 7511  df-sdom 7512  df-fin 7513

This theorem is referenced by:  mapfi  7808  r1fin  8182  dfac12k  8518  pwsdompw  8575  ackbij1lem5  8595  ackbij1lem9  8599  ackbij1lem10  8600  ackbij1lem14  8604  ackbij1b  8610  isfin1-2  8756  isfin1-3  8757  domtriomlem  8813  dominf  8816  dominfac  8939  gchhar  9046  omina  9058  gchina  9066  hashpw  12478  hashbclem  12485  qshash  13721  ackbijnn  13722  incexclem  13730  incexc  13731  incexc2  13732  hashbccl  14605  lagsubg2  16461  lagsubg  16462  orbsta2  16551  sylow1lem3  16819  sylow1lem5  16821  sylow2alem2  16837  sylow2a  16838  sylow2blem2  16840  sylow2blem3  16841  sylow3lem3  16848  sylow3lem4  16849  sylow3lem6  16851  pgpfac1lem5  17325  discmp  20065  cmpfi  20075  dis1stc  20166  1stckgenlem  20220  ptcmpfi  20480  fiufl  20583  musum  23665  qerclwwlknfi  25031  hasheuni  28314  coinfliplem  28681  ballotth  28740  erdszelem2  28900  kelac2lem  31249  pwinfig  38159