MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pwfi Unicode version

Theorem pwfi 7393
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.
StepHypRef Expression
1 isfi 7122 . . 3  |-  ( A  e.  Fin  <->  E. m  e.  om  A  ~~  m
)
2 pweq 3794 . . . . . . 7  |-  ( m  =  (/)  ->  ~P m  =  ~P (/) )
32eleq1d 2501 . . . . . 6  |-  ( m  =  (/)  ->  ( ~P m  e.  Fin  <->  ~P (/)  e.  Fin ) )
4 pweq 3794 . . . . . . 7  |-  ( m  =  k  ->  ~P m  =  ~P k
)
54eleq1d 2501 . . . . . 6  |-  ( m  =  k  ->  ( ~P m  e.  Fin  <->  ~P k  e.  Fin )
)
6 pweq 3794 . . . . . . . 8  |-  ( m  =  suc  k  ->  ~P m  =  ~P suc  k )
7 df-suc 4579 . . . . . . . . 9  |-  suc  k  =  ( k  u. 
{ k } )
87pweqi 3795 . . . . . . . 8  |-  ~P suc  k  =  ~P (
k  u.  { k } )
96, 8syl6eq 2483 . . . . . . 7  |-  ( m  =  suc  k  ->  ~P m  =  ~P ( k  u.  {
k } ) )
109eleq1d 2501 . . . . . 6  |-  ( m  =  suc  k  -> 
( ~P m  e. 
Fin 
<->  ~P ( k  u. 
{ k } )  e.  Fin ) )
11 pw0 3937 . . . . . . . 8  |-  ~P (/)  =  { (/)
}
12 df1o2 6727 . . . . . . . 8  |-  1o  =  { (/) }
1311, 12eqtr4i 2458 . . . . . . 7  |-  ~P (/)  =  1o
14 1onn 6873 . . . . . . . 8  |-  1o  e.  om
15 ssid 3359 . . . . . . . 8  |-  1o  C_  1o
16 ssnnfi 7319 . . . . . . . 8  |-  ( ( 1o  e.  om  /\  1o  C_  1o )  ->  1o  e.  Fin )
1714, 15, 16mp2an 654 . . . . . . 7  |-  1o  e.  Fin
1813, 17eqeltri 2505 . . . . . 6  |-  ~P (/)  e.  Fin
19 eqid 2435 . . . . . . . 8  |-  ( c  e.  ~P k  |->  ( c  u.  { k } ) )  =  ( c  e.  ~P k  |->  ( c  u. 
{ k } ) )
2019pwfilem 7392 . . . . . . 7  |-  ( ~P k  e.  Fin  ->  ~P ( k  u.  {
k } )  e. 
Fin )
2120a1i 11 . . . . . 6  |-  ( k  e.  om  ->  ( ~P k  e.  Fin  ->  ~P ( k  u. 
{ k } )  e.  Fin ) )
223, 5, 10, 18, 21finds1 4865 . . . . 5  |-  ( m  e.  om  ->  ~P m  e.  Fin )
23 pwen 7271 . . . . 5  |-  ( A 
~~  m  ->  ~P A  ~~  ~P m )
24 enfii 7317 . . . . 5  |-  ( ( ~P m  e.  Fin  /\ 
~P A  ~~  ~P m )  ->  ~P A  e.  Fin )
2522, 23, 24syl2an 464 . . . 4  |-  ( ( m  e.  om  /\  A  ~~  m )  ->  ~P A  e.  Fin )
2625rexlimiva 2817 . . 3  |-  ( E. m  e.  om  A  ~~  m  ->  ~P A  e.  Fin )
271, 26sylbi 188 . 2  |-  ( A  e.  Fin  ->  ~P A  e.  Fin )
28 elex 2956 . . . . 5  |-  ( ~P A  e.  Fin  ->  ~P A  e.  _V )
29 pwexb 4744 . . . . 5  |-  ( A  e.  _V  <->  ~P A  e.  _V )
3028, 29sylibr 204 . . . 4  |-  ( ~P A  e.  Fin  ->  A  e.  _V )
31 canth2g 7252 . . . 4  |-  ( A  e.  _V  ->  A  ~<  ~P A )
32 sdomdom 7126 . . . 4  |-  ( A 
~<  ~P A  ->  A  ~<_  ~P A )
3330, 31, 323syl 19 . . 3  |-  ( ~P A  e.  Fin  ->  A  ~<_  ~P A )
34 domfi 7321 . . 3  |-  ( ( ~P A  e.  Fin  /\  A  ~<_  ~P A )  ->  A  e.  Fin )
3533, 34mpdan 650 . 2  |-  ( ~P A  e.  Fin  ->  A  e.  Fin )
3627, 35impbii 181 1  |-  ( A  e.  Fin  <->  ~P A  e.  Fin )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652    e. wcel 1725   E.wrex 2698   _Vcvv 2948    u. cun 3310    C_ wss 3312   (/)c0 3620   ~Pcpw 3791   {csn 3806   class class class wbr 4204    e. cmpt 4258   suc csuc 4575   omcom 4836   1oc1o 6708    ~~ cen 7097    ~<_ cdom 7098    ~< csdm 7099   Fincfn 7100
This theorem is referenced by:  mapfi  7394  r1fin  7688  dfac12k  8016  pwsdompw  8073  ackbij1lem5  8093  ackbij1lem9  8097  ackbij1lem10  8098  ackbij1lem14  8102  ackbij1b  8108  isfin1-2  8254  isfin1-3  8255  domtriomlem  8311  dominf  8314  dominfac  8437  gchhar  8535  omina  8555  gchina  8563  hashpw  11687  hashbclem  11689  qshash  12594  ackbijnn  12595  incexclem  12604  incexc  12605  incexc2  12606  hashbccl  13359  lagsubg2  14989  lagsubg  14990  orbsta2  15079  sylow1lem3  15222  sylow1lem5  15224  sylow2alem2  15240  sylow2a  15241  sylow2blem2  15243  sylow2blem3  15244  sylow3lem3  15251  sylow3lem4  15252  sylow3lem6  15254  pgpfac1lem5  15625  discmp  17449  cmpfi  17459  dis1stc  17550  1stckgenlem  17573  ptcmpfi  17833  fiufl  17936  musum  20964  hasheuni  24463  coinfliplem  24724  ballotth  24783  erdszelem2  24866  kelac2lem  27077
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4692
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-reu 2704  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-int 4043  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4837  df-xp 4875  df-rel 4876  df-cnv 4877  df-co 4878  df-dm 4879  df-rn 4880  df-res 4881  df-ima 4882  df-iota 5409  df-fun 5447  df-fn 5448  df-f 5449  df-f1 5450  df-fo 5451  df-f1o 5452  df-fv 5453  df-ov 6075  df-oprab 6076  df-mpt2 6077  df-1st 6340  df-2nd 6341  df-recs 6624  df-rdg 6659  df-1o 6715  df-2o 6716  df-oadd 6719  df-er 6896  df-map 7011  df-en 7101  df-dom 7102  df-sdom 7103  df-fin 7104
  Copyright terms: Public domain W3C validator