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

Theorem snfi 7681
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 7371 . . . 4  |-  1o  e.  om
2 ensn1g 7665 . . . 4  |-  ( A  e.  _V  ->  { A }  ~~  1o )
3 breq2 4422 . . . . 5  |-  ( x  =  1o  ->  ( { A }  ~~  x  <->  { A }  ~~  1o ) )
43rspcev 3162 . . . 4  |-  ( ( 1o  e.  om  /\  { A }  ~~  1o )  ->  E. x  e.  om  { A }  ~~  x
)
51, 2, 4sylancr 674 . . 3  |-  ( A  e.  _V  ->  E. x  e.  om  { A }  ~~  x )
6 snprc 4048 . . . 4  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
7 en0 7663 . . . . 5  |-  ( { A }  ~~  (/)  <->  { A }  =  (/) )
8 peano1 6744 . . . . . 6  |-  (/)  e.  om
9 breq2 4422 . . . . . . 7  |-  ( x  =  (/)  ->  ( { A }  ~~  x  <->  { A }  ~~  (/) ) )
109rspcev 3162 . . . . . 6  |-  ( (
(/)  e.  om  /\  { A }  ~~  (/) )  ->  E. x  e.  om  { A }  ~~  x
)
118, 10mpan 681 . . . . 5  |-  ( { A }  ~~  (/)  ->  E. x  e.  om  { A }  ~~  x )
127, 11sylbir 218 . . . 4  |-  ( { A }  =  (/)  ->  E. x  e.  om  { A }  ~~  x
)
136, 12sylbi 200 . . 3  |-  ( -.  A  e.  _V  ->  E. x  e.  om  { A }  ~~  x )
145, 13pm2.61i 169 . 2  |-  E. x  e.  om  { A }  ~~  x
15 isfi 7624 . 2  |-  ( { A }  e.  Fin  <->  E. x  e.  om  { A }  ~~  x )
1614, 15mpbir 214 1  |-  { A }  e.  Fin
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1455    e. wcel 1898   E.wrex 2750   _Vcvv 3057   (/)c0 3743   {csn 3980   class class class wbr 4418   omcom 6724   1oc1o 7206    ~~ cen 7597   Fincfn 7600
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 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615
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-rab 2758  df-v 3059  df-sbc 3280  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-br 4419  df-opab 4478  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-om 6725  df-1o 7213  df-en 7601  df-fin 7604
This theorem is referenced by:  fiprc  7682  prfi  7877  tpfi  7878  fnfi  7880  unifpw  7908  snopfsupp  7937  sniffsupp  7954  ssfii  7964  cantnfp1lem1  8214  infpwfidom  8490  ackbij1lem4  8684  ackbij1lem9  8689  ackbij1lem10  8690  fin23lem21  8800  isfin1-3  8847  axcclem  8918  zornn0g  8966  hashsng  12587  hashen1  12588  hashunsng  12609  hashprg  12610  hashsnlei  12631  hashxplem  12644  hashmap  12646  hashfun  12648  hashbclem  12654  hashf1lem1  12657  hashf1lem2  12658  hashf1  12659  fsummsnunz  13870  fsumsplitsnun  13871  fsum2dlem  13886  fsumcom2  13890  ackbijnn  13941  incexclem  13949  isumltss  13961  fprod2dlem  14089  fprodcom2  14093  fprodsplitsn  14098  rexpen  14335  2ebits  14476  lcmfunsnlem2lem1  14666  lcmfunsnlem2lem2  14667  lcmfunsnlem2  14668  lcmfass  14674  phicl2  14771  ramub1lem1  15039  cshwshashnsame  15129  acsfn1  15622  acsfiindd  16478  symg1hash  17091  odcau  17311  sylow2alem2  17325  gsumsnfd  17639  gsumzunsnd  17643  gsumunsnfd  17644  gsumpt  17649  ablfac1eu  17761  pgpfaclem2  17770  ablfaclem3  17775  srgbinomlem4  17831  psrlidm  18682  psrridm  18683  mplsubrg  18719  mvrcl  18728  mplmon  18742  mplmonmul  18743  psrbagsn  18773  psr1baslem  18833  uvcff  19404  mat1dimelbas  19551  mat1dim0  19553  mat1dimid  19554  mat1dimmul  19556  mat1dimcrng  19557  mat1f1o  19558  mat1ghm  19563  mat1mhm  19564  mat1rhm  19565  mat1rngiso  19566  mat1scmat  19619  mvmumamul1  19634  mdetrsca  19683  mdetunilem9  19700  mdetmul  19703  pmatcoe1fsupp  19780  d1mat2pmat  19818  pmatcollpw3fi1lem1  19865  chpmat1dlem  19914  chpmat1d  19915  0cmp  20464  discmp  20468  bwth  20480  disllycmp  20568  dis1stc  20569  locfincmp  20596  dissnlocfin  20599  comppfsc  20602  1stckgenlem  20623  ptpjpre2  20650  ptopn2  20654  xkohaus  20723  xkoptsub  20724  ptcmpfi  20883  cfinufil  20998  ufinffr  20999  fin1aufil  21002  alexsubALTlem3  21119  ptcmplem5  21126  tmdgsum  21165  tsmsxplem1  21222  tsmsxplem2  21223  prdsmet  21440  imasdsf1olem  21443  prdsbl  21561  icccmplem1  21895  icccmplem2  21896  ovolsn  22503  ovolfiniun  22509  volfiniun  22556  i1f0  22701  fta1glem2  23173  fta1blem  23175  fta1lem  23316  vieta1lem2  23320  vieta1  23321  aalioulem2  23345  tayl0  23373  radcnv0  23427  wilthlem2  24050  fsumvma  24197  dchrfi  24239  cusgrafilem3  25265  eupath2lem3  25763  vdegp1ai  25768  vdegp1bi  25769  konigsberg  25771  usgreghash2spotv  25850  ffsrn  28366  locfinref  28719  esumcst  28935  esumsnf  28936  hasheuni  28957  rossros  29053  sibf0  29217  eulerpartlems  29243  eulerpartlemb  29251  ccatmulgnn0dir  29478  ofcccat  29480  plymulx0  29486  derangsn  29943  onsucsuccmpi  31153  topdifinffinlem  31796  finixpnum  31976  poimirlem25  32011  poimirlem26  32012  poimirlem27  32013  poimirlem31  32017  poimirlem32  32018  prdsbnd  32171  heiborlem3  32191  heiborlem8  32196  ismrer1  32216  reheibor  32217  pclfinN  33511  elrfi  35582  mzpcompact2lem  35639  dfac11  35966  pwslnmlem0  35995  lpirlnr  36022  acsfn1p  36111  mpct  37536  fsumsplitsn  37734  dvmptfprodlem  37905  dvnprodlem2  37908  stoweidlem44  38006  fourierdlem51  38122  fourierdlem80  38151  fouriersw  38196  salexct  38294  salexct3  38302  salgencntex  38303  salgensscntex  38304  sge0sn  38324  sge0tsms  38325  sge0cl  38326  sge0sup  38336  sge0iunmptlemfi  38358  sge0splitsn  38386  hoiprodp1  38517  sge0hsphoire  38518  hoidmv1le  38523  hoidmvlelem1  38524  hoidmvlelem2  38525  hoidmvlelem5  38528  hspmbllem2  38556  ovnovollem3  38587  vonvolmbl  38590  vonvol  38591  vonvol2  38593  fsummmodsnunz  39236  cusgrfilem3  39664  suppmptcfin  40533  lcosn0  40582  lincext2  40617  snlindsntor  40633
  Copyright terms: Public domain W3C validator