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

Theorem snfi 7146
Description: A singleton is finite. (Contributed by NM, 4-Nov-2002.)
Assertion
Ref Expression
snfi  |-  { A }  e.  Fin

Proof of Theorem snfi
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 1onn 6841 . . . 4  |-  1o  e.  om
2 ensn1g 7131 . . . 4  |-  ( A  e.  _V  ->  { A }  ~~  1o )
3 breq2 4176 . . . . 5  |-  ( x  =  1o  ->  ( { A }  ~~  x  <->  { A }  ~~  1o ) )
43rspcev 3012 . . . 4  |-  ( ( 1o  e.  om  /\  { A }  ~~  1o )  ->  E. x  e.  om  { A }  ~~  x
)
51, 2, 4sylancr 645 . . 3  |-  ( A  e.  _V  ->  E. x  e.  om  { A }  ~~  x )
6 snprc 3831 . . . 4  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
7 en0 7129 . . . . 5  |-  ( { A }  ~~  (/)  <->  { A }  =  (/) )
8 peano1 4823 . . . . . 6  |-  (/)  e.  om
9 breq2 4176 . . . . . . 7  |-  ( x  =  (/)  ->  ( { A }  ~~  x  <->  { A }  ~~  (/) ) )
109rspcev 3012 . . . . . 6  |-  ( (
(/)  e.  om  /\  { A }  ~~  (/) )  ->  E. x  e.  om  { A }  ~~  x
)
118, 10mpan 652 . . . . 5  |-  ( { A }  ~~  (/)  ->  E. x  e.  om  { A }  ~~  x )
127, 11sylbir 205 . . . 4  |-  ( { A }  =  (/)  ->  E. x  e.  om  { A }  ~~  x
)
136, 12sylbi 188 . . 3  |-  ( -.  A  e.  _V  ->  E. x  e.  om  { A }  ~~  x )
145, 13pm2.61i 158 . 2  |-  E. x  e.  om  { A }  ~~  x
15 isfi 7090 . 2  |-  ( { A }  e.  Fin  <->  E. x  e.  om  { A }  ~~  x )
1614, 15mpbir 201 1  |-  { A }  e.  Fin
Colors of variables: wff set class
Syntax hints:   -. wn 3    = wceq 1649    e. wcel 1721   E.wrex 2667   _Vcvv 2916   (/)c0 3588   {csn 3774   class class class wbr 4172   omcom 4804   1oc1o 6676    ~~ cen 7065   Fincfn 7068
This theorem is referenced by:  fiprc  7147  prfi  7340  tpfi  7341  fnfi  7343  unifpw  7367  ssfii  7382  cantnfp1lem1  7590  infpwfidom  7865  ackbij1lem4  8059  ackbij1lem9  8064  ackbij1lem10  8065  fin23lem21  8175  isfin1-3  8222  axcclem  8293  zornn0g  8341  hashsng  11602  hashunsng  11620  hashprg  11621  hashsnlei  11635  hashxplem  11651  hashmap  11653  hashfun  11655  hashbclem  11656  hashf1lem1  11659  hashf1lem2  11660  hashf1  11661  fsum2dlem  12509  fsumcom2  12513  ackbijnn  12562  incexclem  12571  isumltss  12583  rexpen  12782  2ebits  12914  phicl2  13112  ramub1lem1  13349  acsfn1  13841  acsfiindd  14558  odcau  15193  sylow2alem2  15207  gsumsn  15498  gsumunsn  15499  gsumpt  15500  dprdfid  15530  ablfac1eu  15586  pgpfaclem2  15595  ablfaclem3  15600  psrlidm  16422  psrridm  16423  mvridlem  16438  mplsubrg  16458  mvrcl  16467  mplmon  16481  mplmonmul  16482  mplcoe3  16484  mplcoe2  16485  psrbagsn  16510  psr1baslem  16538  0cmp  17411  discmp  17415  disllycmp  17514  dis1stc  17515  1stckgenlem  17538  ptpjpre2  17565  ptopn2  17569  xkohaus  17638  xkoptsub  17639  ptcmpfi  17798  cfinufil  17913  ufinffr  17914  fin1aufil  17917  alexsubALTlem3  18033  ptcmplem5  18040  tmdgsum  18078  tsmsxplem1  18135  tsmsxplem2  18136  prdsmet  18353  imasdsf1olem  18356  prdsbl  18474  icccmplem1  18806  icccmplem2  18807  ovolsn  19344  ovolfiniun  19350  volfiniun  19394  i1f0  19532  fta1glem2  20042  fta1blem  20044  fta1lem  20177  vieta1lem2  20181  vieta1  20182  aalioulem2  20203  tayl0  20231  radcnv0  20285  wilthlem2  20805  fsumvma  20950  dchrfi  20992  cusgrafilem3  21443  eupath2lem3  21654  vdegp1ai  21659  vdegp1bi  21660  konigsberg  21662  gsumsn2  24172  esumcst  24408  esumsn  24409  hasheuni  24428  sibf0  24602  derangsn  24809  fprod2dlem  25257  fprodcom2  25261  onsucsuccmpi  26097  locfincmp  26274  comppfsc  26277  prdsbnd  26392  heiborlem3  26412  heiborlem8  26417  ismrer1  26437  reheibor  26438  funsnfsup  26633  elrfi  26638  mzpcompact2lem  26698  dfac11  27028  pwslnmlem0  27061  uvcff  27108  lpirlnr  27189  acsfn1p  27375  stoweidlem44  27660  usgreghash2spotv  28169  pclfinN  30382
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-1o 6683  df-en 7069  df-fin 7072
  Copyright terms: Public domain W3C validator