Theorem snfi 8978

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 8566	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 8957	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5100	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3574	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 587	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 8910	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 234	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4672	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 8977	. . . 4 ⊢ ∅ ∈ Fin
10		eleq1 2822	. . . 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 3058  Vcvv 3438  ∅c0 4283  {csn 4578   class class class wbr 5096  ωcom 7806  1_oc1o 8388   ≈ cen 8878  Fincfn 8881

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 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

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 2537  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-om 7807  df-1o 8395  df-en 8882  df-fin 8885

This theorem is referenced by:  fiprc  8979  ssfi  9095  cnvfi  9098  fnfi  9100  sucdom2  9125  fodomfi  9210  imafiOLD  9214  pwfi  9217  prfi  9222  prfiALT  9223  tpfi  9224  fodomfir  9226  unifpw  9253  snopfsupp  9292  sniffsupp  9301  ssfii  9320  cantnfp1lem1  9585  infpwfidom  9936  ficardadju  10108  ackbij1lem4  10130  ackbij1lem9  10135  ackbij1lem10  10136  fin23lem21  10247  isfin1-3  10294  axcclem  10365  zornn0g  10413  hashsng  14290  hashen1  14291  hashunsng  14313  hashunsngx  14314  hashprg  14316  hashsnlei  14339  hashxplem  14354  hashmap  14356  hashfun  14358  hashbclem  14373  hashf1lem2  14377  hashf1  14378  hash7g  14407  hash3tpexb  14415  s7f1o  14887  fsumsplitsn  15665  fsummsnunz  15675  fsumsplitsnun  15676  fsum2dlem  15691  fsumcom2  15695  ackbijnn  15749  incexclem  15757  isumltss  15769  fprod2dlem  15901  fprodcom2  15905  fprodsplitsn  15910  rexpen  16151  2ebits  16372  lcmfunsnlem2lem1  16563  lcmfunsnlem2lem2  16564  lcmfunsnlem2  16565  lcmfass  16571  phicl2  16693  ramub1lem1  16952  cshwshashnsame  17029  acsfn1  17582  acsfiindd  18474  efmnd1hash  18815  symg1hash  19317  odcau  19531  sylow2alem2  19545  gsumsnfd  19878  gsumzunsnd  19883  gsumunsnfd  19884  gsumpt  19889  ablfac1eu  20002  pgpfaclem2  20011  ablfaclem3  20016  srgbinomlem4  20162  acsfn1p  20730  uvcff  21744  psrlidm  21915  psrridm  21916  mvrcl  21945  mplsubrg  21958  mplmon  21988  mplmonmul  21989  psrbagsn  22016  psr1baslem  22123  mat1dimelbas  22413  mat1dim0  22415  mat1dimid  22416  mat1dimmul  22418  mat1dimcrng  22419  mat1f1o  22420  mat1ghm  22425  mat1mhm  22426  mat1rhm  22427  mat1scmat  22481  mvmumamul1  22496  mdetrsca  22545  mdetunilem9  22562  mdetmul  22565  pmatcoe1fsupp  22643  d1mat2pmat  22681  pmatcollpw3fi1lem1  22728  chpmat1dlem  22777  chpmat1d  22778  0cmp  23336  discmp  23340  bwth  23352  disllycmp  23440  dis1stc  23441  locfincmp  23468  dissnlocfin  23471  comppfsc  23474  1stckgenlem  23495  ptpjpre2  23522  ptopn2  23526  xkohaus  23595  xkoptsub  23596  ptcmpfi  23755  cfinufil  23870  ufinffr  23871  fin1aufil  23874  alexsubALTlem3  23991  ptcmplem5  23998  tmdgsum  24037  tsmsxplem1  24095  tsmsxplem2  24096  prdsmet  24312  imasdsf1olem  24315  prdsbl  24433  icccmplem1  24765  icccmplem2  24766  ovolsn  25450  ovolfiniun  25456  volfiniun  25502  i1f0  25642  fta1glem2  26128  fta1blem  26130  fta1lem  26269  vieta1lem2  26273  vieta1  26274  aalioulem2  26295  tayl0  26323  radcnv0  26379  wilthlem2  27033  fsumvma  27178  dchrfi  27220  cusgrfilem3  29480  eupth2eucrct  30241  trlsegvdeglem7  30250  fusgreghash2wspv  30359  ex-hash  30477  fsupprnfi  32720  ffsrn  32756  fsumiunle  32859  elrgspnlem2  33274  elrgspnlem3  33275  fply1  33588  mplmulmvr  33653  vieta  33685  constrfin  33852  locfinref  33947  esumcst  34169  esumsnf  34170  hasheuni  34191  rossros  34286  sibf0  34440  eulerpartlems  34466  eulerpartlemb  34474  ccatmulgnn0dir  34648  ofcccat  34649  plymulx0  34653  prodfzo03  34709  breprexp  34739  hgt750lemb  34762  hgt750leme  34764  lpadlem2  34786  fineqvnttrclselem1  35226  derangsn  35313  onsucsuccmpi  36586  topdifinffinlem  37491  pibt2  37561  finixpnum  37745  lindsenlbs  37755  poimirlem26  37786  poimirlem27  37787  poimirlem31  37791  poimirlem32  37792  prdsbnd  37933  heiborlem3  37953  heiborlem8  37958  ismrer1  37978  reheibor  37979  pclfinN  40099  frlmvscadiccat  42703  frlmsnic  42737  selvvvval  42770  elrfi  42878  mzpcompact2lem  42935  dfac11  43246  pwslnmlem0  43275  lpirlnr  43301  mpct  45387  cnrefiisplem  46015  dvmptfprodlem  46130  dvnprodlem2  46133  stoweidlem44  46230  fourierdlem51  46343  fourierdlem80  46372  fouriersw  46417  salexct  46520  salexct3  46528  salgencntex  46529  salgensscntex  46530  sge0sn  46565  sge0tsms  46566  sge0cl  46567  sge0sup  46577  sge0iunmptlemfi  46599  sge0splitsn  46627  hoiprodp1  46774  sge0hsphoire  46775  hoidmv1le  46780  hoidmvlelem1  46781  hoidmvlelem2  46782  hoidmvlelem5  46785  hspmbllem2  46813  ovnovollem3  46844  vonvolmbl  46847  vonvol  46848  vonvol2  46850  fsummmodsnunz  47563  edgusgrclnbfin  48030  suppmptcfin  48564  lcosn0  48608  lincext2  48643  snlindsntor  48659