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

Theorem snfi 7378
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 7066 . . . 4  |-  1o  e.  om
2 ensn1g 7362 . . . 4  |-  ( A  e.  _V  ->  { A }  ~~  1o )
3 breq2 4284 . . . . 5  |-  ( x  =  1o  ->  ( { A }  ~~  x  <->  { A }  ~~  1o ) )
43rspcev 3062 . . . 4  |-  ( ( 1o  e.  om  /\  { A }  ~~  1o )  ->  E. x  e.  om  { A }  ~~  x
)
51, 2, 4sylancr 656 . . 3  |-  ( A  e.  _V  ->  E. x  e.  om  { A }  ~~  x )
6 snprc 3927 . . . 4  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
7 en0 7360 . . . . 5  |-  ( { A }  ~~  (/)  <->  { A }  =  (/) )
8 peano1 6484 . . . . . 6  |-  (/)  e.  om
9 breq2 4284 . . . . . . 7  |-  ( x  =  (/)  ->  ( { A }  ~~  x  <->  { A }  ~~  (/) ) )
109rspcev 3062 . . . . . 6  |-  ( (
(/)  e.  om  /\  { A }  ~~  (/) )  ->  E. x  e.  om  { A }  ~~  x
)
118, 10mpan 663 . . . . 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 7321 . 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 1362    e. wcel 1755   E.wrex 2706   _Vcvv 2962   (/)c0 3625   {csn 3865   class class class wbr 4280   omcom 6465   1oc1o 6901    ~~ cen 7295   Fincfn 7298
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-om 6466  df-1o 6908  df-en 7299  df-fin 7302
This theorem is referenced by:  fiprc  7379  prfi  7574  tpfi  7575  fnfi  7577  unifpw  7602  snopfsupp  7631  sniffsupp  7647  ssfii  7657  cantnfp1lem1  7874  cantnfp1lem1OLD  7900  infpwfidom  8186  ackbij1lem4  8380  ackbij1lem9  8385  ackbij1lem10  8386  fin23lem21  8496  isfin1-3  8543  axcclem  8614  zornn0g  8662  hashsng  12119  hashunsng  12137  hashprg  12138  hashsnlei  12153  hashxplem  12178  hashmap  12180  hashfun  12182  hashbclem  12188  hashf1lem1  12191  hashf1lem2  12192  hashf1  12193  fsum2dlem  13220  fsumcom2  13224  ackbijnn  13273  incexclem  13281  isumltss  13293  rexpen  13492  2ebits  13625  phicl2  13825  ramub1lem1  14069  cshwshashnsame  14112  acsfn1  14581  acsfiindd  15329  symg1hash  15879  odcau  16082  sylow2alem2  16096  gsumsn  16424  gsumsnd  16425  gsumunsnd  16426  gsumpt  16428  gsumptOLD  16429  dprdfidOLD  16487  ablfac1eu  16547  pgpfaclem2  16556  ablfaclem3  16561  psrlidm  17407  psrlidmOLD  17408  psrridm  17409  psrridmOLD  17410  mvridlemOLD  17425  mplsubrg  17452  mvrcl  17461  mplmon  17475  mplmonmul  17476  mplcoe3OLD  17479  mplcoe2OLD  17481  psrbagsn  17508  psr1baslem  17539  funsnfsupOLD  17568  uvcff  18057  mvmumamul1  18206  mdetrsca  18251  mdetunilem9  18267  mdetmul  18270  0cmp  18838  discmp  18842  bwth  18854  bwthOLD  18855  disllycmp  18943  dis1stc  18944  1stckgenlem  18967  ptpjpre2  18994  ptopn2  18998  xkohaus  19067  xkoptsub  19068  ptcmpfi  19227  cfinufil  19342  ufinffr  19343  fin1aufil  19346  alexsubALTlem3  19462  ptcmplem5  19469  tmdgsum  19507  tsmsxplem1  19568  tsmsxplem2  19569  prdsmet  19786  imasdsf1olem  19789  prdsbl  19907  icccmplem1  20240  icccmplem2  20241  ovolsn  20819  ovolfiniun  20825  volfiniun  20869  i1f0  21006  fta1glem2  21522  fta1blem  21524  fta1lem  21657  vieta1lem2  21661  vieta1  21662  aalioulem2  21683  tayl0  21711  radcnv0  21765  wilthlem2  22291  fsumvma  22436  dchrfi  22478  cusgrafilem3  23211  eupath2lem3  23422  vdegp1ai  23427  vdegp1bi  23428  konigsberg  23430  ffsrn  25853  gsumsn2  26091  gsumsnf  26095  gsumunsnf  26096  esumcst  26367  esumsn  26368  hasheuni  26387  sibf0  26567  eulerpartlems  26590  eulerpartlemb  26598  ccatmulgnn0dir  26787  ofcccat  26789  plymulx0  26795  derangsn  26905  fprod2dlem  27337  fprodcom2  27341  onsucsuccmpi  28136  finixpnum  28255  locfincmp  28417  comppfsc  28420  prdsbnd  28533  heiborlem3  28553  heiborlem8  28558  ismrer1  28578  reheibor  28579  elrfi  28872  mzpcompact2lem  28930  dfac11  29257  pwslnmlem0  29286  lpirlnr  29315  acsfn1p  29398  stoweidlem44  29682  fsummsnunz  30084  fsumsplitsnun  30085  fsummmodsnunre  30086  usgreghash2spotv  30502  hashen1  30578  suppmptcfin  30620  lcosn0  30660  lincext2  30695  snlindsntor  30711  pclfinN  33114
  Copyright terms: Public domain W3C validator