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

Theorem snfi 7923
Description: A singleton is finite. (Contributed by NM, 4-Nov-2002.)
Assertion
Ref Expression
snfi {𝐴} ∈ Fin

Proof of Theorem snfi
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 1onn 7606 . . . 4 1𝑜 ∈ ω
2 ensn1g 7907 . . . 4 (𝐴 ∈ V → {𝐴} ≈ 1𝑜)
3 breq2 4587 . . . . 5 (𝑥 = 1𝑜 → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1𝑜))
43rspcev 3282 . . . 4 ((1𝑜 ∈ ω ∧ {𝐴} ≈ 1𝑜) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
51, 2, 4sylancr 694 . . 3 (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6 snprc 4197 . . . 4 𝐴 ∈ V ↔ {𝐴} = ∅)
7 en0 7905 . . . . 5 ({𝐴} ≈ ∅ ↔ {𝐴} = ∅)
8 peano1 6977 . . . . . 6 ∅ ∈ ω
9 breq2 4587 . . . . . . 7 (𝑥 = ∅ → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ ∅))
109rspcev 3282 . . . . . 6 ((∅ ∈ ω ∧ {𝐴} ≈ ∅) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
118, 10mpan 702 . . . . 5 ({𝐴} ≈ ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
127, 11sylbir 224 . . . 4 ({𝐴} = ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
136, 12sylbi 206 . . 3 𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
145, 13pm2.61i 175 . 2 𝑥 ∈ ω {𝐴} ≈ 𝑥
15 isfi 7865 . 2 ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
1614, 15mpbir 220 1 {𝐴} ∈ Fin
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1475  wcel 1977  wrex 2897  Vcvv 3173  c0 3874  {csn 4125   class class class wbr 4583  ωcom 6957  1𝑜c1o 7440  cen 7838  Fincfn 7841
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-om 6958  df-1o 7447  df-en 7842  df-fin 7845
This theorem is referenced by:  fiprc  7924  prfi  8120  tpfi  8121  fnfi  8123  unifpw  8152  snopfsupp  8181  sniffsupp  8198  ssfii  8208  cantnfp1lem1  8458  infpwfidom  8734  ackbij1lem4  8928  ackbij1lem9  8933  ackbij1lem10  8934  fin23lem21  9044  isfin1-3  9091  axcclem  9162  zornn0g  9210  hashsng  13020  hashen1  13021  hashunsng  13042  hashprg  13043  hashprgOLD  13044  hashsnlei  13067  hashxplem  13080  hashmap  13082  hashfun  13084  hashbclem  13093  hashf1lem1  13096  hashf1lem2  13097  hashf1  13098  fsummsnunz  14327  fsumsplitsnun  14328  fsum2dlem  14343  fsumcom2  14347  fsumcom2OLD  14348  ackbijnn  14399  incexclem  14407  isumltss  14419  fprod2dlem  14549  fprodcom2  14553  fprodcom2OLD  14554  fprodsplitsn  14559  rexpen  14796  2ebits  15007  lcmfunsnlem2lem1  15189  lcmfunsnlem2lem2  15190  lcmfunsnlem2  15191  lcmfass  15197  phicl2  15311  ramub1lem1  15568  cshwshashnsame  15648  acsfn1  16145  acsfiindd  17000  symg1hash  17638  odcau  17842  sylow2alem2  17856  gsumsnfd  18174  gsumzunsnd  18178  gsumunsnfd  18179  gsumpt  18184  ablfac1eu  18295  pgpfaclem2  18304  ablfaclem3  18309  srgbinomlem4  18366  psrlidm  19224  psrridm  19225  mplsubrg  19261  mvrcl  19270  mplmon  19284  mplmonmul  19285  psrbagsn  19316  psr1baslem  19376  uvcff  19949  mat1dimelbas  20096  mat1dim0  20098  mat1dimid  20099  mat1dimmul  20101  mat1dimcrng  20102  mat1f1o  20103  mat1ghm  20108  mat1mhm  20109  mat1rhm  20110  mat1rngiso  20111  mat1scmat  20164  mvmumamul1  20179  mdetrsca  20228  mdetunilem9  20245  mdetmul  20248  pmatcoe1fsupp  20325  d1mat2pmat  20363  pmatcollpw3fi1lem1  20410  chpmat1dlem  20459  chpmat1d  20460  0cmp  21007  discmp  21011  bwth  21023  disllycmp  21111  dis1stc  21112  locfincmp  21139  dissnlocfin  21142  comppfsc  21145  1stckgenlem  21166  ptpjpre2  21193  ptopn2  21197  xkohaus  21266  xkoptsub  21267  ptcmpfi  21426  cfinufil  21542  ufinffr  21543  fin1aufil  21546  alexsubALTlem3  21663  ptcmplem5  21670  tmdgsum  21709  tsmsxplem1  21766  tsmsxplem2  21767  prdsmet  21985  imasdsf1olem  21988  prdsbl  22106  icccmplem1  22433  icccmplem2  22434  ovolsn  23070  ovolfiniun  23076  volfiniun  23122  i1f0  23260  fta1glem2  23730  fta1blem  23732  fta1lem  23866  vieta1lem2  23870  vieta1  23871  aalioulem2  23892  tayl0  23920  radcnv0  23974  wilthlem2  24595  fsumvma  24738  dchrfi  24780  cusgrafilem3  26009  eupath2lem3  26506  vdegp1ai  26511  vdegp1bi  26512  konigsberg  26514  usgreghash2spotv  26593  ex-hash  26702  ffsrn  28892  locfinref  29236  esumcst  29452  esumsnf  29453  hasheuni  29474  rossros  29570  sibf0  29723  eulerpartlems  29749  eulerpartlemb  29757  ccatmulgnn0dir  29945  ofcccat  29946  plymulx0  29950  derangsn  30406  onsucsuccmpi  31612  topdifinffinlem  32371  finixpnum  32564  lindsenlbs  32574  poimirlem26  32605  poimirlem27  32606  poimirlem31  32610  poimirlem32  32611  prdsbnd  32762  heiborlem3  32782  heiborlem8  32787  ismrer1  32807  reheibor  32808  pclfinN  34204  elrfi  36275  mzpcompact2lem  36332  dfac11  36650  pwslnmlem0  36679  lpirlnr  36706  acsfn1p  36788  mpct  38388  fsumsplitsn  38637  dvmptfprodlem  38834  dvnprodlem2  38837  stoweidlem44  38937  fourierdlem51  39050  fourierdlem80  39079  fouriersw  39124  salexct  39228  salexct3  39236  salgencntex  39237  salgensscntex  39238  sge0sn  39272  sge0tsms  39273  sge0cl  39274  sge0sup  39284  sge0iunmptlemfi  39306  sge0splitsn  39334  hoiprodp1  39478  sge0hsphoire  39479  hoidmv1le  39484  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem5  39489  hspmbllem2  39517  ovnovollem3  39548  vonvolmbl  39551  vonvol  39552  vonvol2  39554  fsummmodsnunz  40374  cusgrfilem3  40673  eupth2eucrct  41385  trlsegvdeglem7  41394  fusgreghash2wspv  41499  suppmptcfin  41954  lcosn0  42003  lincext2  42038  snlindsntor  42054
  Copyright terms: Public domain W3C validator