Theorem snfi 8980

Description: A singleton is finite. (Contributed by NM, 4-Nov-2002.) (Proof shortened by BTernaryTau, 13-Jan-2025.)

Assertion

Ref	Expression
snfi	⊢ {𝐴} ∈ Fin

Proof of Theorem snfi

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		1onn 8566	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 8959	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5076	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3560	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 593	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 8912	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 235	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4649	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 8979	. . . 4 ⊢ ∅ ∈ Fin
10		eleq1 2827	. . . 4 ⊢ ({𝐴} = ∅ → ({𝐴} ∈ Fin ↔ ∅ ∈ Fin))
11	9, 10	mpbiri 259	. . 3 ⊢ ({𝐴} = ∅ → {𝐴} ∈ Fin)
12	8, 11	sylbi 218	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴} ∈ Fin)
13	7, 12	pm2.61i 183	1 ⊢ {𝐴} ∈ Fin

Syntax hints:  ¬ wn 3   = wceq 1547   ∈ wcel 2119  ∃wrex 3063  Vcvv 3431  ∅c0 4261  {csn 4555   class class class wbr 5072  ωcom 7806  1_oc1o 8388   ≈ cen 8880  Fincfn 8883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-mo 2543  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-om 7807  df-1o 8395  df-en 8884  df-fin 8887

This theorem is referenced by:  fiprc  8981  ssfi  9097  cnvfi  9100  fnfi  9102  sucdom2  9127  fodomfi  9212  imafiOLD  9216  pwfi  9219  prfi  9224  prfiALT  9225  tpfi  9226  fodomfir  9228  unifpw  9255  snopfsupp  9294  sniffsupp  9303  ssfii  9322  cantnfp1lem1  9590  infpwfidom  9941  ficardadju  10113  ackbij1lem4  10135  ackbij1lem9  10140  ackbij1lem10  10141  fin23lem21  10252  isfin1-3  10299  axcclem  10370  zornn0g  10418  hashsng  14322  hashen1  14323  hashunsng  14345  hashunsngx  14346  hashprg  14348  hashsnlei  14371  hashxplem  14386  hashmap  14388  hashfun  14390  hashbclem  14405  hashf1lem2  14409  hashf1  14410  hash7g  14439  hash3tpexb  14447  s7f1o  14919  fsumsplitsn  15697  fsummsnunz  15707  fsumsplitsnun  15708  fsum2dlem  15723  fsumcom2  15727  ackbijnn  15784  incexclem  15792  isumltss  15804  fprod2dlem  15936  fprodcom2  15940  fprodsplitsn  15945  rexpen  16186  2ebits  16407  lcmfunsnlem2lem1  16598  lcmfunsnlem2lem2  16599  lcmfunsnlem2  16600  lcmfass  16606  phicl2  16729  ramub1lem1  16988  cshwshashnsame  17065  acsfn1  17618  acsfiindd  18510  efmnd1hash  18851  symg1hash  19356  odcau  19570  sylow2alem2  19584  gsumsnfd  19917  gsumzunsnd  19922  gsumunsnfd  19923  gsumpt  19928  ablfac1eu  20041  pgpfaclem2  20050  ablfaclem3  20055  srgbinomlem4  20201  acsfn1p  20771  uvcff  21766  psrlidm  21936  psrridm  21937  mvrcl  21966  mplsubrg  21979  mplmon  22011  mplmonmul  22012  psrbagsn  22039  selvvvval  22118  psr1baslem  22170  mat1dimelbas  22454  mat1dim0  22456  mat1dimid  22457  mat1dimmul  22459  mat1dimcrng  22460  mat1f1o  22461  mat1ghm  22466  mat1mhm  22467  mat1rhm  22468  mat1scmat  22522  mvmumamul1  22537  mdetrsca  22586  mdetunilem9  22603  mdetmul  22606  pmatcoe1fsupp  22684  d1mat2pmat  22722  pmatcollpw3fi1lem1  22769  chpmat1dlem  22818  chpmat1d  22819  0cmp  23377  discmp  23381  bwth  23393  disllycmp  23481  dis1stc  23482  locfincmp  23509  dissnlocfin  23512  comppfsc  23515  1stckgenlem  23536  ptpjpre2  23563  ptopn2  23567  xkohaus  23636  xkoptsub  23637  ptcmpfi  23796  cfinufil  23911  ufinffr  23912  fin1aufil  23915  alexsubALTlem3  24032  ptcmplem5  24039  tmdgsum  24078  tsmsxplem1  24136  tsmsxplem2  24137  prdsmet  24353  imasdsf1olem  24356  prdsbl  24474  icccmplem1  24806  icccmplem2  24807  ovolsn  25480  ovolfiniun  25486  volfiniun  25532  i1f0  25672  fta1glem2  26152  fta1blem  26154  fta1lem  26291  vieta1lem2  26295  vieta1  26296  aalioulem2  26317  tayl0  26345  radcnv0  26399  wilthlem2  27050  fsumvma  27194  dchrfi  27236  cusgrfilem3  29544  eupth2eucrct  30305  trlsegvdeglem7  30314  fusgreghash2wspv  30423  ex-hash  30541  fsupprnfi  32784  ffsrn  32820  fsumiunle  32921  elrgspnlem2  33324  elrgspnlem3  33325  fply1  33641  selvply1rhmlema  33702  selvply1rhmlemb  33703  mplidomlem  33711  mplmulmvr  33723  psrmonmul  33734  mplmonprod  33738  vieta  33764  constrfin  33930  locfinref  34025  esumcst  34247  esumsnf  34248  hasheuni  34269  rossros  34364  sibf0  34518  eulerpartlems  34544  eulerpartlemb  34552  ccatmulgnn0dir  34726  ofcccat  34727  plymulx0  34731  prodfzo03  34787  breprexp  34817  hgt750lemb  34840  hgt750leme  34842  lpadlem2  34864  fineqvnttrclselem1  35302  derangsn  35398  onsucsuccmpi  36671  topdifinffinlem  37709  pibt2  37779  finixpnum  37972  lindsenlbs  37982  poimirlem26  38013  poimirlem27  38014  poimirlem31  38018  poimirlem32  38019  prdsbnd  38160  heiborlem3  38180  heiborlem8  38185  ismrer1  38205  reheibor  38206  pclfinN  40392  frlmvscadiccat  42996  frlmsnic  43026  elrfi  43143  mzpcompact2lem  43200  dfac11  43507  pwslnmlem0  43536  lpirlnr  43562  mpct  45647  cnrefiisplem  46272  dvmptfprodlem  46387  dvnprodlem2  46390  stoweidlem44  46487  fourierdlem51  46600  fourierdlem80  46629  fouriersw  46674  salexct  46777  salexct3  46785  salgencntex  46786  salgensscntex  46787  sge0sn  46822  sge0tsms  46823  sge0cl  46824  sge0sup  46834  sge0iunmptlemfi  46856  sge0splitsn  46884  hoiprodp1  47031  sge0hsphoire  47032  hoidmv1le  47037  hoidmvlelem1  47038  hoidmvlelem2  47039  hoidmvlelem5  47042  hspmbllem2  47070  ovnovollem3  47101  vonvolmbl  47104  vonvol  47105  vonvol2  47107  fsummmodsnunz  47846  edgusgrclnbfin  48333  suppmptcfin  48867  lcosn0  48911  lincext2  48946  snlindsntor  48962