Theorem pwfi 7895

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 7619	. . 3 |- ( A e. Fin <-> E. m e. om A ~~ m )
2		pweq 3966	. . . . . . 7 |- ( m = (/) -> ~P m = ~P (/) )
3	2	eleq1d 2524	. . . . . 6 |- ( m = (/) -> ( ~P m e. Fin <-> ~P (/) e. Fin ) )
4		pweq 3966	. . . . . . 7 |- ( m = k -> ~P m = ~P k )
5	4	eleq1d 2524	. . . . . 6 |- ( m = k -> ( ~P m e. Fin <-> ~P k e. Fin ) )
6		pweq 3966	. . . . . . . 8 |- ( m = suc k -> ~P m = ~P suc k )
7		df-suc 5448	. . . . . . . . 9 |- suc k = ( k u. { k } )
8	7	pweqi 3967	. . . . . . . 8 |- ~P suc k = ~P ( k u. { k } )
9	6, 8	syl6eq 2512	. . . . . . 7 |- ( m = suc k -> ~P m = ~P ( k u. { k } ) )
10	9	eleq1d 2524	. . . . . 6 |- ( m = suc k -> ( ~P m e. Fin <-> ~P ( k u. { k } ) e. Fin ) )
11		pw0 4132	. . . . . . . 8 |- ~P (/) = { (/) }
12		df1o2 7220	. . . . . . . 8 |- 1o = { (/) }
13	11, 12	eqtr4i 2487	. . . . . . 7 |- ~P (/) = 1o
14		1onn 7366	. . . . . . . 8 |- 1o e. om
15		ssid 3463	. . . . . . . 8 |- 1o C_ 1o
16		ssnnfi 7817	. . . . . . . 8 |- ( ( 1o e. om /\ 1o C_ 1o ) -> 1o e. Fin )
17	14, 15, 16	mp2an 683	. . . . . . 7 |- 1o e. Fin
18	13, 17	eqeltri 2536	. . . . . 6 |- ~P (/) e. Fin
19		eqid 2462	. . . . . . . 8 |- ( c e. ~P k |-> ( c u. { k } ) ) = ( c e. ~P k |-> ( c u. { k } ) )
20	19	pwfilem 7894	. . . . . . 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 6749	. . . . 5 |- ( m e. om -> ~P m e. Fin )
23		pwen 7771	. . . . 5 |- ( A ~~ m -> ~P A ~~ ~P m )
24		enfii 7815	. . . . 5 |- ( ( ~P m e. Fin /\ ~P A ~~ ~P m ) -> ~P A e. Fin )
25	22, 23, 24	syl2an 484	. . . 4 |- ( ( m e. om /\ A ~~ m ) -> ~P A e. Fin )
26	25	rexlimiva 2887	. . 3 |- ( E. m e. om A ~~ m -> ~P A e. Fin )
27	1, 26	sylbi 200	. 2 |- ( A e. Fin -> ~P A e. Fin )
28		elex 3066	. . . . 5 |- ( ~P A e. Fin -> ~P A e. _V )
29		pwexb 6629	. . . . 5 |- ( A e. _V <-> ~P A e. _V )
30	28, 29	sylibr 217	. . . 4 |- ( ~P A e. Fin -> A e. _V )
31		canth2g 7752	. . . 4 |- ( A e. _V -> A ~< ~P A )
32		sdomdom 7623	. . . 4 |- ( A ~< ~P A -> A ~<_ ~P A )
33	30, 31, 32	3syl 18	. . 3 |- ( ~P A e. Fin -> A ~<_ ~P A )
34		domfi 7819	. . 3 |- ( ( ~P A e. Fin /\ A ~<_ ~P A ) -> A e. Fin )
35	33, 34	mpdan 679	. 2 |- ( ~P A e. Fin -> A e. Fin )
36	27, 35	impbii 192	1 |- ( A e. Fin <-> ~P A e. Fin )

Syntax hints:   -> wi 4   <-> wb 189   = wceq 1455   e. wcel 1898   E.wrex 2750   _Vcvv 3057   u. cun 3414   C_ wss 3416   (/)c0 3743   ~Pcpw 3963   {csn 3980   class class class wbr 4416   |-> cmpt 4475   suc csuc 5444   omcom 6719   1oc1o 7201   ~~ cen 7592   ~<_ cdom 7593   ~< csdm 7594   Fincfn 7595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-1st 6820  df-2nd 6821  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-1o 7208  df-2o 7209  df-oadd 7212  df-er 7389  df-map 7500  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599

This theorem is referenced by:  mapfi  7896  r1fin  8270  dfac12k  8603  pwsdompw  8660  ackbij1lem5  8680  ackbij1lem9  8684  ackbij1lem10  8685  ackbij1lem14  8689  ackbij1b  8695  isfin1-2  8841  isfin1-3  8842  domtriomlem  8898  dominf  8901  dominfac  9024  gchhar  9130  omina  9142  gchina  9150  hashpw  12641  hashbclem  12648  qshash  13934  ackbijnn  13935  incexclem  13943  incexc  13944  incexc2  13945  hashbccl  15004  lagsubg2  16927  lagsubg  16928  orbsta2  17017  sylow1lem3  17301  sylow1lem5  17303  sylow2alem2  17319  sylow2a  17320  sylow2blem2  17322  sylow2blem3  17323  sylow3lem3  17330  sylow3lem4  17331  sylow3lem6  17333  pgpfac1lem5  17761  discmp  20462  cmpfi  20472  dis1stc  20563  1stckgenlem  20617  ptcmpfi  20877  fiufl  20980  musum  24169  qerclwwlknfi  25606  hasheuni  28955  coinfliplem  29360  ballotth  29419  ballotthOLD  29457  erdszelem2  29964  kelac2lem  35967  pwinfig  36210