Theorem snfi 9024

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 8610	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 9003	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5104	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3581	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 596	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 8956	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 236	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4676	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 9023	. . . 4 ⊢ ∅ ∈ Fin
10		eleq1 2850	. . . 4 ⊢ ({𝐴} = ∅ → ({𝐴} ∈ Fin ↔ ∅ ∈ Fin))
11	9, 10	mpbiri 260	. . 3 ⊢ ({𝐴} = ∅ → {𝐴} ∈ Fin)
12	8, 11	sylbi 219	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴} ∈ Fin)
13	7, 12	pm2.61i 183	1 ⊢ {𝐴} ∈ Fin

Syntax hints:  ¬ wn 3   = wceq 1560   ∈ wcel 2142  ∃wrex 3086  Vcvv 3454  ∅c0 4285  {csn 4582   class class class wbr 5100  ωcom 7846  1_oc1o 8430   ≈ cen 8924  Fincfn 8927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-mo 2566  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-om 7847  df-1o 8437  df-en 8928  df-fin 8931

This theorem is referenced by:  fiprc  9025  ssfi  9141  cnvfi  9144  fnfi  9146  sucdom2  9171  fodomfi  9256  imafiOLD  9260  pwfi  9263  prfi  9268  prfiALT  9269  tpfi  9270  fodomfir  9272  unifpw  9298  snopfsupp  9337  sniffsupp  9346  ssfii  9365  cantnfp1lem1  9633  infpwfidom  9984  ficardadju  10156  ackbij1lem4  10178  ackbij1lem9  10183  ackbij1lem10  10184  fin23lem21  10296  isfin1-3  10343  axcclem  10414  zornn0g  10462  hashsng  14382  hashen1  14383  hashunsng  14405  hashunsngx  14406  hashprg  14408  hashsnlei  14431  hashxplem  14446  hashmap  14448  hashfun  14450  hashbclem  14465  hashf1lem2  14469  hashf1  14470  hash7g  14499  hash3tpexb  14507  s7f1o  14979  fsumsplitsn  15771  fsummsnunz  15781  fsumsplitsnun  15782  fsum2dlem  15797  fsumcom2  15801  ackbijnn  15858  incexclem  15866  isumltss  15878  fprod2dlem  16010  fprodcom2  16014  fprodsplitsn  16019  rexpen  16260  2ebits  16481  lcmfunsnlem2lem1  16672  lcmfunsnlem2lem2  16673  lcmfunsnlem2  16674  lcmfass  16680  phicl2  16803  ramub1lem1  17062  cshwshashnsame  17139  acsfn1  17693  acsfiindd  18585  efmnd1hash  18926  symg1hash  19430  odcau  19644  sylow2alem2  19658  gsumsnfd  19991  gsumzunsnd  19996  gsumunsnfd  19997  gsumpt  20002  ablfac1eu  20115  pgpfaclem2  20124  ablfaclem3  20129  srgbinomlem4  20279  acsfn1p  20848  uvcff  21843  psrlidm  22013  psrridm  22014  mvrcl  22043  mplsubrg  22056  mplmon  22088  mplmonmul  22089  psrbagsn  22116  selvvvval  22195  psr1baslem  22247  mat1dimelbas  22531  mat1dim0  22533  mat1dimid  22534  mat1dimmul  22536  mat1dimcrng  22537  mat1f1o  22538  mat1ghm  22543  mat1mhm  22544  mat1rhm  22545  mat1scmat  22599  mvmumamul1  22614  mdetrsca  22663  mdetunilem9  22680  mdetmul  22683  pmatcoe1fsupp  22761  d1mat2pmat  22799  pmatcollpw3fi1lem1  22846  chpmat1dlem  22895  chpmat1d  22896  0cmp  23454  discmp  23458  bwth  23470  disllycmp  23558  dis1stc  23559  locfincmp  23586  dissnlocfin  23589  comppfsc  23592  1stckgenlem  23613  ptpjpre2  23640  ptopn2  23644  xkohaus  23713  xkoptsub  23714  ptcmpfi  23873  cfinufil  23988  ufinffr  23989  fin1aufil  23992  alexsubALTlem3  24109  ptcmplem5  24116  tmdgsum  24155  tsmsxplem1  24213  tsmsxplem2  24214  prdsmet  24430  imasdsf1olem  24433  prdsbl  24551  icccmplem1  24883  icccmplem2  24884  ovolsn  25557  ovolfiniun  25563  volfiniun  25609  i1f0  25749  fta1glem2  26229  fta1blem  26231  plyn0mulidp  26345  fta1lem  26371  vieta1lem2  26375  vieta1  26376  aalioulem2  26397  tayl0  26425  radcnv0  26479  wilthlem2  27133  fsumvma  27277  dchrfi  27319  cusgrfilem3  29658  eupth2eucrct  30419  trlsegvdeglem7  30428  fusgreghash2wspv  30537  ex-hash  30655  fsupprnfi  32894  ffsrn  32930  fsumiunle  33031  elrgspnlem2  33424  elrgspnlem3  33425  fply1  33754  selvply1rhmlema  33815  selvply1rhmlemb  33816  mplidomlem  33824  mplmulmvr  33836  psrmonmul  33847  mplmonprod  33851  vieta  33877  constrfin  34043  locfinref  34138  esumcst  34360  esumsnf  34361  hasheuni  34382  rossros  34477  sibf0  34631  eulerpartlems  34657  eulerpartlemb  34665  ccatmulgnn0dir  34839  ofcccat  34840  prodfzo03  34897  breprexp  34927  hgt750lemb  34950  hgt750leme  34952  lpadlem2  34977  fineqvnttrclselem1  35417  derangsn  35520  onsucsuccmpi  36803  topdifinffinlem  37841  pibt2  37911  finixpnum  38104  lindsenlbs  38114  poimirlem26  38145  poimirlem27  38146  poimirlem31  38150  poimirlem32  38151  prdsbnd  38292  heiborlem3  38312  heiborlem8  38317  ismrer1  38337  reheibor  38338  pclfinN  40524  frlmvscadiccat  43128  frlmsnic  43158  elrfi  43275  mzpcompact2lem  43332  dfac11  43639  pwslnmlem0  43668  lpirlnr  43694  mpct  45778  cnrefiisplem  46403  dvmptfprodlem  46518  dvnprodlem2  46521  stoweidlem44  46618  fourierdlem51  46731  fourierdlem80  46760  fouriersw  46805  salexct  46908  salexct3  46916  salgencntex  46917  salgensscntex  46918  sge0sn  46953  sge0tsms  46954  sge0cl  46955  sge0sup  46965  sge0iunmptlemfi  46987  sge0splitsn  47015  hoiprodp1  47162  sge0hsphoire  47163  hoidmv1le  47168  hoidmvlelem1  47169  hoidmvlelem2  47170  hoidmvlelem5  47173  hspmbllem2  47201  ovnovollem3  47232  vonvolmbl  47235  vonvol  47236  vonvol2  47238  fsummmodsnunz  47977  edgusgrclnbfin  48464  suppmptcfin  48998  lcosn0  49042  lincext2  49077  snlindsntor  49093