Theorem snfi 9039

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 8625	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 9018	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5117	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3590	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 598	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 8971	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 237	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4688	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 9038	. . . 4 ⊢ ∅ ∈ Fin
10		eleq1 2857	. . . 4 ⊢ ({𝐴} = ∅ → ({𝐴} ∈ Fin ↔ ∅ ∈ Fin))
11	9, 10	mpbiri 261	. . 3 ⊢ ({𝐴} = ∅ → {𝐴} ∈ Fin)
12	8, 11	sylbi 220	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴} ∈ Fin)
13	7, 12	pm2.61i 184	1 ⊢ {𝐴} ∈ Fin

Syntax hints:  ¬ wn 3   = wceq 1567   ∈ wcel 2149  ∃wrex 3095  Vcvv 3463  ∅c0 4294  {csn 4594   class class class wbr 5113  ωcom 7861  1_oc1o 8445   ≈ cen 8939  Fincfn 8942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-mo 2573  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-om 7862  df-1o 8452  df-en 8943  df-fin 8946

This theorem is referenced by:  fiprc  9040  ssfi  9156  cnvfi  9159  fnfi  9161  sucdom2  9186  fodomfi  9271  pwfi  9277  prfi  9282  prfiALT  9283  tpfi  9284  fodomfir  9286  unifpw  9311  snopfsupp  9350  sniffsupp  9359  ssfii  9378  cantnfp1lem1  9646  infpwfidom  10011  ficardadju  10182  ackbij1lem4  10204  ackbij1lem9  10209  ackbij1lem10  10210  fin23lem21  10322  isfin1-3  10369  axcclem  10440  zornn0g  10488  hashsng  14404  hashen1  14405  hashunsng  14427  hashunsngx  14428  hashprg  14430  hashsnlei  14454  hashxplem  14469  hashmap  14471  hashfun  14473  hashbclem  14488  hashf1lem2  14492  hashf1  14493  hash7g  14522  hash3tpexb  14530  s7f1o  15002  fsumsplitsn  15794  fsummsnunz  15804  fsumsplitsnun  15805  fsum2dlem  15820  fsumcom2  15824  ackbijnn  15881  incexclem  15889  isumltss  15901  fprod2dlem  16033  fprodcom2  16037  fprodsplitsn  16042  rexpen  16283  2ebits  16504  lcmfunsnlem2lem1  16695  lcmfunsnlem2lem2  16696  lcmfunsnlem2  16697  lcmfass  16703  phicl2  16826  ramub1lem1  17085  cshwshashnsame  17162  acsfn1  17716  acsfiindd  18608  efmnd1hash  18950  symg1hash  19459  odcau  19673  sylow2alem2  19687  gsumsnfd  20020  gsumzunsnd  20025  gsumunsnfd  20026  gsumpt  20031  ablfac1eu  20144  pgpfaclem2  20153  ablfaclem3  20158  srgbinomlem4  20310  acsfn1p  20879  uvcff  21909  psrlidm  22079  psrridm  22080  mvrcl  22109  mplsubrg  22122  mplmon  22154  mplmonmul  22155  psrbagsn  22182  selvvvval  22261  psr1baslem  22313  mat1dimelbas  22596  mat1dim0  22598  mat1dimid  22599  mat1dimmul  22601  mat1dimcrng  22602  mat1f1o  22603  mat1ghm  22608  mat1mhm  22609  mat1rhm  22610  mat1scmat  22664  mvmumamul1  22679  mdetrsca  22728  mdetunilem9  22745  mdetmul  22748  pmatcoe1fsupp  22826  d1mat2pmat  22864  pmatcollpw3fi1lem1  22911  chpmat1dlem  22960  chpmat1d  22961  0cmp  23519  discmp  23523  bwth  23535  disllycmp  23623  dis1stc  23624  locfincmp  23651  dissnlocfin  23654  comppfsc  23657  1stckgenlem  23678  ptpjpre2  23705  ptopn2  23709  xkohaus  23778  xkoptsub  23779  ptcmpfi  23938  cfinufil  24053  ufinffr  24054  fin1aufil  24057  alexsubALTlem3  24174  ptcmplem5  24181  tmdgsum  24220  tsmsxplem1  24278  tsmsxplem2  24279  prdsmet  24495  imasdsf1olem  24498  prdsbl  24616  icccmplem1  24948  icccmplem2  24949  ovolsn  25622  ovolfiniun  25628  volfiniun  25674  i1f0  25814  fta1glem2  26294  fta1blem  26296  plyn0mulidp  26410  fta1lem  26436  vieta1lem2  26440  vieta1  26441  aalioulem2  26462  tayl0  26490  radcnv0  26544  wilthlem2  27198  fsumvma  27342  dchrfi  27384  cusgrfilem3  29747  eupth2eucrct  30508  trlsegvdeglem7  30517  fusgreghash2wspv  30626  ex-hash  30744  fsupprnfi  32977  ffsrn  33013  fsumiunle  33113  elrgspnlem2  33503  elrgspnlem3  33504  fply1  33792  selvply1rhmlema  33852  selvply1rhmlemb  33853  mplidomlem  33861  mplmulmvr  33873  psrmonmul  33884  mplmonprod  33888  vieta  33914  constrfin  34080  locfinref  34175  esumcst  34397  esumsnf  34398  hasheuni  34419  rossros  34514  sibf0  34668  eulerpartlems  34694  eulerpartlemb  34702  ccatmulgnn0dir  34876  ofcccat  34877  prodfzo03  34934  breprexp  34964  hgt750lemb  34987  hgt750leme  34989  lpadlem2  35014  fineqvnttrclselem1  35456  derangsn  35560  onsucsuccmpi  36842  topdifinffinlem  37880  pibt2  37950  finixpnum  38143  lindsenlbs  38153  poimirlem26  38184  poimirlem27  38185  poimirlem31  38189  poimirlem32  38190  prdsbnd  38331  heiborlem3  38351  heiborlem8  38356  ismrer1  38376  reheibor  38377  pclfinN  40563  frlmvscadiccat  43169  frlmsnic  43199  elrfi  43316  mzpcompact2lem  43373  dfac11  43680  pwslnmlem0  43709  lpirlnr  43735  mpct  45809  cnrefiisplem  46434  dvmptfprodlem  46549  dvnprodlem2  46552  stoweidlem44  46649  fourierdlem51  46762  fourierdlem80  46791  fouriersw  46836  salexct  46939  salexct3  46947  salgencntex  46948  salgensscntex  46949  sge0sn  46984  sge0tsms  46985  sge0cl  46986  sge0sup  46996  sge0iunmptlemfi  47018  sge0splitsn  47046  hoiprodp1  47193  sge0hsphoire  47194  hoidmv1le  47199  hoidmvlelem1  47200  hoidmvlelem2  47201  hoidmvlelem5  47204  hspmbllem2  47232  ovnovollem3  47263  vonvolmbl  47266  vonvol  47267  vonvol2  47269  fsummmodsnunz  48008  edgusgrclnbfin  48495  suppmptcfin  49040  lcosn0  49084  lincext2  49119  snlindsntor  49135