Theorem snfi 8965

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 8555	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 8944	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5093	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3572	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 587	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 8898	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 234	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4667	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 8964	. . . 4 ⊢ ∅ ∈ Fin
10		eleq1 2819	. . . 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 2111  ∃wrex 3056  Vcvv 3436  ∅c0 4280  {csn 4573   class class class wbr 5089  ωcom 7796  1_oc1o 8378   ≈ cen 8866  Fincfn 8869

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

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 2535  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-om 7797  df-1o 8385  df-en 8870  df-fin 8873

This theorem is referenced by:  fiprc  8966  ssfi  9082  cnvfi  9085  fnfi  9087  sucdom2  9112  fodomfi  9196  imafiOLD  9200  pwfi  9203  prfi  9208  prfiALT  9209  tpfi  9210  fodomfir  9212  unifpw  9239  snopfsupp  9275  sniffsupp  9284  ssfii  9303  cantnfp1lem1  9568  infpwfidom  9919  ficardadju  10091  ackbij1lem4  10113  ackbij1lem9  10118  ackbij1lem10  10119  fin23lem21  10230  isfin1-3  10277  axcclem  10348  zornn0g  10396  hashsng  14276  hashen1  14277  hashunsng  14299  hashunsngx  14300  hashprg  14302  hashsnlei  14325  hashxplem  14340  hashmap  14342  hashfun  14344  hashbclem  14359  hashf1lem2  14363  hashf1  14364  hash7g  14393  hash3tpexb  14401  s7f1o  14873  fsumsplitsn  15651  fsummsnunz  15661  fsumsplitsnun  15662  fsum2dlem  15677  fsumcom2  15681  ackbijnn  15735  incexclem  15743  isumltss  15755  fprod2dlem  15887  fprodcom2  15891  fprodsplitsn  15896  rexpen  16137  2ebits  16358  lcmfunsnlem2lem1  16549  lcmfunsnlem2lem2  16550  lcmfunsnlem2  16551  lcmfass  16557  phicl2  16679  ramub1lem1  16938  cshwshashnsame  17015  acsfn1  17567  acsfiindd  18459  efmnd1hash  18800  symg1hash  19302  odcau  19516  sylow2alem2  19530  gsumsnfd  19863  gsumzunsnd  19868  gsumunsnfd  19869  gsumpt  19874  ablfac1eu  19987  pgpfaclem2  19996  ablfaclem3  20001  srgbinomlem4  20147  acsfn1p  20714  uvcff  21728  psrlidm  21899  psrridm  21900  mvrcl  21929  mplsubrg  21942  mplmon  21970  mplmonmul  21971  psrbagsn  21998  psr1baslem  22097  mat1dimelbas  22386  mat1dim0  22388  mat1dimid  22389  mat1dimmul  22391  mat1dimcrng  22392  mat1f1o  22393  mat1ghm  22398  mat1mhm  22399  mat1rhm  22400  mat1scmat  22454  mvmumamul1  22469  mdetrsca  22518  mdetunilem9  22535  mdetmul  22538  pmatcoe1fsupp  22616  d1mat2pmat  22654  pmatcollpw3fi1lem1  22701  chpmat1dlem  22750  chpmat1d  22751  0cmp  23309  discmp  23313  bwth  23325  disllycmp  23413  dis1stc  23414  locfincmp  23441  dissnlocfin  23444  comppfsc  23447  1stckgenlem  23468  ptpjpre2  23495  ptopn2  23499  xkohaus  23568  xkoptsub  23569  ptcmpfi  23728  cfinufil  23843  ufinffr  23844  fin1aufil  23847  alexsubALTlem3  23964  ptcmplem5  23971  tmdgsum  24010  tsmsxplem1  24068  tsmsxplem2  24069  prdsmet  24285  imasdsf1olem  24288  prdsbl  24406  icccmplem1  24738  icccmplem2  24739  ovolsn  25423  ovolfiniun  25429  volfiniun  25475  i1f0  25615  fta1glem2  26101  fta1blem  26103  fta1lem  26242  vieta1lem2  26246  vieta1  26247  aalioulem2  26268  tayl0  26296  radcnv0  26352  wilthlem2  27006  fsumvma  27151  dchrfi  27193  cusgrfilem3  29436  eupth2eucrct  30197  trlsegvdeglem7  30206  fusgreghash2wspv  30315  ex-hash  30433  fsupprnfi  32673  ffsrn  32711  fsumiunle  32812  elrgspnlem2  33210  elrgspnlem3  33211  fply1  33521  constrfin  33759  locfinref  33854  esumcst  34076  esumsnf  34077  hasheuni  34098  rossros  34193  sibf0  34347  eulerpartlems  34373  eulerpartlemb  34381  ccatmulgnn0dir  34555  ofcccat  34556  plymulx0  34560  prodfzo03  34616  breprexp  34646  hgt750lemb  34669  hgt750leme  34671  lpadlem2  34693  fineqvnttrclselem1  35141  derangsn  35214  onsucsuccmpi  36487  topdifinffinlem  37391  pibt2  37461  finixpnum  37655  lindsenlbs  37665  poimirlem26  37696  poimirlem27  37697  poimirlem31  37701  poimirlem32  37702  prdsbnd  37843  heiborlem3  37863  heiborlem8  37868  ismrer1  37888  reheibor  37889  pclfinN  40009  frlmvscadiccat  42609  frlmsnic  42643  selvvvval  42688  elrfi  42797  mzpcompact2lem  42854  dfac11  43165  pwslnmlem0  43194  lpirlnr  43220  mpct  45308  cnrefiisplem  45937  dvmptfprodlem  46052  dvnprodlem2  46055  stoweidlem44  46152  fourierdlem51  46265  fourierdlem80  46294  fouriersw  46339  salexct  46442  salexct3  46450  salgencntex  46451  salgensscntex  46452  sge0sn  46487  sge0tsms  46488  sge0cl  46489  sge0sup  46499  sge0iunmptlemfi  46521  sge0splitsn  46549  hoiprodp1  46696  sge0hsphoire  46697  hoidmv1le  46702  hoidmvlelem1  46703  hoidmvlelem2  46704  hoidmvlelem5  46707  hspmbllem2  46735  ovnovollem3  46766  vonvolmbl  46769  vonvol  46770  vonvol2  46772  fsummmodsnunz  47485  edgusgrclnbfin  47952  suppmptcfin  48486  lcosn0  48531  lincext2  48566  snlindsntor  48582