Theorem snfi 9036

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 8622	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 9015	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5113	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3581	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 598	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 8968	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 237	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4683	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 9035	. . . 4 ⊢ ∅ ∈ Fin
10		eleq1 2851	. . . 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 2143  ∃wrex 3089  Vcvv 3455  ∅c0 4286  {csn 4589   class class class wbr 5109  ωcom 7858  1_oc1o 8442   ≈ cen 8936  Fincfn 8939

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-om 7859  df-1o 8449  df-en 8940  df-fin 8943

This theorem is used by:  fiprc  9037  ssfi  9153  cnvfi  9156  fnfi  9158  sucdom2  9183  fodomfi  9268  pwfi  9274  prfi  9279  prfiALT  9280  tpfi  9281  fodomfir  9283  unifpw  9308  snopfsupp  9347  sniffsupp  9356  ssfii  9375  cantnfp1lem1  9643  infpwfidom  10017  ficardadju  10188  ackbij1lem4  10210  ackbij1lem9  10215  ackbij1lem10  10216  fin23lem21  10327  isfin1-3  10374  axcclem  10445  zornn0g  10493  hashsng  14410  hashen1  14411  hashunsng  14433  hashunsngx  14434  hashprg  14436  hashsnlei  14460  hashxplem  14475  hashmap  14477  hashfun  14479  hashbclem  14494  hashf1lem2  14498  hashf1  14499  hash7g  14528  hash3tpexb  14536  s7f1o  15008  fsumsplitsn  15800  fsummsnunz  15810  fsumsplitsnun  15811  fsum2dlem  15826  fsumcom2  15830  ackbijnn  15887  incexclem  15895  isumltss  15907  fprod2dlem  16039  fprodcom2  16043  fprodsplitsn  16048  rexpen  16288  2ebits  16509  lcmfunsnlem2lem1  16700  lcmfunsnlem2lem2  16701  lcmfunsnlem2  16702  lcmfass  16708  phicl2  16831  ramub1lem1  17090  cshwshashnsame  17167  acsfn1  17721  acsfiindd  18613  efmnd1hash  18955  symg1hash  19464  odcau  19678  sylow2alem2  19692  gsumsnfd  20025  gsumzunsnd  20030  gsumunsnfd  20031  gsumpt  20036  ablfac1eu  20149  pgpfaclem2  20158  ablfaclem3  20163  srgbinomlem4  20315  acsfn1p  20911  uvcff  21950  psrlidm  22120  psrridm  22121  mvrcl  22150  mplsubrg  22163  mplmon  22195  mplmonmul  22196  psrbagsn  22223  selvvvval  22302  psr1baslem  22354  mat1dimelbas  22637  mat1dim0  22639  mat1dimid  22640  mat1dimmul  22642  mat1dimcrng  22643  mat1f1o  22644  mat1ghm  22649  mat1mhm  22650  mat1rhm  22651  mat1scmat  22705  mvmumamul1  22720  mdetrsca  22769  mdetunilem9  22786  mdetmul  22789  pmatcoe1fsupp  22867  d1mat2pmat  22905  pmatcollpw3fi1lem1  22952  chpmat1dlem  23001  chpmat1d  23002  0cmp  23560  discmp  23564  bwth  23576  disllycmp  23664  dis1stc  23665  locfincmp  23692  dissnlocfin  23695  comppfsc  23698  1stckgenlem  23719  ptpjpre2  23746  ptopn2  23750  xkohaus  23819  xkoptsub  23820  ptcmpfi  23979  cfinufil  24094  ufinffr  24095  fin1aufil  24098  alexsubALTlem3  24215  ptcmplem5  24222  tmdgsum  24261  tsmsxplem1  24319  tsmsxplem2  24320  prdsmet  24536  imasdsf1olem  24539  prdsbl  24657  icccmplem1  24989  icccmplem2  24990  ovolsn  25663  ovolfiniun  25669  volfiniun  25715  i1f0  25855  fta1glem2  26335  fta1blem  26337  plyn0mulidp  26451  fta1lem  26477  vieta1lem2  26481  vieta1  26482  aalioulem2  26505  tayl0  26534  radcnv0  26588  wilthlem2  27242  fsumvma  27386  dchrfi  27428  cusgrfilem3  29816  eupth2eucrct  30577  trlsegvdeglem7  30586  fusgreghash2wspv  30695  ex-hash  30813  fsupprnfi  33046  ffsrn  33082  fsumiunle  33182  elrgspnlem2  33572  elrgspnlem3  33573  fply1  33857  selvply1rhmlema  33917  selvply1rhmlemb  33918  mplidomlem  33926  mplmulmvr  33938  psrmonmul  33949  mplmonprod  33953  vieta  33979  constrfin  34145  locfinref  34240  esumcst  34462  esumsnf  34463  hasheuni  34484  rossros  34579  sibf0  34733  eulerpartlems  34759  eulerpartlemb  34767  ccatmulgnn0dir  34941  ofcccat  34942  prodfzo03  34999  breprexp  35029  hgt750lemb  35052  hgt750leme  35054  lpadlem2  35079  fineqvnttrclselem1  35542  derangsn  35670  onsucsuccmpi  36982  topdifinffinlem  38021  pibt2  38091  finixpnum  38284  lindsenlbs  38294  poimirlem26  38325  poimirlem27  38326  poimirlem31  38330  poimirlem32  38331  prdsbnd  38472  heiborlem3  38492  heiborlem8  38497  ismrer1  38517  reheibor  38518  pclfinN  40702  frlmvscadiccat  43308  frlmsnic  43336  elrfi  43453  mzpcompact2lem  43510  dfac11  43817  pwslnmlem0  43846  lpirlnr  43872  mpct  45946  cnrefiisplem  46571  dvmptfprodlem  46686  dvnprodlem2  46689  stoweidlem44  46786  fourierdlem51  46899  fourierdlem80  46928  fouriersw  46973  salexct  47076  salexct3  47084  salgencntex  47085  salgensscntex  47086  sge0sn  47121  sge0tsms  47122  sge0cl  47123  sge0sup  47133  sge0iunmptlemfi  47155  sge0splitsn  47183  hoiprodp1  47330  sge0hsphoire  47331  hoidmv1le  47336  hoidmvlelem1  47337  hoidmvlelem2  47338  hoidmvlelem5  47341  hspmbllem2  47369  ovnovollem3  47400  vonvolmbl  47403  vonvol  47404  vonvol2  47406  fsummmodsnunz  48148  edgusgrclnbfin  48635  suppmptcfin  49184  lcosn0  49228  lincext2  49263  snlindsntor  49279