Theorem snfi 8968

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 8558	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 8947	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5096	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3577	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 587	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 8901	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 234	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4669	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 8967	. . . 4 ⊢ ∅ ∈ Fin
10		eleq1 2816	. . . 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 1540   ∈ wcel 2109  ∃wrex 3053  Vcvv 3436  ∅c0 4284  {csn 4577   class class class wbr 5092  ωcom 7799  1_oc1o 8381   ≈ cen 8869  Fincfn 8872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-mo 2533  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-om 7800  df-1o 8388  df-en 8873  df-fin 8876

This theorem is referenced by:  fiprc  8970  ssfi  9087  cnvfi  9090  fnfi  9092  sucdom2  9117  fodomfi  9201  imafiOLD  9205  pwfi  9208  prfi  9213  prfiALT  9214  tpfi  9215  fodomfir  9218  unifpw  9245  snopfsupp  9281  sniffsupp  9290  ssfii  9309  cantnfp1lem1  9574  infpwfidom  9922  ficardadju  10094  ackbij1lem4  10116  ackbij1lem9  10121  ackbij1lem10  10122  fin23lem21  10233  isfin1-3  10280  axcclem  10351  zornn0g  10399  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  18766  symg1hash  19269  odcau  19483  sylow2alem2  19497  gsumsnfd  19830  gsumzunsnd  19835  gsumunsnfd  19836  gsumpt  19841  ablfac1eu  19954  pgpfaclem2  19963  ablfaclem3  19968  srgbinomlem4  20114  acsfn1p  20684  uvcff  21698  psrlidm  21869  psrridm  21870  mvrcl  21899  mplsubrg  21912  mplmon  21940  mplmonmul  21941  psrbagsn  21968  psr1baslem  22067  mat1dimelbas  22356  mat1dim0  22358  mat1dimid  22359  mat1dimmul  22361  mat1dimcrng  22362  mat1f1o  22363  mat1ghm  22368  mat1mhm  22369  mat1rhm  22370  mat1scmat  22424  mvmumamul1  22439  mdetrsca  22488  mdetunilem9  22505  mdetmul  22508  pmatcoe1fsupp  22586  d1mat2pmat  22624  pmatcollpw3fi1lem1  22671  chpmat1dlem  22720  chpmat1d  22721  0cmp  23279  discmp  23283  bwth  23295  disllycmp  23383  dis1stc  23384  locfincmp  23411  dissnlocfin  23414  comppfsc  23417  1stckgenlem  23438  ptpjpre2  23465  ptopn2  23469  xkohaus  23538  xkoptsub  23539  ptcmpfi  23698  cfinufil  23813  ufinffr  23814  fin1aufil  23817  alexsubALTlem3  23934  ptcmplem5  23941  tmdgsum  23980  tsmsxplem1  24038  tsmsxplem2  24039  prdsmet  24256  imasdsf1olem  24259  prdsbl  24377  icccmplem1  24709  icccmplem2  24710  ovolsn  25394  ovolfiniun  25400  volfiniun  25446  i1f0  25586  fta1glem2  26072  fta1blem  26074  fta1lem  26213  vieta1lem2  26217  vieta1  26218  aalioulem2  26239  tayl0  26267  radcnv0  26323  wilthlem2  26977  fsumvma  27122  dchrfi  27164  cusgrfilem3  29403  eupth2eucrct  30161  trlsegvdeglem7  30170  fusgreghash2wspv  30279  ex-hash  30397  fsupprnfi  32634  ffsrn  32672  fsumiunle  32774  elrgspnlem2  33183  elrgspnlem3  33184  fply1  33493  constrfin  33713  locfinref  33808  esumcst  34030  esumsnf  34031  hasheuni  34052  rossros  34147  sibf0  34302  eulerpartlems  34328  eulerpartlemb  34336  ccatmulgnn0dir  34510  ofcccat  34511  plymulx0  34515  prodfzo03  34571  breprexp  34601  hgt750lemb  34624  hgt750leme  34626  lpadlem2  34648  fineqvnttrclselem1  35074  derangsn  35147  onsucsuccmpi  36421  topdifinffinlem  37325  pibt2  37395  finixpnum  37589  lindsenlbs  37599  poimirlem26  37630  poimirlem27  37631  poimirlem31  37635  poimirlem32  37636  prdsbnd  37777  heiborlem3  37797  heiborlem8  37802  ismrer1  37822  reheibor  37823  pclfinN  39883  frlmvscadiccat  42483  frlmsnic  42517  selvvvval  42562  elrfi  42671  mzpcompact2lem  42728  dfac11  43039  pwslnmlem0  43068  lpirlnr  43094  mpct  45183  cnrefiisplem  45814  dvmptfprodlem  45929  dvnprodlem2  45932  stoweidlem44  46029  fourierdlem51  46142  fourierdlem80  46171  fouriersw  46216  salexct  46319  salexct3  46327  salgencntex  46328  salgensscntex  46329  sge0sn  46364  sge0tsms  46365  sge0cl  46366  sge0sup  46376  sge0iunmptlemfi  46398  sge0splitsn  46426  hoiprodp1  46573  sge0hsphoire  46574  hoidmv1le  46579  hoidmvlelem1  46580  hoidmvlelem2  46581  hoidmvlelem5  46584  hspmbllem2  46612  ovnovollem3  46643  vonvolmbl  46646  vonvol  46647  vonvol2  46649  fsummmodsnunz  47363  edgusgrclnbfin  47830  suppmptcfin  48364  lcosn0  48409  lincext2  48444  snlindsntor  48460