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

Theorem snfi 7589
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 7280 . . . 4  |-  1o  e.  om
2 ensn1g 7573 . . . 4  |-  ( A  e.  _V  ->  { A }  ~~  1o )
3 breq2 4443 . . . . 5  |-  ( x  =  1o  ->  ( { A }  ~~  x  <->  { A }  ~~  1o ) )
43rspcev 3207 . . . 4  |-  ( ( 1o  e.  om  /\  { A }  ~~  1o )  ->  E. x  e.  om  { A }  ~~  x
)
51, 2, 4sylancr 661 . . 3  |-  ( A  e.  _V  ->  E. x  e.  om  { A }  ~~  x )
6 snprc 4079 . . . 4  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
7 en0 7571 . . . . 5  |-  ( { A }  ~~  (/)  <->  { A }  =  (/) )
8 peano1 6692 . . . . . 6  |-  (/)  e.  om
9 breq2 4443 . . . . . . 7  |-  ( x  =  (/)  ->  ( { A }  ~~  x  <->  { A }  ~~  (/) ) )
109rspcev 3207 . . . . . 6  |-  ( (
(/)  e.  om  /\  { A }  ~~  (/) )  ->  E. x  e.  om  { A }  ~~  x
)
118, 10mpan 668 . . . . 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 7532 . 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 1398    e. wcel 1823   E.wrex 2805   _Vcvv 3106   (/)c0 3783   {csn 4016   class class class wbr 4439   omcom 6673   1oc1o 7115    ~~ cen 7506   Fincfn 7509
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-om 6674  df-1o 7122  df-en 7510  df-fin 7513
This theorem is referenced by:  fiprc  7590  prfi  7787  tpfi  7788  fnfi  7790  unifpw  7815  snopfsupp  7844  sniffsupp  7861  ssfii  7871  cantnfp1lem1  8088  cantnfp1lem1OLD  8114  infpwfidom  8400  ackbij1lem4  8594  ackbij1lem9  8599  ackbij1lem10  8600  fin23lem21  8710  isfin1-3  8757  axcclem  8828  zornn0g  8876  hashsng  12424  hashen1  12425  hashunsng  12446  hashprg  12447  hashsnlei  12465  hashxplem  12478  hashmap  12480  hashfun  12482  hashbclem  12488  hashf1lem1  12491  hashf1lem2  12492  hashf1  12493  fsummsnunz  13654  fsumsplitsnun  13655  fsum2dlem  13670  fsumcom2  13674  ackbijnn  13725  incexclem  13733  isumltss  13745  fprod2dlem  13869  fprodcom2  13873  rexpen  14048  2ebits  14184  phicl2  14385  ramub1lem1  14631  cshwshashnsame  14675  acsfn1  15153  acsfiindd  16009  symg1hash  16622  odcau  16826  sylow2alem2  16840  gsumsnfd  17177  gsumzunsnd  17181  gsumunsnfd  17182  gsumpt  17187  gsumptOLD  17188  dprdfidOLD  17262  ablfac1eu  17322  pgpfaclem2  17331  ablfaclem3  17336  srgbinomlem4  17392  psrlidm  18254  psrlidmOLD  18255  psrridm  18256  psrridmOLD  18257  mvridlemOLD  18273  mplsubrg  18300  mvrcl  18309  mplmon  18323  mplmonmul  18324  mplcoe3OLD  18327  mplcoe2OLD  18331  psrbagsn  18358  psr1baslem  18422  funsnfsupOLD  18454  uvcff  18996  mat1dimelbas  19143  mat1dim0  19145  mat1dimid  19146  mat1dimmul  19148  mat1dimcrng  19149  mat1f1o  19150  mat1ghm  19155  mat1mhm  19156  mat1rhm  19157  mat1rngiso  19158  mat1scmat  19211  mvmumamul1  19226  mdetrsca  19275  mdetunilem9  19292  mdetmul  19295  pmatcoe1fsupp  19372  d1mat2pmat  19410  pmatcollpw3fi1lem1  19457  chpmat1dlem  19506  chpmat1d  19507  0cmp  20064  discmp  20068  bwth  20080  disllycmp  20168  dis1stc  20169  locfincmp  20196  dissnlocfin  20199  comppfsc  20202  1stckgenlem  20223  ptpjpre2  20250  ptopn2  20254  xkohaus  20323  xkoptsub  20324  ptcmpfi  20483  cfinufil  20598  ufinffr  20599  fin1aufil  20602  alexsubALTlem3  20718  ptcmplem5  20725  tmdgsum  20763  tsmsxplem1  20824  tsmsxplem2  20825  prdsmet  21042  imasdsf1olem  21045  prdsbl  21163  icccmplem1  21496  icccmplem2  21497  ovolsn  22075  ovolfiniun  22081  volfiniun  22126  i1f0  22263  fta1glem2  22736  fta1blem  22738  fta1lem  22872  vieta1lem2  22876  vieta1  22877  aalioulem2  22898  tayl0  22926  radcnv0  22980  wilthlem2  23544  fsumvma  23689  dchrfi  23731  cusgrafilem3  24686  eupath2lem3  25184  vdegp1ai  25189  vdegp1bi  25190  konigsberg  25192  usgreghash2spotv  25271  ffsrn  27786  locfinref  28082  esumcst  28295  esumsnf  28296  hasheuni  28317  sibf0  28543  eulerpartlems  28566  eulerpartlemb  28574  ccatmulgnn0dir  28763  ofcccat  28765  plymulx0  28771  derangsn  28881  onsucsuccmpi  30139  finixpnum  30281  prdsbnd  30532  heiborlem3  30552  heiborlem8  30557  ismrer1  30577  reheibor  30578  elrfi  30869  mzpcompact2lem  30926  dfac11  31250  pwslnmlem0  31279  lpirlnr  31310  acsfn1p  31392  fsumsplitsn  31813  fprodsplitsn  31834  dvmptfprodlem  31983  dvnprodlem2  31986  stoweidlem44  32068  fourierdlem51  32182  fourierdlem80  32211  fouriersw  32256  fsummmodsnunz  32739  suppmptcfin  33245  lcosn0  33294  lincext2  33329  snlindsntor  33345  pclfinN  36040
  Copyright terms: Public domain W3C validator