Theorem snfi 9014

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 8604	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 8993	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5111	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3588	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 587	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 8947	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 234	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4681	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 9013	. . . 4 ⊢ ∅ ∈ Fin
10		eleq1 2816	. . . 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 2109  ∃wrex 3053  Vcvv 3447  ∅c0 4296  {csn 4589   class class class wbr 5107  ωcom 7842  1_oc1o 8427   ≈ cen 8915  Fincfn 8918

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 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-mo 2533  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-om 7843  df-1o 8434  df-en 8919  df-fin 8922

This theorem is referenced by:  fiprc  9016  ssfi  9137  cnvfi  9140  fnfi  9142  sucdom2  9167  fodomfi  9261  imafiOLD  9265  pwfi  9268  prfi  9274  prfiALT  9275  tpfi  9276  fodomfir  9279  unifpw  9306  snopfsupp  9342  sniffsupp  9351  ssfii  9370  cantnfp1lem1  9631  infpwfidom  9981  ficardadju  10153  ackbij1lem4  10175  ackbij1lem9  10180  ackbij1lem10  10181  fin23lem21  10292  isfin1-3  10339  axcclem  10410  zornn0g  10458  hashsng  14334  hashen1  14335  hashunsng  14357  hashunsngx  14358  hashprg  14360  hashsnlei  14383  hashxplem  14398  hashmap  14400  hashfun  14402  hashbclem  14417  hashf1lem2  14421  hashf1  14422  hash7g  14451  hash3tpexb  14459  s7f1o  14932  fsumsplitsn  15710  fsummsnunz  15720  fsumsplitsnun  15721  fsum2dlem  15736  fsumcom2  15740  ackbijnn  15794  incexclem  15802  isumltss  15814  fprod2dlem  15946  fprodcom2  15950  fprodsplitsn  15955  rexpen  16196  2ebits  16417  lcmfunsnlem2lem1  16608  lcmfunsnlem2lem2  16609  lcmfunsnlem2  16610  lcmfass  16616  phicl2  16738  ramub1lem1  16997  cshwshashnsame  17074  acsfn1  17622  acsfiindd  18512  efmnd1hash  18819  symg1hash  19320  odcau  19534  sylow2alem2  19548  gsumsnfd  19881  gsumzunsnd  19886  gsumunsnfd  19887  gsumpt  19892  ablfac1eu  20005  pgpfaclem2  20014  ablfaclem3  20019  srgbinomlem4  20138  acsfn1p  20708  uvcff  21700  psrlidm  21871  psrridm  21872  mvrcl  21901  mplsubrg  21914  mplmon  21942  mplmonmul  21943  psrbagsn  21970  psr1baslem  22069  mat1dimelbas  22358  mat1dim0  22360  mat1dimid  22361  mat1dimmul  22363  mat1dimcrng  22364  mat1f1o  22365  mat1ghm  22370  mat1mhm  22371  mat1rhm  22372  mat1scmat  22426  mvmumamul1  22441  mdetrsca  22490  mdetunilem9  22507  mdetmul  22510  pmatcoe1fsupp  22588  d1mat2pmat  22626  pmatcollpw3fi1lem1  22673  chpmat1dlem  22722  chpmat1d  22723  0cmp  23281  discmp  23285  bwth  23297  disllycmp  23385  dis1stc  23386  locfincmp  23413  dissnlocfin  23416  comppfsc  23419  1stckgenlem  23440  ptpjpre2  23467  ptopn2  23471  xkohaus  23540  xkoptsub  23541  ptcmpfi  23700  cfinufil  23815  ufinffr  23816  fin1aufil  23819  alexsubALTlem3  23936  ptcmplem5  23943  tmdgsum  23982  tsmsxplem1  24040  tsmsxplem2  24041  prdsmet  24258  imasdsf1olem  24261  prdsbl  24379  icccmplem1  24711  icccmplem2  24712  ovolsn  25396  ovolfiniun  25402  volfiniun  25448  i1f0  25588  fta1glem2  26074  fta1blem  26076  fta1lem  26215  vieta1lem2  26219  vieta1  26220  aalioulem2  26241  tayl0  26269  radcnv0  26325  wilthlem2  26979  fsumvma  27124  dchrfi  27166  cusgrfilem3  29385  eupth2eucrct  30146  trlsegvdeglem7  30155  fusgreghash2wspv  30264  ex-hash  30382  fsupprnfi  32615  ffsrn  32652  fsumiunle  32754  elrgspnlem2  33194  elrgspnlem3  33195  fply1  33527  constrfin  33736  locfinref  33831  esumcst  34053  esumsnf  34054  hasheuni  34075  rossros  34170  sibf0  34325  eulerpartlems  34351  eulerpartlemb  34359  ccatmulgnn0dir  34533  ofcccat  34534  plymulx0  34538  prodfzo03  34594  breprexp  34624  hgt750lemb  34647  hgt750leme  34649  lpadlem2  34671  derangsn  35157  onsucsuccmpi  36431  topdifinffinlem  37335  pibt2  37405  finixpnum  37599  lindsenlbs  37609  poimirlem26  37640  poimirlem27  37641  poimirlem31  37645  poimirlem32  37646  prdsbnd  37787  heiborlem3  37807  heiborlem8  37812  ismrer1  37832  reheibor  37833  pclfinN  39894  frlmvscadiccat  42494  frlmsnic  42528  selvvvval  42573  elrfi  42682  mzpcompact2lem  42739  dfac11  43051  pwslnmlem0  43080  lpirlnr  43106  mpct  45195  cnrefiisplem  45827  dvmptfprodlem  45942  dvnprodlem2  45945  stoweidlem44  46042  fourierdlem51  46155  fourierdlem80  46184  fouriersw  46229  salexct  46332  salexct3  46340  salgencntex  46341  salgensscntex  46342  sge0sn  46377  sge0tsms  46378  sge0cl  46379  sge0sup  46389  sge0iunmptlemfi  46411  sge0splitsn  46439  hoiprodp1  46586  sge0hsphoire  46587  hoidmv1le  46592  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem5  46597  hspmbllem2  46625  ovnovollem3  46656  vonvolmbl  46659  vonvol  46660  vonvol2  46662  fsummmodsnunz  47376  edgusgrclnbfin  47842  suppmptcfin  48364  lcosn0  48409  lincext2  48444  snlindsntor  48460