Theorem snfi 8980

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 8568	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 8959	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5102	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3576	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 587	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 8912	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 234	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4674	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 8979	. . . 4 ⊢ ∅ ∈ Fin
10		eleq1 2824	. . . 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 1541   ∈ wcel 2113  ∃wrex 3060  Vcvv 3440  ∅c0 4285  {csn 4580   class class class wbr 5098  ωcom 7808  1_oc1o 8390   ≈ cen 8880  Fincfn 8883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-mo 2539  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-om 7809  df-1o 8397  df-en 8884  df-fin 8887

This theorem is referenced by:  fiprc  8981  ssfi  9097  cnvfi  9100  fnfi  9102  sucdom2  9127  fodomfi  9212  imafiOLD  9216  pwfi  9219  prfi  9224  prfiALT  9225  tpfi  9226  fodomfir  9228  unifpw  9255  snopfsupp  9294  sniffsupp  9303  ssfii  9322  cantnfp1lem1  9587  infpwfidom  9938  ficardadju  10110  ackbij1lem4  10132  ackbij1lem9  10137  ackbij1lem10  10138  fin23lem21  10249  isfin1-3  10296  axcclem  10367  zornn0g  10415  hashsng  14292  hashen1  14293  hashunsng  14315  hashunsngx  14316  hashprg  14318  hashsnlei  14341  hashxplem  14356  hashmap  14358  hashfun  14360  hashbclem  14375  hashf1lem2  14379  hashf1  14380  hash7g  14409  hash3tpexb  14417  s7f1o  14889  fsumsplitsn  15667  fsummsnunz  15677  fsumsplitsnun  15678  fsum2dlem  15693  fsumcom2  15697  ackbijnn  15751  incexclem  15759  isumltss  15771  fprod2dlem  15903  fprodcom2  15907  fprodsplitsn  15912  rexpen  16153  2ebits  16374  lcmfunsnlem2lem1  16565  lcmfunsnlem2lem2  16566  lcmfunsnlem2  16567  lcmfass  16573  phicl2  16695  ramub1lem1  16954  cshwshashnsame  17031  acsfn1  17584  acsfiindd  18476  efmnd1hash  18817  symg1hash  19319  odcau  19533  sylow2alem2  19547  gsumsnfd  19880  gsumzunsnd  19885  gsumunsnfd  19886  gsumpt  19891  ablfac1eu  20004  pgpfaclem2  20013  ablfaclem3  20018  srgbinomlem4  20164  acsfn1p  20732  uvcff  21746  psrlidm  21917  psrridm  21918  mvrcl  21947  mplsubrg  21960  mplmon  21990  mplmonmul  21991  psrbagsn  22018  psr1baslem  22125  mat1dimelbas  22415  mat1dim0  22417  mat1dimid  22418  mat1dimmul  22420  mat1dimcrng  22421  mat1f1o  22422  mat1ghm  22427  mat1mhm  22428  mat1rhm  22429  mat1scmat  22483  mvmumamul1  22498  mdetrsca  22547  mdetunilem9  22564  mdetmul  22567  pmatcoe1fsupp  22645  d1mat2pmat  22683  pmatcollpw3fi1lem1  22730  chpmat1dlem  22779  chpmat1d  22780  0cmp  23338  discmp  23342  bwth  23354  disllycmp  23442  dis1stc  23443  locfincmp  23470  dissnlocfin  23473  comppfsc  23476  1stckgenlem  23497  ptpjpre2  23524  ptopn2  23528  xkohaus  23597  xkoptsub  23598  ptcmpfi  23757  cfinufil  23872  ufinffr  23873  fin1aufil  23876  alexsubALTlem3  23993  ptcmplem5  24000  tmdgsum  24039  tsmsxplem1  24097  tsmsxplem2  24098  prdsmet  24314  imasdsf1olem  24317  prdsbl  24435  icccmplem1  24767  icccmplem2  24768  ovolsn  25452  ovolfiniun  25458  volfiniun  25504  i1f0  25644  fta1glem2  26130  fta1blem  26132  fta1lem  26271  vieta1lem2  26275  vieta1  26276  aalioulem2  26297  tayl0  26325  radcnv0  26381  wilthlem2  27035  fsumvma  27180  dchrfi  27222  cusgrfilem3  29531  eupth2eucrct  30292  trlsegvdeglem7  30301  fusgreghash2wspv  30410  ex-hash  30528  fsupprnfi  32771  ffsrn  32807  fsumiunle  32910  elrgspnlem2  33325  elrgspnlem3  33326  fply1  33639  mplmulmvr  33704  vieta  33736  constrfin  33903  locfinref  33998  esumcst  34220  esumsnf  34221  hasheuni  34242  rossros  34337  sibf0  34491  eulerpartlems  34517  eulerpartlemb  34525  ccatmulgnn0dir  34699  ofcccat  34700  plymulx0  34704  prodfzo03  34760  breprexp  34790  hgt750lemb  34813  hgt750leme  34815  lpadlem2  34837  fineqvnttrclselem1  35277  derangsn  35364  onsucsuccmpi  36637  topdifinffinlem  37552  pibt2  37622  finixpnum  37806  lindsenlbs  37816  poimirlem26  37847  poimirlem27  37848  poimirlem31  37852  poimirlem32  37853  prdsbnd  37994  heiborlem3  38014  heiborlem8  38019  ismrer1  38039  reheibor  38040  pclfinN  40160  frlmvscadiccat  42761  frlmsnic  42795  selvvvval  42828  elrfi  42936  mzpcompact2lem  42993  dfac11  43304  pwslnmlem0  43333  lpirlnr  43359  mpct  45445  cnrefiisplem  46073  dvmptfprodlem  46188  dvnprodlem2  46191  stoweidlem44  46288  fourierdlem51  46401  fourierdlem80  46430  fouriersw  46475  salexct  46578  salexct3  46586  salgencntex  46587  salgensscntex  46588  sge0sn  46623  sge0tsms  46624  sge0cl  46625  sge0sup  46635  sge0iunmptlemfi  46657  sge0splitsn  46685  hoiprodp1  46832  sge0hsphoire  46833  hoidmv1le  46838  hoidmvlelem1  46839  hoidmvlelem2  46840  hoidmvlelem5  46843  hspmbllem2  46871  ovnovollem3  46902  vonvolmbl  46905  vonvol  46906  vonvol2  46908  fsummmodsnunz  47621  edgusgrclnbfin  48088  suppmptcfin  48622  lcosn0  48666  lincext2  48701  snlindsntor  48717