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

Theorem snfi 7599
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 7290 . . . 4  |-  1o  e.  om
2 ensn1g 7583 . . . 4  |-  ( A  e.  _V  ->  { A }  ~~  1o )
3 breq2 4365 . . . . 5  |-  ( x  =  1o  ->  ( { A }  ~~  x  <->  { A }  ~~  1o ) )
43rspcev 3120 . . . 4  |-  ( ( 1o  e.  om  /\  { A }  ~~  1o )  ->  E. x  e.  om  { A }  ~~  x
)
51, 2, 4sylancr 667 . . 3  |-  ( A  e.  _V  ->  E. x  e.  om  { A }  ~~  x )
6 snprc 4001 . . . 4  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
7 en0 7581 . . . . 5  |-  ( { A }  ~~  (/)  <->  { A }  =  (/) )
8 peano1 6665 . . . . . 6  |-  (/)  e.  om
9 breq2 4365 . . . . . . 7  |-  ( x  =  (/)  ->  ( { A }  ~~  x  <->  { A }  ~~  (/) ) )
109rspcev 3120 . . . . . 6  |-  ( (
(/)  e.  om  /\  { A }  ~~  (/) )  ->  E. x  e.  om  { A }  ~~  x
)
118, 10mpan 674 . . . . 5  |-  ( { A }  ~~  (/)  ->  E. x  e.  om  { A }  ~~  x )
127, 11sylbir 216 . . . 4  |-  ( { A }  =  (/)  ->  E. x  e.  om  { A }  ~~  x
)
136, 12sylbi 198 . . 3  |-  ( -.  A  e.  _V  ->  E. x  e.  om  { A }  ~~  x )
145, 13pm2.61i 167 . 2  |-  E. x  e.  om  { A }  ~~  x
15 isfi 7542 . 2  |-  ( { A }  e.  Fin  <->  E. x  e.  om  { A }  ~~  x )
1614, 15mpbir 212 1  |-  { A }  e.  Fin
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1437    e. wcel 1872   E.wrex 2710   _Vcvv 3017   (/)c0 3699   {csn 3936   class class class wbr 4361   omcom 6645   1oc1o 7125    ~~ cen 7516   Fincfn 7519
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-rab 2718  df-v 3019  df-sbc 3238  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-br 4362  df-opab 4421  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-om 6646  df-1o 7132  df-en 7520  df-fin 7523
This theorem is referenced by:  fiprc  7600  prfi  7794  tpfi  7795  fnfi  7797  unifpw  7825  snopfsupp  7854  sniffsupp  7871  ssfii  7881  cantnfp1lem1  8130  infpwfidom  8405  ackbij1lem4  8599  ackbij1lem9  8604  ackbij1lem10  8605  fin23lem21  8715  isfin1-3  8762  axcclem  8833  zornn0g  8881  hashsng  12494  hashen1  12495  hashunsng  12516  hashprg  12517  hashsnlei  12535  hashxplem  12548  hashmap  12550  hashfun  12552  hashbclem  12558  hashf1lem1  12561  hashf1lem2  12562  hashf1  12563  fsummsnunz  13753  fsumsplitsnun  13754  fsum2dlem  13769  fsumcom2  13773  ackbijnn  13824  incexclem  13832  isumltss  13844  fprod2dlem  13972  fprodcom2  13976  fprodsplitsn  13981  rexpen  14218  2ebits  14359  lcmfunsnlem2lem1  14549  lcmfunsnlem2lem2  14550  lcmfunsnlem2  14551  lcmfass  14557  phicl2  14654  ramub1lem1  14922  cshwshashnsame  15012  acsfn1  15505  acsfiindd  16361  symg1hash  16974  odcau  17194  sylow2alem2  17208  gsumsnfd  17522  gsumzunsnd  17526  gsumunsnfd  17527  gsumpt  17532  ablfac1eu  17644  pgpfaclem2  17653  ablfaclem3  17658  srgbinomlem4  17714  psrlidm  18565  psrridm  18566  mplsubrg  18602  mvrcl  18611  mplmon  18625  mplmonmul  18626  psrbagsn  18656  psr1baslem  18716  uvcff  19286  mat1dimelbas  19433  mat1dim0  19435  mat1dimid  19436  mat1dimmul  19438  mat1dimcrng  19439  mat1f1o  19440  mat1ghm  19445  mat1mhm  19446  mat1rhm  19447  mat1rngiso  19448  mat1scmat  19501  mvmumamul1  19516  mdetrsca  19565  mdetunilem9  19582  mdetmul  19585  pmatcoe1fsupp  19662  d1mat2pmat  19700  pmatcollpw3fi1lem1  19747  chpmat1dlem  19796  chpmat1d  19797  0cmp  20346  discmp  20350  bwth  20362  disllycmp  20450  dis1stc  20451  locfincmp  20478  dissnlocfin  20481  comppfsc  20484  1stckgenlem  20505  ptpjpre2  20532  ptopn2  20536  xkohaus  20605  xkoptsub  20606  ptcmpfi  20765  cfinufil  20880  ufinffr  20881  fin1aufil  20884  alexsubALTlem3  21001  ptcmplem5  21008  tmdgsum  21047  tsmsxplem1  21104  tsmsxplem2  21105  prdsmet  21322  imasdsf1olem  21325  prdsbl  21443  icccmplem1  21777  icccmplem2  21778  ovolsn  22385  ovolfiniun  22391  volfiniun  22437  i1f0  22582  fta1glem2  23054  fta1blem  23056  fta1lem  23197  vieta1lem2  23201  vieta1  23202  aalioulem2  23226  tayl0  23254  radcnv0  23308  wilthlem2  23931  fsumvma  24078  dchrfi  24120  cusgrafilem3  25146  eupath2lem3  25644  vdegp1ai  25649  vdegp1bi  25650  konigsberg  25652  usgreghash2spotv  25731  ffsrn  28259  locfinref  28615  esumcst  28831  esumsnf  28832  hasheuni  28853  rossros  28949  sibf0  29114  eulerpartlems  29140  eulerpartlemb  29148  ccatmulgnn0dir  29375  ofcccat  29377  plymulx0  29383  derangsn  29840  onsucsuccmpi  31047  topdifinffinlem  31657  finixpnum  31837  poimirlem25  31872  poimirlem26  31873  poimirlem27  31874  poimirlem31  31878  poimirlem32  31879  prdsbnd  32032  heiborlem3  32052  heiborlem8  32057  ismrer1  32077  reheibor  32078  pclfinN  33377  elrfi  35448  mzpcompact2lem  35505  dfac11  35833  pwslnmlem0  35862  lpirlnr  35889  acsfn1p  35978  fsumsplitsn  37533  dvmptfprodlem  37702  dvnprodlem2  37705  stoweidlem44  37788  fourierdlem51  37904  fourierdlem80  37933  fouriersw  37978  sge0sn  38072  sge0tsms  38073  sge0cl  38074  sge0sup  38084  sge0iunmptlemfi  38106  sge0splitsn  38134  hoiprodp1  38257  sge0hsphoire  38258  hoidmv1le  38263  hoidmvlelem1  38264  hoidmvlelem2  38265  hoidmvlelem5  38268  fsummmodsnunz  38868  cusgrfilem3  39246  suppmptcfin  39757  lcosn0  39806  lincext2  39841  snlindsntor  39857
  Copyright terms: Public domain W3C validator