Theorem snfi 9109

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 8687	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 9087	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5112	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3580	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 599	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 9040	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 237	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4680	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 9108	. . . 4 ⊢ ∅ ∈ Fin
10		eleq1 2852	. . . 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 2147  ∃wrex 3090  Vcvv 3454  ∅c0 4281  {csn 4588   class class class wbr 5108  ωcom 7911  1_oc1o 8507   ≈ cen 9008  Fincfn 9011

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-nul 5266  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 2102  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-om 7912  df-1o 8514  df-en 9012  df-fin 9015

This theorem is used by:  fiprc  9110  ssfi  9226  cnvfi  9229  fnfi  9231  sucdom2  9256  fodomfi  9342  pwfi  9348  prfi  9353  prfiALT  9354  tpfi  9355  fodomfir  9357  unifpw  9382  snopfsupp  9420  sniffsupp  9429  ssfii  9448  cantnfp1lem1  9716  hfsn  9957  infpwfidom  10146  ficardadju  10317  ackbij1lem4  10339  ackbij1lem9  10344  ackbij1lem10  10345  fin23lem21  10456  isfin1-3  10503  axcclem  10574  zornn0g  10622  hashsng  14554  hashen1  14555  hashunsng  14577  hashunsngx  14578  hashprg  14580  hashsnlei  14604  hashxplem  14619  hashmap  14621  hashfun  14623  hashbclem  14638  hashf1lem2  14642  hashf1  14643  hash7g  14672  hash3tpexb  14680  s7f1o  15162  fsumsplitsn  15954  fsummsnunz  15964  fsumsplitsnun  15965  fsum2dlem  15980  fsumcom2  15984  ackbijnn  16041  incexclem  16049  isumltss  16061  fprod2dlem  16191  fprodcom2  16195  fprodsplitsn  16200  rexpen  16440  2ebits  16661  lcmfunsnlem2lem1  16857  lcmfunsnlem2lem2  16858  lcmfunsnlem2  16859  lcmfass  16865  phicl2  16989  ramub1lem1  17248  cshwshashnsame  17325  acsfn1  17885  acsfiindd  18777  efmnd1hash  19138  symg1hash  19655  odcau  19869  sylow2alem2  19883  gsumsnfd  20216  gsumzunsnd  20221  gsumunsnfd  20222  gsumpt  20227  ablfac1eu  20340  pgpfaclem2  20349  ablfaclem3  20354  srgbinomlem4  20506  acsfn1p  21107  uvcff  22152  lindsenlbs  22212  psrlidm  22324  psrridm  22325  mvrcl  22354  mplsubrg  22367  mplmon  22399  mplmonmul  22400  psrbagsn  22427  selvvvval  22506  psr1baslem  22558  mat1dimelbas  22841  mat1dim0  22843  mat1dimid  22844  mat1dimmul  22846  mat1dimcrng  22847  mat1f1o  22848  mat1ghm  22853  mat1mhm  22854  mat1rhm  22855  mat1scmat  22909  mvmumamul1  22924  mdetrsca  22973  mdetunilem9  22990  mdetmul  22993  pmatcoe1fsupp  23074  d1mat2pmat  23112  pmatcollpw3fi1lem1  23159  chpmat1dlem  23208  chpmat1d  23209  0cmp  23767  discmp  23771  bwth  23783  disllycmp  23872  dis1stc  23873  locfincmp  23900  dissnlocfin  23903  comppfsc  23906  1stckgenlem  23927  ptpjpre2  23954  ptopn2  23958  xkohaus  24027  xkoptsub  24028  ptcmpfi  24187  cfinufil  24302  ufinffr  24303  fin1aufil  24306  alexsubALTlem3  24423  ptcmplem5  24430  tmdgsum  24469  tsmsxplem1  24527  tsmsxplem2  24528  prdsmet  24744  imasdsf1olem  24747  prdsbl  24865  icccmplem1  25197  icccmplem2  25198  ovolsn  25871  ovolfiniun  25877  volfiniun  25923  i1f0  26063  fta1glem2  26542  fta1blem  26544  plyn0mulidp  26657  fta1lem  26683  vieta1lem2  26689  vieta1  26690  aalioulem2  26717  tayl0  26746  radcnv0  26800  wilthlem2  27453  fsumvma  27597  dchrfi  27639  cusgrfilem3  30095  eupth2eucrct  30875  trlsegvdeglem7  30884  fusgreghash2wspv  30993  ex-hash  31111  fsupprnfi  33382  ffsrn  33416  fsumiunle  33516  elrgspnlem2  33903  elrgspnlem3  33904  fply1  34193  selvply1rhmlema  34261  selvply1rhmlemb  34262  mplidomlem  34270  mplmulmvr  34282  psrmonmul  34293  mplmonprod  34297  vieta  34323  constrfin  34489  locfinref  34584  esumcst  34806  esumsnf  34807  hasheuni  34828  rossros  34924  sibf0  35077  eulerpartlems  35103  eulerpartlemb  35111  ccatmulgnn0dir  35285  ofcccat  35286  prodfzo03  35343  breprexp  35373  hgt750lemb  35396  hgt750leme  35398  lpadlem2  35423  fineqvnttrclselem1  35930  derangsn  36143  onsucsuccmpi  37446  topdifinffinlem  38538  pibt2  38608  finixpnum  38796  poimirlem26  38832  poimirlem27  38833  poimirlem31  38837  poimirlem32  38838  prdsbnd  38993  heiborlem3  39013  heiborlem8  39018  ismrer1  39038  reheibor  39039  pclfinN  41223  frlmvscadiccat  43839  frlmsnic  43870  elrfi  43971  mzpcompact2lem  44028  dfac11  44330  pwslnmlem0  44359  lpirlnr  44384  mpct  46488  cnrefiisplem  47112  dvmptfprodlem  47227  dvnprodlem2  47230  stoweidlem44  47327  fourierdlem51  47440  fourierdlem80  47469  fouriersw  47514  salexct  47617  salexct3  47625  salgencntex  47626  salgensscntex  47627  sge0sn  47662  sge0tsms  47663  sge0cl  47664  sge0sup  47674  sge0iunmptlemfi  47696  sge0splitsn  47724  hoiprodp1  47871  sge0hsphoire  47872  hoidmv1le  47877  hoidmvlelem1  47878  hoidmvlelem2  47879  hoidmvlelem5  47882  hspmbllem2  47910  ovnovollem3  47941  vonvolmbl  47944  vonvol  47945  vonvol2  47947  tmachlem-agreeprod  48220  tmachlem-agreefin  48231  fsummmodsnunz  48726  edgusgrclnbfin  49213  suppmptcfin  49819  lcosn0  49863  lincext2  49898  snlindsntor  49914