Theorem snfi 9079

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 8657	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 9057	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5106	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3576	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 599	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 9010	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 237	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4674	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 9078	. . . 4 ⊢ ∅ ∈ Fin
10		eleq1 2848	. . . 4 ⊢ ({𝐴} = ∅ → ({𝐴} ∈ Fin ↔ ∅ ∈ Fin))
11	9, 10	mpbiri 261	. . 3 ⊢ ({𝐴} = ∅ → {𝐴} ∈ Fin)
12	8, 11	sylbi 220	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴} ∈ Fin)
13	7, 12	pm2.61i 184	1 ⊢ {𝐴} ∈ Fin

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1569   ∈ wcel 2144  ∃wrex 3086  Vcvv 3450  ∅c0 4277  {csn 4584   class class class wbr 5102  ωcom 7881  1_oc1o 8477   ≈ cen 8978  Fincfn 8981

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-mo 2564  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-om 7882  df-1o 8484  df-en 8982  df-fin 8985

This theorem is used by:  fiprc  9080  ssfi  9196  cnvfi  9199  fnfi  9201  sucdom2  9226  fodomfi  9312  pwfi  9318  prfi  9323  prfiALT  9324  tpfi  9325  fodomfir  9327  unifpw  9352  snopfsupp  9390  sniffsupp  9399  ssfii  9418  cantnfp1lem1  9686  hfsn  9927  infpwfidom  10114  ficardadju  10285  ackbij1lem4  10307  ackbij1lem9  10312  ackbij1lem10  10313  fin23lem21  10424  isfin1-3  10471  axcclem  10542  zornn0g  10590  hashsng  14520  hashen1  14521  hashunsng  14543  hashunsngx  14544  hashprg  14546  hashsnlei  14570  hashxplem  14585  hashmap  14587  hashfun  14589  hashbclem  14604  hashf1lem2  14608  hashf1  14609  hash7g  14638  hash3tpexb  14646  s7f1o  15128  fsumsplitsn  15919  fsummsnunz  15929  fsumsplitsnun  15930  fsum2dlem  15945  fsumcom2  15949  ackbijnn  16006  incexclem  16014  isumltss  16026  fprod2dlem  16156  fprodcom2  16160  fprodsplitsn  16165  rexpen  16405  2ebits  16626  lcmfunsnlem2lem1  16822  lcmfunsnlem2lem2  16823  lcmfunsnlem2  16824  lcmfass  16830  phicl2  16954  ramub1lem1  17213  cshwshashnsame  17290  acsfn1  17844  acsfiindd  18736  efmnd1hash  19097  symg1hash  19613  odcau  19827  sylow2alem2  19841  gsumsnfd  20174  gsumzunsnd  20179  gsumunsnfd  20180  gsumpt  20185  ablfac1eu  20298  pgpfaclem2  20307  ablfaclem3  20312  srgbinomlem4  20464  acsfn1p  21065  uvcff  22106  lindsenlbs  22166  psrlidm  22278  psrridm  22279  mvrcl  22308  mplsubrg  22321  mplmon  22353  mplmonmul  22354  psrbagsn  22381  selvvvval  22460  psr1baslem  22512  mat1dimelbas  22795  mat1dim0  22797  mat1dimid  22798  mat1dimmul  22800  mat1dimcrng  22801  mat1f1o  22802  mat1ghm  22807  mat1mhm  22808  mat1rhm  22809  mat1scmat  22863  mvmumamul1  22878  mdetrsca  22927  mdetunilem9  22944  mdetmul  22947  pmatcoe1fsupp  23028  d1mat2pmat  23066  pmatcollpw3fi1lem1  23113  chpmat1dlem  23162  chpmat1d  23163  0cmp  23721  discmp  23725  bwth  23737  disllycmp  23826  dis1stc  23827  locfincmp  23854  dissnlocfin  23857  comppfsc  23860  1stckgenlem  23881  ptpjpre2  23908  ptopn2  23912  xkohaus  23981  xkoptsub  23982  ptcmpfi  24141  cfinufil  24256  ufinffr  24257  fin1aufil  24260  alexsubALTlem3  24377  ptcmplem5  24384  tmdgsum  24423  tsmsxplem1  24481  tsmsxplem2  24482  prdsmet  24698  imasdsf1olem  24701  prdsbl  24819  icccmplem1  25151  icccmplem2  25152  ovolsn  25825  ovolfiniun  25831  volfiniun  25877  i1f0  26017  fta1glem2  26496  fta1blem  26498  plyn0mulidp  26611  fta1lem  26637  vieta1lem2  26643  vieta1  26644  aalioulem2  26669  tayl0  26698  radcnv0  26752  wilthlem2  27405  fsumvma  27549  dchrfi  27591  cusgrfilem3  30047  eupth2eucrct  30827  trlsegvdeglem7  30836  fusgreghash2wspv  30945  ex-hash  31063  fsupprnfi  33336  ffsrn  33370  fsumiunle  33470  elrgspnlem2  33854  elrgspnlem3  33855  fply1  34140  selvply1rhmlema  34200  selvply1rhmlemb  34201  mplidomlem  34209  mplmulmvr  34221  psrmonmul  34232  mplmonprod  34236  vieta  34262  constrfin  34428  locfinref  34523  esumcst  34745  esumsnf  34746  hasheuni  34767  rossros  34863  sibf0  35016  eulerpartlems  35042  eulerpartlemb  35050  ccatmulgnn0dir  35224  ofcccat  35225  prodfzo03  35282  breprexp  35312  hgt750lemb  35335  hgt750leme  35337  lpadlem2  35362  fineqvnttrclselem1  35857  derangsn  36053  onsucsuccmpi  37355  topdifinffinlem  38407  pibt2  38477  finixpnum  38665  poimirlem26  38701  poimirlem27  38702  poimirlem31  38706  poimirlem32  38707  prdsbnd  38864  heiborlem3  38884  heiborlem8  38889  ismrer1  38909  reheibor  38910  pclfinN  41094  frlmvscadiccat  43710  frlmsnic  43741  elrfi  43842  mzpcompact2lem  43899  dfac11  44201  pwslnmlem0  44230  lpirlnr  44256  mpct  46351  cnrefiisplem  46975  dvmptfprodlem  47090  dvnprodlem2  47093  stoweidlem44  47190  fourierdlem51  47303  fourierdlem80  47332  fouriersw  47377  salexct  47480  salexct3  47488  salgencntex  47489  salgensscntex  47490  sge0sn  47525  sge0tsms  47526  sge0cl  47527  sge0sup  47537  sge0iunmptlemfi  47559  sge0splitsn  47587  hoiprodp1  47734  sge0hsphoire  47735  hoidmv1le  47740  hoidmvlelem1  47741  hoidmvlelem2  47742  hoidmvlelem5  47745  hspmbllem2  47773  ovnovollem3  47804  vonvolmbl  47807  vonvol  47808  vonvol2  47810  tmachlem-agreeprod  48083  tmachlem-agreefin  48094  fsummmodsnunz  48589  edgusgrclnbfin  49076  suppmptcfin  49624  lcosn0  49668  lincext2  49703  snlindsntor  49719