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

Theorem snfi 8023
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 7704 . . . 4 1𝑜 ∈ ω
2 ensn1g 8006 . . . 4 (𝐴 ∈ V → {𝐴} ≈ 1𝑜)
3 breq2 4648 . . . . 5 (𝑥 = 1𝑜 → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1𝑜))
43rspcev 3304 . . . 4 ((1𝑜 ∈ ω ∧ {𝐴} ≈ 1𝑜) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
51, 2, 4sylancr 694 . . 3 (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6 snprc 4244 . . . 4 𝐴 ∈ V ↔ {𝐴} = ∅)
7 en0 8004 . . . . 5 ({𝐴} ≈ ∅ ↔ {𝐴} = ∅)
8 peano1 7070 . . . . . 6 ∅ ∈ ω
9 breq2 4648 . . . . . . 7 (𝑥 = ∅ → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ ∅))
109rspcev 3304 . . . . . 6 ((∅ ∈ ω ∧ {𝐴} ≈ ∅) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
118, 10mpan 705 . . . . 5 ({𝐴} ≈ ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
127, 11sylbir 225 . . . 4 ({𝐴} = ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
136, 12sylbi 207 . . 3 𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
145, 13pm2.61i 176 . 2 𝑥 ∈ ω {𝐴} ≈ 𝑥
15 isfi 7964 . 2 ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
1614, 15mpbir 221 1 {𝐴} ∈ Fin
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1481  wcel 1988  wrex 2910  Vcvv 3195  c0 3907  {csn 4168   class class class wbr 4644  ωcom 7050  1𝑜c1o 7538  cen 7937  Fincfn 7940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-om 7051  df-1o 7545  df-en 7941  df-fin 7944
This theorem is referenced by:  fiprc  8024  prfi  8220  tpfi  8221  fnfi  8223  unifpw  8254  snopfsupp  8283  sniffsupp  8300  ssfii  8310  cantnfp1lem1  8560  infpwfidom  8836  ackbij1lem4  9030  ackbij1lem9  9035  ackbij1lem10  9036  fin23lem21  9146  isfin1-3  9193  axcclem  9264  zornn0g  9312  hashsng  13142  hashen1  13143  hashunsng  13164  hashprg  13165  hashprgOLD  13166  hashsnlei  13189  hashxplem  13203  hashmap  13205  hashfun  13207  hashbclem  13219  hashf1lem1  13222  hashf1lem2  13223  hashf1  13224  fsumsplitsn  14455  fsummsnunz  14464  fsumsplitsnun  14465  fsummsnunzOLD  14466  fsumsplitsnunOLD  14467  fsum2dlem  14482  fsumcom2  14486  fsumcom2OLD  14487  ackbijnn  14541  incexclem  14549  isumltss  14561  fprod2dlem  14691  fprodcom2  14695  fprodcom2OLD  14696  fprodsplitsn  14701  rexpen  14938  2ebits  15150  lcmfunsnlem2lem1  15332  lcmfunsnlem2lem2  15333  lcmfunsnlem2  15334  lcmfass  15340  phicl2  15454  ramub1lem1  15711  cshwshashnsame  15791  acsfn1  16303  acsfiindd  17158  symg1hash  17796  odcau  18000  sylow2alem2  18014  gsumsnfd  18332  gsumzunsnd  18336  gsumunsnfd  18337  gsumpt  18342  ablfac1eu  18453  pgpfaclem2  18462  ablfaclem3  18467  srgbinomlem4  18524  psrlidm  19384  psrridm  19385  mplsubrg  19421  mvrcl  19430  mplmon  19444  mplmonmul  19445  psrbagsn  19476  psr1baslem  19536  uvcff  20111  mat1dimelbas  20258  mat1dim0  20260  mat1dimid  20261  mat1dimmul  20263  mat1dimcrng  20264  mat1f1o  20265  mat1ghm  20270  mat1mhm  20271  mat1rhm  20272  mat1rngiso  20273  mat1scmat  20326  mvmumamul1  20341  mdetrsca  20390  mdetunilem9  20407  mdetmul  20410  pmatcoe1fsupp  20487  d1mat2pmat  20525  pmatcollpw3fi1lem1  20572  chpmat1dlem  20621  chpmat1d  20622  0cmp  21178  discmp  21182  bwth  21194  disllycmp  21282  dis1stc  21283  locfincmp  21310  dissnlocfin  21313  comppfsc  21316  1stckgenlem  21337  ptpjpre2  21364  ptopn2  21368  xkohaus  21437  xkoptsub  21438  ptcmpfi  21597  cfinufil  21713  ufinffr  21714  fin1aufil  21717  alexsubALTlem3  21834  ptcmplem5  21841  tmdgsum  21880  tsmsxplem1  21937  tsmsxplem2  21938  prdsmet  22156  imasdsf1olem  22159  prdsbl  22277  icccmplem1  22606  icccmplem2  22607  ovolsn  23244  ovolfiniun  23250  volfiniun  23296  i1f0  23435  fta1glem2  23907  fta1blem  23909  fta1lem  24043  vieta1lem2  24047  vieta1  24048  aalioulem2  24069  tayl0  24097  radcnv0  24151  wilthlem2  24776  fsumvma  24919  dchrfi  24961  cusgrfilem3  26334  eupth2eucrct  27057  trlsegvdeglem7  27066  fusgreghash2wspv  27173  ex-hash  27280  ffsrn  29478  fsumiunle  29549  locfinref  29882  esumcst  30099  esumsnf  30100  hasheuni  30121  rossros  30217  sibf0  30370  eulerpartlems  30396  eulerpartlemb  30404  ccatmulgnn0dir  30593  ofcccat  30594  plymulx0  30598  prodfzo03  30655  breprexp  30685  hgt750lemb  30708  hgt750leme  30710  derangsn  31126  onsucsuccmpi  32417  topdifinffinlem  33166  finixpnum  33365  lindsenlbs  33375  poimirlem26  33406  poimirlem27  33407  poimirlem31  33411  poimirlem32  33412  prdsbnd  33563  heiborlem3  33583  heiborlem8  33588  ismrer1  33608  reheibor  33609  pclfinN  35005  elrfi  37076  mzpcompact2lem  37133  dfac11  37451  pwslnmlem0  37480  lpirlnr  37506  acsfn1p  37588  mpct  39209  dvmptfprodlem  39922  dvnprodlem2  39925  stoweidlem44  40024  fourierdlem51  40137  fourierdlem80  40166  fouriersw  40211  salexct  40315  salexct3  40323  salgencntex  40324  salgensscntex  40325  sge0sn  40359  sge0tsms  40360  sge0cl  40361  sge0sup  40371  sge0iunmptlemfi  40393  sge0splitsn  40421  hoiprodp1  40565  sge0hsphoire  40566  hoidmv1le  40571  hoidmvlelem1  40572  hoidmvlelem2  40573  hoidmvlelem5  40576  hspmbllem2  40604  ovnovollem3  40635  vonvolmbl  40638  vonvol  40639  vonvol2  40641  fsummmodsnunz  41109  suppmptcfin  41925  lcosn0  41974  lincext2  42009  snlindsntor  42025
  Copyright terms: Public domain W3C validator