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

Theorem snfi 8205
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 7890 . . . 4 1𝑜 ∈ ω
2 ensn1g 8188 . . . 4 (𝐴 ∈ V → {𝐴} ≈ 1𝑜)
3 breq2 4808 . . . . 5 (𝑥 = 1𝑜 → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1𝑜))
43rspcev 3449 . . . 4 ((1𝑜 ∈ ω ∧ {𝐴} ≈ 1𝑜) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
51, 2, 4sylancr 698 . . 3 (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6 snprc 4397 . . . 4 𝐴 ∈ V ↔ {𝐴} = ∅)
7 en0 8186 . . . . 5 ({𝐴} ≈ ∅ ↔ {𝐴} = ∅)
8 peano1 7251 . . . . . 6 ∅ ∈ ω
9 breq2 4808 . . . . . . 7 (𝑥 = ∅ → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ ∅))
109rspcev 3449 . . . . . 6 ((∅ ∈ ω ∧ {𝐴} ≈ ∅) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
118, 10mpan 708 . . . . 5 ({𝐴} ≈ ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
127, 11sylbir 225 . . . 4 ({𝐴} = ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
136, 12sylbi 207 . . 3 𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
145, 13pm2.61i 176 . 2 𝑥 ∈ ω {𝐴} ≈ 𝑥
15 isfi 8147 . 2 ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
1614, 15mpbir 221 1 {𝐴} ∈ Fin
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1632  wcel 2139  wrex 3051  Vcvv 3340  c0 4058  {csn 4321   class class class wbr 4804  ωcom 7231  1𝑜c1o 7723  cen 8120  Fincfn 8123
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-om 7232  df-1o 7730  df-en 8124  df-fin 8127
This theorem is referenced by:  fiprc  8206  prfi  8402  tpfi  8403  fnfi  8405  unifpw  8436  snopfsupp  8465  sniffsupp  8482  ssfii  8492  cantnfp1lem1  8750  infpwfidom  9061  ackbij1lem4  9257  ackbij1lem9  9262  ackbij1lem10  9263  fin23lem21  9373  isfin1-3  9420  axcclem  9491  zornn0g  9539  hashsng  13371  hashen1  13372  hashunsng  13393  hashprg  13394  hashprgOLD  13395  hashsnlei  13418  hashxplem  13432  hashmap  13434  hashfun  13436  hashbclem  13448  hashf1lem1  13451  hashf1lem2  13452  hashf1  13453  fsumsplitsn  14693  fsummsnunz  14702  fsumsplitsnun  14703  fsummsnunzOLD  14704  fsumsplitsnunOLD  14705  fsum2dlem  14720  fsumcom2  14724  fsumcom2OLD  14725  ackbijnn  14779  incexclem  14787  isumltss  14799  fprod2dlem  14929  fprodcom2  14933  fprodcom2OLD  14934  fprodsplitsn  14939  rexpen  15176  2ebits  15391  lcmfunsnlem2lem1  15573  lcmfunsnlem2lem2  15574  lcmfunsnlem2  15575  lcmfass  15581  phicl2  15695  ramub1lem1  15952  cshwshashnsame  16032  acsfn1  16543  acsfiindd  17398  symg1hash  18035  odcau  18239  sylow2alem2  18253  gsumsnfd  18571  gsumzunsnd  18575  gsumunsnfd  18576  gsumpt  18581  ablfac1eu  18692  pgpfaclem2  18701  ablfaclem3  18706  srgbinomlem4  18763  psrlidm  19625  psrridm  19626  mplsubrg  19662  mvrcl  19671  mplmon  19685  mplmonmul  19686  psrbagsn  19717  psr1baslem  19777  uvcff  20352  mat1dimelbas  20499  mat1dim0  20501  mat1dimid  20502  mat1dimmul  20504  mat1dimcrng  20505  mat1f1o  20506  mat1ghm  20511  mat1mhm  20512  mat1rhm  20513  mat1rngiso  20514  mat1scmat  20567  mvmumamul1  20582  mdetrsca  20631  mdetunilem9  20648  mdetmul  20651  pmatcoe1fsupp  20728  d1mat2pmat  20766  pmatcollpw3fi1lem1  20813  chpmat1dlem  20862  chpmat1d  20863  0cmp  21419  discmp  21423  bwth  21435  disllycmp  21523  dis1stc  21524  locfincmp  21551  dissnlocfin  21554  comppfsc  21557  1stckgenlem  21578  ptpjpre2  21605  ptopn2  21609  xkohaus  21678  xkoptsub  21679  ptcmpfi  21838  cfinufil  21953  ufinffr  21954  fin1aufil  21957  alexsubALTlem3  22074  ptcmplem5  22081  tmdgsum  22120  tsmsxplem1  22177  tsmsxplem2  22178  prdsmet  22396  imasdsf1olem  22399  prdsbl  22517  icccmplem1  22846  icccmplem2  22847  ovolsn  23483  ovolfiniun  23489  volfiniun  23535  i1f0  23673  fta1glem2  24145  fta1blem  24147  fta1lem  24281  vieta1lem2  24285  vieta1  24286  aalioulem2  24307  tayl0  24335  radcnv0  24389  wilthlem2  25015  fsumvma  25158  dchrfi  25200  cusgrfilem3  26584  eupth2eucrct  27390  trlsegvdeglem7  27399  fusgreghash2wspv  27510  ex-hash  27642  ffsrn  29834  fsumiunle  29905  locfinref  30238  esumcst  30455  esumsnf  30456  hasheuni  30477  rossros  30573  sibf0  30726  eulerpartlems  30752  eulerpartlemb  30760  ccatmulgnn0dir  30949  ofcccat  30950  plymulx0  30954  prodfzo03  31011  breprexp  31041  hgt750lemb  31064  hgt750leme  31066  derangsn  31480  onsucsuccmpi  32769  topdifinffinlem  33524  finixpnum  33725  lindsenlbs  33735  poimirlem26  33766  poimirlem27  33767  poimirlem31  33771  poimirlem32  33772  prdsbnd  33923  heiborlem3  33943  heiborlem8  33948  ismrer1  33968  reheibor  33969  pclfinN  35707  elrfi  37777  mzpcompact2lem  37834  dfac11  38152  pwslnmlem0  38181  lpirlnr  38207  acsfn1p  38289  mpct  39910  cnrefiisplem  40576  dvmptfprodlem  40680  dvnprodlem2  40683  stoweidlem44  40782  fourierdlem51  40895  fourierdlem80  40924  fouriersw  40969  salexct  41073  salexct3  41081  salgencntex  41082  salgensscntex  41083  sge0sn  41117  sge0tsms  41118  sge0cl  41119  sge0sup  41129  sge0iunmptlemfi  41151  sge0splitsn  41179  hoiprodp1  41326  sge0hsphoire  41327  hoidmv1le  41332  hoidmvlelem1  41333  hoidmvlelem2  41334  hoidmvlelem5  41337  hspmbllem2  41365  ovnovollem3  41396  vonvolmbl  41399  vonvol  41400  vonvol2  41402  fsummmodsnunz  41873  suppmptcfin  42688  lcosn0  42737  lincext2  42772  snlindsntor  42788
  Copyright terms: Public domain W3C validator