Theorem snfi 8984

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 8570	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 8963	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5090	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3565	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 588	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 8916	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 234	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4662	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 8983	. . . 4 ⊢ ∅ ∈ Fin
10		eleq1 2825	. . . 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 1542   ∈ wcel 2114  ∃wrex 3062  Vcvv 3430  ∅c0 4274  {csn 4568   class class class wbr 5086  ωcom 7811  1_oc1o 8392   ≈ cen 8884  Fincfn 8887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-om 7812  df-1o 8399  df-en 8888  df-fin 8891

This theorem is referenced by:  fiprc  8985  ssfi  9101  cnvfi  9104  fnfi  9106  sucdom2  9131  fodomfi  9216  imafiOLD  9220  pwfi  9223  prfi  9228  prfiALT  9229  tpfi  9230  fodomfir  9232  unifpw  9259  snopfsupp  9298  sniffsupp  9307  ssfii  9326  cantnfp1lem1  9593  infpwfidom  9944  ficardadju  10116  ackbij1lem4  10138  ackbij1lem9  10143  ackbij1lem10  10144  fin23lem21  10255  isfin1-3  10302  axcclem  10373  zornn0g  10421  hashsng  14325  hashen1  14326  hashunsng  14348  hashunsngx  14349  hashprg  14351  hashsnlei  14374  hashxplem  14389  hashmap  14391  hashfun  14393  hashbclem  14408  hashf1lem2  14412  hashf1  14413  hash7g  14442  hash3tpexb  14450  s7f1o  14922  fsumsplitsn  15700  fsummsnunz  15710  fsumsplitsnun  15711  fsum2dlem  15726  fsumcom2  15730  ackbijnn  15787  incexclem  15795  isumltss  15807  fprod2dlem  15939  fprodcom2  15943  fprodsplitsn  15948  rexpen  16189  2ebits  16410  lcmfunsnlem2lem1  16601  lcmfunsnlem2lem2  16602  lcmfunsnlem2  16603  lcmfass  16609  phicl2  16732  ramub1lem1  16991  cshwshashnsame  17068  acsfn1  17621  acsfiindd  18513  efmnd1hash  18854  symg1hash  19359  odcau  19573  sylow2alem2  19587  gsumsnfd  19920  gsumzunsnd  19925  gsumunsnfd  19926  gsumpt  19931  ablfac1eu  20044  pgpfaclem2  20053  ablfaclem3  20058  srgbinomlem4  20204  acsfn1p  20770  uvcff  21784  psrlidm  21953  psrridm  21954  mvrcl  21983  mplsubrg  21996  mplmon  22026  mplmonmul  22027  psrbagsn  22054  psr1baslem  22161  mat1dimelbas  22449  mat1dim0  22451  mat1dimid  22452  mat1dimmul  22454  mat1dimcrng  22455  mat1f1o  22456  mat1ghm  22461  mat1mhm  22462  mat1rhm  22463  mat1scmat  22517  mvmumamul1  22532  mdetrsca  22581  mdetunilem9  22598  mdetmul  22601  pmatcoe1fsupp  22679  d1mat2pmat  22717  pmatcollpw3fi1lem1  22764  chpmat1dlem  22813  chpmat1d  22814  0cmp  23372  discmp  23376  bwth  23388  disllycmp  23476  dis1stc  23477  locfincmp  23504  dissnlocfin  23507  comppfsc  23510  1stckgenlem  23531  ptpjpre2  23558  ptopn2  23562  xkohaus  23631  xkoptsub  23632  ptcmpfi  23791  cfinufil  23906  ufinffr  23907  fin1aufil  23910  alexsubALTlem3  24027  ptcmplem5  24034  tmdgsum  24073  tsmsxplem1  24131  tsmsxplem2  24132  prdsmet  24348  imasdsf1olem  24351  prdsbl  24469  icccmplem1  24801  icccmplem2  24802  ovolsn  25475  ovolfiniun  25481  volfiniun  25527  i1f0  25667  fta1glem2  26147  fta1blem  26149  fta1lem  26287  vieta1lem2  26291  vieta1  26292  aalioulem2  26313  tayl0  26341  radcnv0  26397  wilthlem2  27049  fsumvma  27193  dchrfi  27235  cusgrfilem3  29544  eupth2eucrct  30305  trlsegvdeglem7  30314  fusgreghash2wspv  30423  ex-hash  30541  fsupprnfi  32783  ffsrn  32819  fsumiunle  32920  elrgspnlem2  33322  elrgspnlem3  33323  fply1  33636  mplmulmvr  33701  psrmonmul  33712  mplmonprod  33716  vieta  33742  constrfin  33909  locfinref  34004  esumcst  34226  esumsnf  34227  hasheuni  34248  rossros  34343  sibf0  34497  eulerpartlems  34523  eulerpartlemb  34531  ccatmulgnn0dir  34705  ofcccat  34706  plymulx0  34710  prodfzo03  34766  breprexp  34796  hgt750lemb  34819  hgt750leme  34821  lpadlem2  34843  fineqvnttrclselem1  35284  derangsn  35371  onsucsuccmpi  36644  topdifinffinlem  37680  pibt2  37750  finixpnum  37943  lindsenlbs  37953  poimirlem26  37984  poimirlem27  37985  poimirlem31  37989  poimirlem32  37990  prdsbnd  38131  heiborlem3  38151  heiborlem8  38156  ismrer1  38176  reheibor  38177  pclfinN  40363  frlmvscadiccat  42968  frlmsnic  43002  selvvvval  43035  elrfi  43143  mzpcompact2lem  43200  dfac11  43511  pwslnmlem0  43540  lpirlnr  43566  mpct  45651  cnrefiisplem  46278  dvmptfprodlem  46393  dvnprodlem2  46396  stoweidlem44  46493  fourierdlem51  46606  fourierdlem80  46635  fouriersw  46680  salexct  46783  salexct3  46791  salgencntex  46792  salgensscntex  46793  sge0sn  46828  sge0tsms  46829  sge0cl  46830  sge0sup  46840  sge0iunmptlemfi  46862  sge0splitsn  46890  hoiprodp1  47037  sge0hsphoire  47038  hoidmv1le  47043  hoidmvlelem1  47044  hoidmvlelem2  47045  hoidmvlelem5  47048  hspmbllem2  47076  ovnovollem3  47107  vonvolmbl  47110  vonvol  47111  vonvol2  47113  fsummmodsnunz  47846  edgusgrclnbfin  48333  suppmptcfin  48867  lcosn0  48911  lincext2  48946  snlindsntor  48962