Theorem snfi 9081

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 8676	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 9060	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5151	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3621	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 587	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 9014	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 234	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4721	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 9080	. . . 4 ⊢ ∅ ∈ Fin
10		eleq1 2826	. . . 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 1536   ∈ wcel 2105  ∃wrex 3067  Vcvv 3477  ∅c0 4338  {csn 4630   class class class wbr 5147  ωcom 7886  1_oc1o 8497   ≈ cen 8980  Fincfn 8983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-mo 2537  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-om 7887  df-1o 8504  df-en 8984  df-fin 8987

This theorem is referenced by:  fiprc  9083  ssfi  9211  cnvfi  9214  fnfi  9215  sucdom2  9240  fodomfi  9347  imafiOLD  9351  pwfi  9354  prfi  9360  prfiALT  9361  tpfi  9362  fodomfir  9365  unifpw  9392  snopfsupp  9428  sniffsupp  9437  ssfii  9456  cantnfp1lem1  9715  infpwfidom  10065  ficardadju  10237  ackbij1lem4  10259  ackbij1lem9  10264  ackbij1lem10  10265  fin23lem21  10376  isfin1-3  10423  axcclem  10494  zornn0g  10542  hashsng  14404  hashen1  14405  hashunsng  14427  hashunsngx  14428  hashprg  14430  hashsnlei  14453  hashxplem  14468  hashmap  14470  hashfun  14472  hashbclem  14487  hashf1lem2  14491  hashf1  14492  hash7g  14521  hash3tpexb  14529  s7f1o  15001  fsumsplitsn  15776  fsummsnunz  15786  fsumsplitsnun  15787  fsum2dlem  15802  fsumcom2  15806  ackbijnn  15860  incexclem  15868  isumltss  15880  fprod2dlem  16012  fprodcom2  16016  fprodsplitsn  16021  rexpen  16260  2ebits  16480  lcmfunsnlem2lem1  16671  lcmfunsnlem2lem2  16672  lcmfunsnlem2  16673  lcmfass  16679  phicl2  16801  ramub1lem1  17059  cshwshashnsame  17137  acsfn1  17705  acsfiindd  18610  efmnd1hash  18917  symg1hash  19421  odcau  19636  sylow2alem2  19650  gsumsnfd  19983  gsumzunsnd  19988  gsumunsnfd  19989  gsumpt  19994  ablfac1eu  20107  pgpfaclem2  20116  ablfaclem3  20121  srgbinomlem4  20246  acsfn1p  20816  uvcff  21828  psrlidm  21999  psrridm  22000  mvrcl  22029  mplsubrg  22042  mplmon  22070  mplmonmul  22071  psrbagsn  22104  psr1baslem  22201  mat1dimelbas  22492  mat1dim0  22494  mat1dimid  22495  mat1dimmul  22497  mat1dimcrng  22498  mat1f1o  22499  mat1ghm  22504  mat1mhm  22505  mat1rhm  22506  mat1scmat  22560  mvmumamul1  22575  mdetrsca  22624  mdetunilem9  22641  mdetmul  22644  pmatcoe1fsupp  22722  d1mat2pmat  22760  pmatcollpw3fi1lem1  22807  chpmat1dlem  22856  chpmat1d  22857  0cmp  23417  discmp  23421  bwth  23433  disllycmp  23521  dis1stc  23522  locfincmp  23549  dissnlocfin  23552  comppfsc  23555  1stckgenlem  23576  ptpjpre2  23603  ptopn2  23607  xkohaus  23676  xkoptsub  23677  ptcmpfi  23836  cfinufil  23951  ufinffr  23952  fin1aufil  23955  alexsubALTlem3  24072  ptcmplem5  24079  tmdgsum  24118  tsmsxplem1  24176  tsmsxplem2  24177  prdsmet  24395  imasdsf1olem  24398  prdsbl  24519  icccmplem1  24857  icccmplem2  24858  ovolsn  25543  ovolfiniun  25549  volfiniun  25595  i1f0  25735  fta1glem2  26222  fta1blem  26224  fta1lem  26363  vieta1lem2  26367  vieta1  26368  aalioulem2  26389  tayl0  26417  radcnv0  26473  wilthlem2  27126  fsumvma  27271  dchrfi  27313  cusgrfilem3  29489  eupth2eucrct  30245  trlsegvdeglem7  30254  fusgreghash2wspv  30363  ex-hash  30481  fsupprnfi  32706  ffsrn  32746  fsumiunle  32835  elrgspnlem2  33232  elrgspnlem3  33233  fply1  33563  constrfin  33750  locfinref  33801  esumcst  34043  esumsnf  34044  hasheuni  34065  rossros  34160  sibf0  34315  eulerpartlems  34341  eulerpartlemb  34349  ccatmulgnn0dir  34535  ofcccat  34536  plymulx0  34540  prodfzo03  34596  breprexp  34626  hgt750lemb  34649  hgt750leme  34651  lpadlem2  34673  derangsn  35154  onsucsuccmpi  36425  topdifinffinlem  37329  pibt2  37399  finixpnum  37591  lindsenlbs  37601  poimirlem26  37632  poimirlem27  37633  poimirlem31  37637  poimirlem32  37638  prdsbnd  37779  heiborlem3  37799  heiborlem8  37804  ismrer1  37824  reheibor  37825  pclfinN  39882  frlmvscadiccat  42492  frlmsnic  42526  selvvvval  42571  elrfi  42681  mzpcompact2lem  42738  dfac11  43050  pwslnmlem0  43079  lpirlnr  43105  mpct  45143  cnrefiisplem  45784  dvmptfprodlem  45899  dvnprodlem2  45902  stoweidlem44  45999  fourierdlem51  46112  fourierdlem80  46141  fouriersw  46186  salexct  46289  salexct3  46297  salgencntex  46298  salgensscntex  46299  sge0sn  46334  sge0tsms  46335  sge0cl  46336  sge0sup  46346  sge0iunmptlemfi  46368  sge0splitsn  46396  hoiprodp1  46543  sge0hsphoire  46544  hoidmv1le  46549  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem5  46554  hspmbllem2  46582  ovnovollem3  46613  vonvolmbl  46616  vonvol  46617  vonvol2  46619  fsummmodsnunz  47299  edgusgrclnbfin  47765  suppmptcfin  48220  lcosn0  48265  lincext2  48300  snlindsntor  48316