Theorem snfi 8990

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 8576	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 8969	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5089	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3564	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 588	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 8922	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 234	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4661	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 8989	. . . 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 1542   ∈ wcel 2114  ∃wrex 3061  Vcvv 3429  ∅c0 4273  {csn 4567   class class class wbr 5085  ωcom 7817  1_oc1o 8398   ≈ cen 8890  Fincfn 8893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2539  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-om 7818  df-1o 8405  df-en 8894  df-fin 8897

This theorem is referenced by:  fiprc  8991  ssfi  9107  cnvfi  9110  fnfi  9112  sucdom2  9137  fodomfi  9222  imafiOLD  9226  pwfi  9229  prfi  9234  prfiALT  9235  tpfi  9236  fodomfir  9238  unifpw  9265  snopfsupp  9304  sniffsupp  9313  ssfii  9332  cantnfp1lem1  9599  infpwfidom  9950  ficardadju  10122  ackbij1lem4  10144  ackbij1lem9  10149  ackbij1lem10  10150  fin23lem21  10261  isfin1-3  10308  axcclem  10379  zornn0g  10427  hashsng  14331  hashen1  14332  hashunsng  14354  hashunsngx  14355  hashprg  14357  hashsnlei  14380  hashxplem  14395  hashmap  14397  hashfun  14399  hashbclem  14414  hashf1lem2  14418  hashf1  14419  hash7g  14448  hash3tpexb  14456  s7f1o  14928  fsumsplitsn  15706  fsummsnunz  15716  fsumsplitsnun  15717  fsum2dlem  15732  fsumcom2  15736  ackbijnn  15793  incexclem  15801  isumltss  15813  fprod2dlem  15945  fprodcom2  15949  fprodsplitsn  15954  rexpen  16195  2ebits  16416  lcmfunsnlem2lem1  16607  lcmfunsnlem2lem2  16608  lcmfunsnlem2  16609  lcmfass  16615  phicl2  16738  ramub1lem1  16997  cshwshashnsame  17074  acsfn1  17627  acsfiindd  18519  efmnd1hash  18860  symg1hash  19365  odcau  19579  sylow2alem2  19593  gsumsnfd  19926  gsumzunsnd  19931  gsumunsnfd  19932  gsumpt  19937  ablfac1eu  20050  pgpfaclem2  20059  ablfaclem3  20064  srgbinomlem4  20210  acsfn1p  20776  uvcff  21771  psrlidm  21940  psrridm  21941  mvrcl  21970  mplsubrg  21983  mplmon  22013  mplmonmul  22014  psrbagsn  22041  psr1baslem  22148  mat1dimelbas  22436  mat1dim0  22438  mat1dimid  22439  mat1dimmul  22441  mat1dimcrng  22442  mat1f1o  22443  mat1ghm  22448  mat1mhm  22449  mat1rhm  22450  mat1scmat  22504  mvmumamul1  22519  mdetrsca  22568  mdetunilem9  22585  mdetmul  22588  pmatcoe1fsupp  22666  d1mat2pmat  22704  pmatcollpw3fi1lem1  22751  chpmat1dlem  22800  chpmat1d  22801  0cmp  23359  discmp  23363  bwth  23375  disllycmp  23463  dis1stc  23464  locfincmp  23491  dissnlocfin  23494  comppfsc  23497  1stckgenlem  23518  ptpjpre2  23545  ptopn2  23549  xkohaus  23618  xkoptsub  23619  ptcmpfi  23778  cfinufil  23893  ufinffr  23894  fin1aufil  23897  alexsubALTlem3  24014  ptcmplem5  24021  tmdgsum  24060  tsmsxplem1  24118  tsmsxplem2  24119  prdsmet  24335  imasdsf1olem  24338  prdsbl  24456  icccmplem1  24788  icccmplem2  24789  ovolsn  25462  ovolfiniun  25468  volfiniun  25514  i1f0  25654  fta1glem2  26134  fta1blem  26136  fta1lem  26273  vieta1lem2  26277  vieta1  26278  aalioulem2  26299  tayl0  26327  radcnv0  26381  wilthlem2  27032  fsumvma  27176  dchrfi  27218  cusgrfilem3  29526  eupth2eucrct  30287  trlsegvdeglem7  30296  fusgreghash2wspv  30405  ex-hash  30523  fsupprnfi  32765  ffsrn  32801  fsumiunle  32902  elrgspnlem2  33304  elrgspnlem3  33305  fply1  33618  mplmulmvr  33683  psrmonmul  33694  mplmonprod  33698  vieta  33724  constrfin  33890  locfinref  33985  esumcst  34207  esumsnf  34208  hasheuni  34229  rossros  34324  sibf0  34478  eulerpartlems  34504  eulerpartlemb  34512  ccatmulgnn0dir  34686  ofcccat  34687  plymulx0  34691  prodfzo03  34747  breprexp  34777  hgt750lemb  34800  hgt750leme  34802  lpadlem2  34824  fineqvnttrclselem1  35265  derangsn  35352  onsucsuccmpi  36625  topdifinffinlem  37663  pibt2  37733  finixpnum  37926  lindsenlbs  37936  poimirlem26  37967  poimirlem27  37968  poimirlem31  37972  poimirlem32  37973  prdsbnd  38114  heiborlem3  38134  heiborlem8  38139  ismrer1  38159  reheibor  38160  pclfinN  40346  frlmvscadiccat  42951  frlmsnic  42985  selvvvval  43018  elrfi  43126  mzpcompact2lem  43183  dfac11  43490  pwslnmlem0  43519  lpirlnr  43545  mpct  45630  cnrefiisplem  46257  dvmptfprodlem  46372  dvnprodlem2  46375  stoweidlem44  46472  fourierdlem51  46585  fourierdlem80  46614  fouriersw  46659  salexct  46762  salexct3  46770  salgencntex  46771  salgensscntex  46772  sge0sn  46807  sge0tsms  46808  sge0cl  46809  sge0sup  46819  sge0iunmptlemfi  46841  sge0splitsn  46869  hoiprodp1  47016  sge0hsphoire  47017  hoidmv1le  47022  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem5  47027  hspmbllem2  47055  ovnovollem3  47086  vonvolmbl  47089  vonvol  47090  vonvol2  47092  fsummmodsnunz  47831  edgusgrclnbfin  48318  suppmptcfin  48852  lcosn0  48896  lincext2  48931  snlindsntor  48947