Theorem snfi 9051

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 8629	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 9029	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5107	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3576	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 599	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 8982	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 237	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4678	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 9050	. . . 4 ⊢ ∅ ∈ Fin
10		eleq1 2848	. . . 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

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ∈ wcel 2145  ∃wrex 3086  Vcvv 3450  ∅c0 4279  {csn 4584   class class class wbr 5103  ωcom 7863  1_oc1o 8449   ≈ cen 8950  Fincfn 8953

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-mo 2564  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-om 7864  df-1o 8456  df-en 8954  df-fin 8957

This theorem is used by:  fiprc  9052  ssfi  9168  cnvfi  9171  fnfi  9173  sucdom2  9198  fodomfi  9283  pwfi  9289  prfi  9294  prfiALT  9295  tpfi  9296  fodomfir  9298  unifpw  9323  snopfsupp  9362  sniffsupp  9371  ssfii  9390  cantnfp1lem1  9658  infpwfidom  10032  ficardadju  10203  ackbij1lem4  10225  ackbij1lem9  10230  ackbij1lem10  10231  fin23lem21  10342  isfin1-3  10389  axcclem  10460  zornn0g  10508  hashsng  14434  hashen1  14435  hashunsng  14457  hashunsngx  14458  hashprg  14460  hashsnlei  14484  hashxplem  14499  hashmap  14501  hashfun  14503  hashbclem  14518  hashf1lem2  14522  hashf1  14523  hash7g  14552  hash3tpexb  14560  s7f1o  15040  fsumsplitsn  15831  fsummsnunz  15841  fsumsplitsnun  15842  fsum2dlem  15857  fsumcom2  15861  ackbijnn  15918  incexclem  15926  isumltss  15938  fprod2dlem  16068  fprodcom2  16072  fprodsplitsn  16077  rexpen  16317  2ebits  16538  lcmfunsnlem2lem1  16729  lcmfunsnlem2lem2  16730  lcmfunsnlem2  16731  lcmfass  16737  phicl2  16860  ramub1lem1  17119  cshwshashnsame  17196  acsfn1  17750  acsfiindd  18642  efmnd1hash  19002  symg1hash  19518  odcau  19732  sylow2alem2  19746  gsumsnfd  20079  gsumzunsnd  20084  gsumunsnfd  20085  gsumpt  20090  ablfac1eu  20203  pgpfaclem2  20212  ablfaclem3  20217  srgbinomlem4  20369  acsfn1p  20966  uvcff  22005  lindsenlbs  22065  psrlidm  22177  psrridm  22178  mvrcl  22207  mplsubrg  22220  mplmon  22252  mplmonmul  22253  psrbagsn  22280  selvvvval  22359  psr1baslem  22411  mat1dimelbas  22694  mat1dim0  22696  mat1dimid  22697  mat1dimmul  22699  mat1dimcrng  22700  mat1f1o  22701  mat1ghm  22706  mat1mhm  22707  mat1rhm  22708  mat1scmat  22762  mvmumamul1  22777  mdetrsca  22826  mdetunilem9  22843  mdetmul  22846  pmatcoe1fsupp  22927  d1mat2pmat  22965  pmatcollpw3fi1lem1  23012  chpmat1dlem  23061  chpmat1d  23062  0cmp  23620  discmp  23624  bwth  23636  disllycmp  23725  dis1stc  23726  locfincmp  23753  dissnlocfin  23756  comppfsc  23759  1stckgenlem  23780  ptpjpre2  23807  ptopn2  23811  xkohaus  23880  xkoptsub  23881  ptcmpfi  24040  cfinufil  24155  ufinffr  24156  fin1aufil  24159  alexsubALTlem3  24276  ptcmplem5  24283  tmdgsum  24322  tsmsxplem1  24380  tsmsxplem2  24381  prdsmet  24597  imasdsf1olem  24600  prdsbl  24718  icccmplem1  25050  icccmplem2  25051  ovolsn  25724  ovolfiniun  25730  volfiniun  25776  i1f0  25916  fta1glem2  26395  fta1blem  26397  plyn0mulidp  26512  fta1lem  26538  vieta1lem2  26544  vieta1  26545  aalioulem2  26570  tayl0  26599  radcnv0  26653  wilthlem2  27306  fsumvma  27450  dchrfi  27492  cusgrfilem3  29918  eupth2eucrct  30698  trlsegvdeglem7  30707  fusgreghash2wspv  30816  ex-hash  30934  fsupprnfi  33165  ffsrn  33200  fsumiunle  33300  elrgspnlem2  33684  elrgspnlem3  33685  fply1  33969  selvply1rhmlema  34029  selvply1rhmlemb  34030  mplidomlem  34038  mplmulmvr  34050  psrmonmul  34061  mplmonprod  34065  vieta  34091  constrfin  34257  locfinref  34352  esumcst  34574  esumsnf  34575  hasheuni  34596  rossros  34692  sibf0  34846  eulerpartlems  34872  eulerpartlemb  34880  ccatmulgnn0dir  35054  ofcccat  35055  prodfzo03  35112  breprexp  35142  hgt750lemb  35165  hgt750leme  35167  lpadlem2  35192  fineqvnttrclselem1  35648  derangsn  35750  onsucsuccmpi  37063  topdifinffinlem  38102  pibt2  38172  finixpnum  38360  poimirlem26  38396  poimirlem27  38397  poimirlem31  38401  poimirlem32  38402  prdsbnd  38544  heiborlem3  38564  heiborlem8  38569  ismrer1  38589  reheibor  38590  pclfinN  40774  frlmvscadiccat  43395  frlmsnic  43423  elrfi  43540  mzpcompact2lem  43597  dfac11  43904  pwslnmlem0  43933  lpirlnr  43959  mpct  46033  cnrefiisplem  46658  dvmptfprodlem  46773  dvnprodlem2  46776  stoweidlem44  46873  fourierdlem51  46986  fourierdlem80  47015  fouriersw  47060  salexct  47163  salexct3  47171  salgencntex  47172  salgensscntex  47173  sge0sn  47208  sge0tsms  47209  sge0cl  47210  sge0sup  47220  sge0iunmptlemfi  47242  sge0splitsn  47270  hoiprodp1  47417  sge0hsphoire  47418  hoidmv1le  47423  hoidmvlelem1  47424  hoidmvlelem2  47425  hoidmvlelem5  47428  hspmbllem2  47456  ovnovollem3  47487  vonvolmbl  47490  vonvol  47491  vonvol2  47493  tmachlem-agreeprod  47766  tmachlem-agreefin  47777  fsummmodsnunz  48272  edgusgrclnbfin  48759  suppmptcfin  49307  lcosn0  49351  lincext2  49386  snlindsntor  49402