Theorem snfi 9047

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 8632	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 9025	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5115	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3583	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 599	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 8978	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 237	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4685	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 9046	. . . 4 ⊢ ∅ ∈ Fin
10		eleq1 2853	. . . 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 2146  ∃wrex 3091  Vcvv 3457  ∅c0 4286  {csn 4591   class class class wbr 5111  ωcom 7868  1_oc1o 8452   ≈ cen 8946  Fincfn 8949

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

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 2569  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-om 7869  df-1o 8459  df-en 8950  df-fin 8953

This theorem is used by:  fiprc  9048  ssfi  9164  cnvfi  9167  fnfi  9169  sucdom2  9194  fodomfi  9279  pwfi  9285  prfi  9290  prfiALT  9291  tpfi  9292  fodomfir  9294  unifpw  9319  snopfsupp  9358  sniffsupp  9367  ssfii  9386  cantnfp1lem1  9654  infpwfidom  10028  ficardadju  10199  ackbij1lem4  10221  ackbij1lem9  10226  ackbij1lem10  10227  fin23lem21  10338  isfin1-3  10385  axcclem  10456  zornn0g  10504  hashsng  14423  hashen1  14424  hashunsng  14446  hashunsngx  14447  hashprg  14449  hashsnlei  14473  hashxplem  14488  hashmap  14490  hashfun  14492  hashbclem  14507  hashf1lem2  14511  hashf1  14512  hash7g  14541  hash3tpexb  14549  s7f1o  15027  fsumsplitsn  15818  fsummsnunz  15828  fsumsplitsnun  15829  fsum2dlem  15844  fsumcom2  15848  ackbijnn  15905  incexclem  15913  isumltss  15925  fprod2dlem  16057  fprodcom2  16061  fprodsplitsn  16066  rexpen  16306  2ebits  16527  lcmfunsnlem2lem1  16718  lcmfunsnlem2lem2  16719  lcmfunsnlem2  16720  lcmfass  16726  phicl2  16849  ramub1lem1  17108  cshwshashnsame  17185  acsfn1  17739  acsfiindd  18631  efmnd1hash  18988  symg1hash  19504  odcau  19718  sylow2alem2  19732  gsumsnfd  20065  gsumzunsnd  20070  gsumunsnfd  20071  gsumpt  20076  ablfac1eu  20189  pgpfaclem2  20198  ablfaclem3  20203  srgbinomlem4  20355  acsfn1p  20952  uvcff  21991  psrlidm  22161  psrridm  22162  mvrcl  22191  mplsubrg  22204  mplmon  22236  mplmonmul  22237  psrbagsn  22264  selvvvval  22343  psr1baslem  22395  mat1dimelbas  22678  mat1dim0  22680  mat1dimid  22681  mat1dimmul  22683  mat1dimcrng  22684  mat1f1o  22685  mat1ghm  22690  mat1mhm  22691  mat1rhm  22692  mat1scmat  22746  mvmumamul1  22761  mdetrsca  22810  mdetunilem9  22827  mdetmul  22830  pmatcoe1fsupp  22908  d1mat2pmat  22946  pmatcollpw3fi1lem1  22993  chpmat1dlem  23042  chpmat1d  23043  0cmp  23601  discmp  23605  bwth  23617  disllycmp  23706  dis1stc  23707  locfincmp  23734  dissnlocfin  23737  comppfsc  23740  1stckgenlem  23761  ptpjpre2  23788  ptopn2  23792  xkohaus  23861  xkoptsub  23862  ptcmpfi  24021  cfinufil  24136  ufinffr  24137  fin1aufil  24140  alexsubALTlem3  24257  ptcmplem5  24264  tmdgsum  24303  tsmsxplem1  24361  tsmsxplem2  24362  prdsmet  24578  imasdsf1olem  24581  prdsbl  24699  icccmplem1  25031  icccmplem2  25032  ovolsn  25705  ovolfiniun  25711  volfiniun  25757  i1f0  25897  fta1glem2  26377  fta1blem  26379  plyn0mulidp  26493  fta1lem  26519  vieta1lem2  26523  vieta1  26524  aalioulem2  26547  tayl0  26576  radcnv0  26630  wilthlem2  27284  fsumvma  27428  dchrfi  27470  cusgrfilem3  29865  eupth2eucrct  30639  trlsegvdeglem7  30648  fusgreghash2wspv  30757  ex-hash  30875  fsupprnfi  33108  ffsrn  33143  fsumiunle  33243  elrgspnlem2  33627  elrgspnlem3  33628  fply1  33912  selvply1rhmlema  33972  selvply1rhmlemb  33973  mplidomlem  33981  mplmulmvr  33993  psrmonmul  34004  mplmonprod  34008  vieta  34034  constrfin  34200  locfinref  34295  esumcst  34517  esumsnf  34518  hasheuni  34539  rossros  34635  sibf0  34789  eulerpartlems  34815  eulerpartlemb  34823  ccatmulgnn0dir  34997  ofcccat  34998  prodfzo03  35055  breprexp  35085  hgt750lemb  35108  hgt750leme  35110  lpadlem2  35135  fineqvnttrclselem1  35591  derangsn  35699  onsucsuccmpi  37011  topdifinffinlem  38050  pibt2  38120  finixpnum  38313  lindsenlbs  38323  poimirlem26  38354  poimirlem27  38355  poimirlem31  38359  poimirlem32  38360  prdsbnd  38502  heiborlem3  38522  heiborlem8  38527  ismrer1  38547  reheibor  38548  pclfinN  40732  frlmvscadiccat  43338  frlmsnic  43366  elrfi  43483  mzpcompact2lem  43540  dfac11  43847  pwslnmlem0  43876  lpirlnr  43902  mpct  45976  cnrefiisplem  46601  dvmptfprodlem  46716  dvnprodlem2  46719  stoweidlem44  46816  fourierdlem51  46929  fourierdlem80  46958  fouriersw  47003  salexct  47106  salexct3  47114  salgencntex  47115  salgensscntex  47116  sge0sn  47151  sge0tsms  47152  sge0cl  47153  sge0sup  47163  sge0iunmptlemfi  47185  sge0splitsn  47213  hoiprodp1  47360  sge0hsphoire  47361  hoidmv1le  47366  hoidmvlelem1  47367  hoidmvlelem2  47368  hoidmvlelem5  47371  hspmbllem2  47399  ovnovollem3  47430  vonvolmbl  47433  vonvol  47434  vonvol2  47436  fsummmodsnunz  48178  edgusgrclnbfin  48665  suppmptcfin  49213  lcosn0  49257  lincext2  49292  snlindsntor  49308