Theorem snfi 9083

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 8678	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 9062	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5147	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3622	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 587	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 9016	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 234	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4717	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 9082	. . . 4 ⊢ ∅ ∈ Fin
10		eleq1 2829	. . . 4 ⊢ ({𝐴} = ∅ → ({𝐴} ∈ Fin ↔ ∅ ∈ Fin))
11	9, 10	mpbiri 258	. . 3 ⊢ ({𝐴} = ∅ → {𝐴} ∈ Fin)
12	8, 11	sylbi 217	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴} ∈ Fin)
13	7, 12	pm2.61i 182	1 ⊢ {𝐴} ∈ Fin

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2108  ∃wrex 3070  Vcvv 3480  ∅c0 4333  {csn 4626   class class class wbr 5143  ωcom 7887  1_oc1o 8499   ≈ cen 8982  Fincfn 8985

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-mo 2540  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-om 7888  df-1o 8506  df-en 8986  df-fin 8989

This theorem is referenced by:  fiprc  9085  ssfi  9213  cnvfi  9216  fnfi  9218  sucdom2  9243  fodomfi  9350  imafiOLD  9354  pwfi  9357  prfi  9363  prfiALT  9364  tpfi  9365  fodomfir  9368  unifpw  9395  snopfsupp  9431  sniffsupp  9440  ssfii  9459  cantnfp1lem1  9718  infpwfidom  10068  ficardadju  10240  ackbij1lem4  10262  ackbij1lem9  10267  ackbij1lem10  10268  fin23lem21  10379  isfin1-3  10426  axcclem  10497  zornn0g  10545  hashsng  14408  hashen1  14409  hashunsng  14431  hashunsngx  14432  hashprg  14434  hashsnlei  14457  hashxplem  14472  hashmap  14474  hashfun  14476  hashbclem  14491  hashf1lem2  14495  hashf1  14496  hash7g  14525  hash3tpexb  14533  s7f1o  15005  fsumsplitsn  15780  fsummsnunz  15790  fsumsplitsnun  15791  fsum2dlem  15806  fsumcom2  15810  ackbijnn  15864  incexclem  15872  isumltss  15884  fprod2dlem  16016  fprodcom2  16020  fprodsplitsn  16025  rexpen  16264  2ebits  16484  lcmfunsnlem2lem1  16675  lcmfunsnlem2lem2  16676  lcmfunsnlem2  16677  lcmfass  16683  phicl2  16805  ramub1lem1  17064  cshwshashnsame  17141  acsfn1  17704  acsfiindd  18598  efmnd1hash  18905  symg1hash  19407  odcau  19622  sylow2alem2  19636  gsumsnfd  19969  gsumzunsnd  19974  gsumunsnfd  19975  gsumpt  19980  ablfac1eu  20093  pgpfaclem2  20102  ablfaclem3  20107  srgbinomlem4  20226  acsfn1p  20800  uvcff  21811  psrlidm  21982  psrridm  21983  mvrcl  22012  mplsubrg  22025  mplmon  22053  mplmonmul  22054  psrbagsn  22087  psr1baslem  22186  mat1dimelbas  22477  mat1dim0  22479  mat1dimid  22480  mat1dimmul  22482  mat1dimcrng  22483  mat1f1o  22484  mat1ghm  22489  mat1mhm  22490  mat1rhm  22491  mat1scmat  22545  mvmumamul1  22560  mdetrsca  22609  mdetunilem9  22626  mdetmul  22629  pmatcoe1fsupp  22707  d1mat2pmat  22745  pmatcollpw3fi1lem1  22792  chpmat1dlem  22841  chpmat1d  22842  0cmp  23402  discmp  23406  bwth  23418  disllycmp  23506  dis1stc  23507  locfincmp  23534  dissnlocfin  23537  comppfsc  23540  1stckgenlem  23561  ptpjpre2  23588  ptopn2  23592  xkohaus  23661  xkoptsub  23662  ptcmpfi  23821  cfinufil  23936  ufinffr  23937  fin1aufil  23940  alexsubALTlem3  24057  ptcmplem5  24064  tmdgsum  24103  tsmsxplem1  24161  tsmsxplem2  24162  prdsmet  24380  imasdsf1olem  24383  prdsbl  24504  icccmplem1  24844  icccmplem2  24845  ovolsn  25530  ovolfiniun  25536  volfiniun  25582  i1f0  25722  fta1glem2  26208  fta1blem  26210  fta1lem  26349  vieta1lem2  26353  vieta1  26354  aalioulem2  26375  tayl0  26403  radcnv0  26459  wilthlem2  27112  fsumvma  27257  dchrfi  27299  cusgrfilem3  29475  eupth2eucrct  30236  trlsegvdeglem7  30245  fusgreghash2wspv  30354  ex-hash  30472  fsupprnfi  32701  ffsrn  32740  fsumiunle  32831  elrgspnlem2  33247  elrgspnlem3  33248  fply1  33584  constrfin  33787  locfinref  33840  esumcst  34064  esumsnf  34065  hasheuni  34086  rossros  34181  sibf0  34336  eulerpartlems  34362  eulerpartlemb  34370  ccatmulgnn0dir  34557  ofcccat  34558  plymulx0  34562  prodfzo03  34618  breprexp  34648  hgt750lemb  34671  hgt750leme  34673  lpadlem2  34695  derangsn  35175  onsucsuccmpi  36444  topdifinffinlem  37348  pibt2  37418  finixpnum  37612  lindsenlbs  37622  poimirlem26  37653  poimirlem27  37654  poimirlem31  37658  poimirlem32  37659  prdsbnd  37800  heiborlem3  37820  heiborlem8  37825  ismrer1  37845  reheibor  37846  pclfinN  39902  frlmvscadiccat  42516  frlmsnic  42550  selvvvval  42595  elrfi  42705  mzpcompact2lem  42762  dfac11  43074  pwslnmlem0  43103  lpirlnr  43129  mpct  45206  cnrefiisplem  45844  dvmptfprodlem  45959  dvnprodlem2  45962  stoweidlem44  46059  fourierdlem51  46172  fourierdlem80  46201  fouriersw  46246  salexct  46349  salexct3  46357  salgencntex  46358  salgensscntex  46359  sge0sn  46394  sge0tsms  46395  sge0cl  46396  sge0sup  46406  sge0iunmptlemfi  46428  sge0splitsn  46456  hoiprodp1  46603  sge0hsphoire  46604  hoidmv1le  46609  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem5  46614  hspmbllem2  46642  ovnovollem3  46673  vonvolmbl  46676  vonvol  46677  vonvol2  46679  fsummmodsnunz  47362  edgusgrclnbfin  47828  suppmptcfin  48292  lcosn0  48337  lincext2  48372  snlindsntor  48388