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

Theorem snfi 7598
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 7582 . . . 4  |-  ( A  e.  _V  ->  { A }  ~~  1o )
3 breq2 4441 . . . . 5  |-  ( x  =  1o  ->  ( { A }  ~~  x  <->  { A }  ~~  1o ) )
43rspcev 3196 . . . 4  |-  ( ( 1o  e.  om  /\  { A }  ~~  1o )  ->  E. x  e.  om  { A }  ~~  x
)
51, 2, 4sylancr 663 . . 3  |-  ( A  e.  _V  ->  E. x  e.  om  { A }  ~~  x )
6 snprc 4078 . . . 4  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
7 en0 7580 . . . . 5  |-  ( { A }  ~~  (/)  <->  { A }  =  (/) )
8 peano1 6704 . . . . . 6  |-  (/)  e.  om
9 breq2 4441 . . . . . . 7  |-  ( x  =  (/)  ->  ( { A }  ~~  x  <->  { A }  ~~  (/) ) )
109rspcev 3196 . . . . . 6  |-  ( (
(/)  e.  om  /\  { A }  ~~  (/) )  ->  E. x  e.  om  { A }  ~~  x
)
118, 10mpan 670 . . . . 5  |-  ( { A }  ~~  (/)  ->  E. x  e.  om  { A }  ~~  x )
127, 11sylbir 213 . . . 4  |-  ( { A }  =  (/)  ->  E. x  e.  om  { A }  ~~  x
)
136, 12sylbi 195 . . 3  |-  ( -.  A  e.  _V  ->  E. x  e.  om  { A }  ~~  x )
145, 13pm2.61i 164 . 2  |-  E. x  e.  om  { A }  ~~  x
15 isfi 7541 . 2  |-  ( { A }  e.  Fin  <->  E. x  e.  om  { A }  ~~  x )
1614, 15mpbir 209 1  |-  { A }  e.  Fin
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1383    e. wcel 1804   E.wrex 2794   _Vcvv 3095   (/)c0 3770   {csn 4014   class class class wbr 4437   omcom 6685   1oc1o 7125    ~~ cen 7515   Fincfn 7518
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-om 6686  df-1o 7132  df-en 7519  df-fin 7522
This theorem is referenced by:  fiprc  7599  prfi  7797  tpfi  7798  fnfi  7800  unifpw  7825  snopfsupp  7854  sniffsupp  7871  ssfii  7881  cantnfp1lem1  8100  cantnfp1lem1OLD  8126  infpwfidom  8412  ackbij1lem4  8606  ackbij1lem9  8611  ackbij1lem10  8612  fin23lem21  8722  isfin1-3  8769  axcclem  8840  zornn0g  8888  hashsng  12420  hashen1  12421  hashunsng  12441  hashprg  12442  hashsnlei  12460  hashxplem  12473  hashmap  12475  hashfun  12477  hashbclem  12483  hashf1lem1  12486  hashf1lem2  12487  hashf1  12488  fsummsnunz  13551  fsumsplitsnun  13552  fsum2dlem  13567  fsumcom2  13571  ackbijnn  13622  incexclem  13630  isumltss  13642  fprod2dlem  13766  fprodcom2  13770  rexpen  13943  2ebits  14079  phicl2  14280  ramub1lem1  14526  cshwshashnsame  14570  acsfn1  15040  acsfiindd  15786  symg1hash  16399  odcau  16603  sylow2alem2  16617  gsumsnfd  16957  gsumzunsnd  16961  gsumunsnfd  16962  gsumpt  16967  gsumptOLD  16968  dprdfidOLD  17043  ablfac1eu  17103  pgpfaclem2  17112  ablfaclem3  17117  srgbinomlem4  17173  psrlidm  18035  psrlidmOLD  18036  psrridm  18037  psrridmOLD  18038  mvridlemOLD  18054  mplsubrg  18081  mvrcl  18090  mplmon  18104  mplmonmul  18105  mplcoe3OLD  18108  mplcoe2OLD  18112  psrbagsn  18139  psr1baslem  18203  funsnfsupOLD  18235  uvcff  18800  mat1dimelbas  18951  mat1dim0  18953  mat1dimid  18954  mat1dimmul  18956  mat1dimcrng  18957  mat1f1o  18958  mat1ghm  18963  mat1mhm  18964  mat1rhm  18965  mat1rngiso  18966  mat1scmat  19019  mvmumamul1  19034  mdetrsca  19083  mdetunilem9  19100  mdetmul  19103  pmatcoe1fsupp  19180  d1mat2pmat  19218  pmatcollpw3fi1lem1  19265  chpmat1dlem  19314  chpmat1d  19315  0cmp  19872  discmp  19876  bwth  19888  bwthOLD  19889  disllycmp  19977  dis1stc  19978  locfincmp  20005  dissnlocfin  20008  comppfsc  20011  1stckgenlem  20032  ptpjpre2  20059  ptopn2  20063  xkohaus  20132  xkoptsub  20133  ptcmpfi  20292  cfinufil  20407  ufinffr  20408  fin1aufil  20411  alexsubALTlem3  20527  ptcmplem5  20534  tmdgsum  20572  tsmsxplem1  20633  tsmsxplem2  20634  prdsmet  20851  imasdsf1olem  20854  prdsbl  20972  icccmplem1  21305  icccmplem2  21306  ovolsn  21884  ovolfiniun  21890  volfiniun  21935  i1f0  22072  fta1glem2  22545  fta1blem  22547  fta1lem  22681  vieta1lem2  22685  vieta1  22686  aalioulem2  22707  tayl0  22735  radcnv0  22789  wilthlem2  23321  fsumvma  23466  dchrfi  23508  cusgrafilem3  24459  eupath2lem3  24957  vdegp1ai  24962  vdegp1bi  24963  konigsberg  24965  usgreghash2spotv  25044  ffsrn  27530  locfinref  27822  esumcst  28049  esumsn  28050  hasheuni  28069  sibf0  28254  eulerpartlems  28277  eulerpartlemb  28285  ccatmulgnn0dir  28474  ofcccat  28476  plymulx0  28482  derangsn  28592  onsucsuccmpi  29884  finixpnum  30014  prdsbnd  30265  heiborlem3  30285  heiborlem8  30290  ismrer1  30310  reheibor  30311  elrfi  30602  mzpcompact2lem  30660  dfac11  30984  pwslnmlem0  31013  lpirlnr  31042  acsfn1p  31124  fsumsplitsn  31525  fprodsplitsn  31546  dvmptfprodlem  31695  dvnprodlem2  31698  stoweidlem44  31780  fourierdlem51  31894  fourierdlem80  31923  fouriersw  31968  fsummmodsnunz  32302  suppmptcfin  32842  lcosn0  32891  lincext2  32926  snlindsntor  32942  pclfinN  35499
  Copyright terms: Public domain W3C validator