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

Theorem snfi 7389
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 7077 . . . 4  |-  1o  e.  om
2 ensn1g 7373 . . . 4  |-  ( A  e.  _V  ->  { A }  ~~  1o )
3 breq2 4295 . . . . 5  |-  ( x  =  1o  ->  ( { A }  ~~  x  <->  { A }  ~~  1o ) )
43rspcev 3072 . . . 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 3938 . . . 4  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
7 en0 7371 . . . . 5  |-  ( { A }  ~~  (/)  <->  { A }  =  (/) )
8 peano1 6494 . . . . . 6  |-  (/)  e.  om
9 breq2 4295 . . . . . . 7  |-  ( x  =  (/)  ->  ( { A }  ~~  x  <->  { A }  ~~  (/) ) )
109rspcev 3072 . . . . . 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 7332 . 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 1369    e. wcel 1756   E.wrex 2715   _Vcvv 2971   (/)c0 3636   {csn 3876   class class class wbr 4291   omcom 6475   1oc1o 6912    ~~ cen 7306   Fincfn 7309
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4412  ax-nul 4420  ax-pow 4469  ax-pr 4530  ax-un 6371
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2719  df-rex 2720  df-rab 2723  df-v 2973  df-sbc 3186  df-dif 3330  df-un 3332  df-in 3334  df-ss 3341  df-pss 3343  df-nul 3637  df-if 3791  df-pw 3861  df-sn 3877  df-pr 3879  df-tp 3881  df-op 3883  df-uni 4091  df-br 4292  df-opab 4350  df-tr 4385  df-eprel 4631  df-id 4635  df-po 4640  df-so 4641  df-fr 4678  df-we 4680  df-ord 4721  df-on 4722  df-lim 4723  df-suc 4724  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-om 6476  df-1o 6919  df-en 7310  df-fin 7313
This theorem is referenced by:  fiprc  7390  prfi  7585  tpfi  7586  fnfi  7588  unifpw  7613  snopfsupp  7642  sniffsupp  7658  ssfii  7668  cantnfp1lem1  7885  cantnfp1lem1OLD  7911  infpwfidom  8197  ackbij1lem4  8391  ackbij1lem9  8396  ackbij1lem10  8397  fin23lem21  8507  isfin1-3  8554  axcclem  8625  zornn0g  8673  hashsng  12135  hashunsng  12153  hashprg  12154  hashsnlei  12169  hashxplem  12194  hashmap  12196  hashfun  12198  hashbclem  12204  hashf1lem1  12207  hashf1lem2  12208  hashf1  12209  fsum2dlem  13236  fsumcom2  13240  ackbijnn  13290  incexclem  13298  isumltss  13310  rexpen  13509  2ebits  13642  phicl2  13842  ramub1lem1  14086  cshwshashnsame  14129  acsfn1  14598  acsfiindd  15346  symg1hash  15899  odcau  16102  sylow2alem2  16116  gsumsn  16448  gsumsnd  16449  gsumzunsnd  16450  gsumunsnd  16451  gsumpt  16453  gsumptOLD  16454  dprdfidOLD  16513  ablfac1eu  16573  pgpfaclem2  16582  ablfaclem3  16587  psrlidm  17473  psrlidmOLD  17474  psrridm  17475  psrridmOLD  17476  mvridlemOLD  17491  mplsubrg  17518  mvrcl  17527  mplmon  17541  mplmonmul  17542  mplcoe3OLD  17545  mplcoe2OLD  17549  psrbagsn  17576  psr1baslem  17640  funsnfsupOLD  17669  uvcff  18215  mvmumamul1  18364  mdetrsca  18409  mdetunilem9  18425  mdetmul  18428  0cmp  18996  discmp  19000  bwth  19012  bwthOLD  19013  disllycmp  19101  dis1stc  19102  1stckgenlem  19125  ptpjpre2  19152  ptopn2  19156  xkohaus  19225  xkoptsub  19226  ptcmpfi  19385  cfinufil  19500  ufinffr  19501  fin1aufil  19504  alexsubALTlem3  19620  ptcmplem5  19627  tmdgsum  19665  tsmsxplem1  19726  tsmsxplem2  19727  prdsmet  19944  imasdsf1olem  19947  prdsbl  20065  icccmplem1  20398  icccmplem2  20399  ovolsn  20977  ovolfiniun  20983  volfiniun  21027  i1f0  21164  fta1glem2  21637  fta1blem  21639  fta1lem  21772  vieta1lem2  21776  vieta1  21777  aalioulem2  21798  tayl0  21826  radcnv0  21880  wilthlem2  22406  fsumvma  22551  dchrfi  22593  cusgrafilem3  23388  eupath2lem3  23599  vdegp1ai  23604  vdegp1bi  23605  konigsberg  23607  ffsrn  26028  gsumsn2  26242  gsumsnf  26243  gsumunsnf  26244  esumcst  26513  esumsn  26514  hasheuni  26533  sibf0  26719  eulerpartlems  26742  eulerpartlemb  26750  ccatmulgnn0dir  26939  ofcccat  26941  plymulx0  26947  derangsn  27057  fprod2dlem  27490  fprodcom2  27494  onsucsuccmpi  28288  finixpnum  28412  locfincmp  28574  comppfsc  28577  prdsbnd  28690  heiborlem3  28710  heiborlem8  28715  ismrer1  28735  reheibor  28736  elrfi  29028  mzpcompact2lem  29086  dfac11  29413  pwslnmlem0  29442  lpirlnr  29471  acsfn1p  29554  stoweidlem44  29837  fsummsnunz  30239  fsumsplitsnun  30240  fsummmodsnunre  30241  usgreghash2spotv  30657  hashen1  30735  gsumsndf  30761  suppmptcfin  30791  mat1dimelbas  30865  mat1dim0  30867  mat1dimid  30868  mat1dimmul  30870  mat1dimcrng  30871  pmatcoe1fsupp  30890  lcosn0  30952  lincext2  30987  snlindsntor  31003  pclfinN  33542
  Copyright terms: Public domain W3C validator