Theorem snfi 9109

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 8696	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 9084	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5170	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3635	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 586	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 9036	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 234	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4742	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 9108	. . . 4 ⊢ ∅ ∈ Fin
10		eleq1 2832	. . . 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 1537   ∈ wcel 2108  ∃wrex 3076  Vcvv 3488  ∅c0 4352  {csn 4648   class class class wbr 5166  ωcom 7903  1_oc1o 8515   ≈ cen 9000  Fincfn 9003

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-mo 2543  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-om 7904  df-1o 8522  df-en 9004  df-fin 9007

This theorem is referenced by:  fiprc  9111  ssfi  9240  cnvfi  9243  fnfi  9244  sucdom2  9269  fodomfi  9378  imafiOLD  9382  pwfi  9385  prfi  9391  prfiALT  9392  tpfi  9393  fodomfir  9396  unifpw  9425  snopfsupp  9460  sniffsupp  9469  ssfii  9488  cantnfp1lem1  9747  infpwfidom  10097  ficardadju  10269  ackbij1lem4  10291  ackbij1lem9  10296  ackbij1lem10  10297  fin23lem21  10408  isfin1-3  10455  axcclem  10526  zornn0g  10574  hashsng  14418  hashen1  14419  hashunsng  14441  hashunsngx  14442  hashprg  14444  hashsnlei  14467  hashxplem  14482  hashmap  14484  hashfun  14486  hashbclem  14501  hashf1lem2  14505  hashf1  14506  hash7g  14535  hash3tpexb  14543  s7f1o  15015  fsumsplitsn  15792  fsummsnunz  15802  fsumsplitsnun  15803  fsum2dlem  15818  fsumcom2  15822  ackbijnn  15876  incexclem  15884  isumltss  15896  fprod2dlem  16028  fprodcom2  16032  fprodsplitsn  16037  rexpen  16276  2ebits  16493  lcmfunsnlem2lem1  16685  lcmfunsnlem2lem2  16686  lcmfunsnlem2  16687  lcmfass  16693  phicl2  16815  ramub1lem1  17073  cshwshashnsame  17151  acsfn1  17719  acsfiindd  18623  efmnd1hash  18927  symg1hash  19431  odcau  19646  sylow2alem2  19660  gsumsnfd  19993  gsumzunsnd  19998  gsumunsnfd  19999  gsumpt  20004  ablfac1eu  20117  pgpfaclem2  20126  ablfaclem3  20131  srgbinomlem4  20256  acsfn1p  20822  uvcff  21834  psrlidm  22005  psrridm  22006  mvrcl  22035  mplsubrg  22048  mplmon  22076  mplmonmul  22077  psrbagsn  22110  psr1baslem  22207  mat1dimelbas  22498  mat1dim0  22500  mat1dimid  22501  mat1dimmul  22503  mat1dimcrng  22504  mat1f1o  22505  mat1ghm  22510  mat1mhm  22511  mat1rhm  22512  mat1scmat  22566  mvmumamul1  22581  mdetrsca  22630  mdetunilem9  22647  mdetmul  22650  pmatcoe1fsupp  22728  d1mat2pmat  22766  pmatcollpw3fi1lem1  22813  chpmat1dlem  22862  chpmat1d  22863  0cmp  23423  discmp  23427  bwth  23439  disllycmp  23527  dis1stc  23528  locfincmp  23555  dissnlocfin  23558  comppfsc  23561  1stckgenlem  23582  ptpjpre2  23609  ptopn2  23613  xkohaus  23682  xkoptsub  23683  ptcmpfi  23842  cfinufil  23957  ufinffr  23958  fin1aufil  23961  alexsubALTlem3  24078  ptcmplem5  24085  tmdgsum  24124  tsmsxplem1  24182  tsmsxplem2  24183  prdsmet  24401  imasdsf1olem  24404  prdsbl  24525  icccmplem1  24863  icccmplem2  24864  ovolsn  25549  ovolfiniun  25555  volfiniun  25601  i1f0  25741  fta1glem2  26228  fta1blem  26230  fta1lem  26367  vieta1lem2  26371  vieta1  26372  aalioulem2  26393  tayl0  26421  radcnv0  26477  wilthlem2  27130  fsumvma  27275  dchrfi  27317  cusgrfilem3  29493  eupth2eucrct  30249  trlsegvdeglem7  30258  fusgreghash2wspv  30367  ex-hash  30485  fsupprnfi  32704  ffsrn  32743  fsumiunle  32833  fply1  33549  constrfin  33736  locfinref  33787  esumcst  34027  esumsnf  34028  hasheuni  34049  rossros  34144  sibf0  34299  eulerpartlems  34325  eulerpartlemb  34333  ccatmulgnn0dir  34519  ofcccat  34520  plymulx0  34524  prodfzo03  34580  breprexp  34610  hgt750lemb  34633  hgt750leme  34635  lpadlem2  34657  derangsn  35138  onsucsuccmpi  36409  topdifinffinlem  37313  pibt2  37383  finixpnum  37565  lindsenlbs  37575  poimirlem26  37606  poimirlem27  37607  poimirlem31  37611  poimirlem32  37612  prdsbnd  37753  heiborlem3  37773  heiborlem8  37778  ismrer1  37798  reheibor  37799  pclfinN  39857  frlmvscadiccat  42461  frlmsnic  42495  selvvvval  42540  elrfi  42650  mzpcompact2lem  42707  dfac11  43019  pwslnmlem0  43048  lpirlnr  43074  mpct  45108  cnrefiisplem  45750  dvmptfprodlem  45865  dvnprodlem2  45868  stoweidlem44  45965  fourierdlem51  46078  fourierdlem80  46107  fouriersw  46152  salexct  46255  salexct3  46263  salgencntex  46264  salgensscntex  46265  sge0sn  46300  sge0tsms  46301  sge0cl  46302  sge0sup  46312  sge0iunmptlemfi  46334  sge0splitsn  46362  hoiprodp1  46509  sge0hsphoire  46510  hoidmv1le  46515  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem5  46520  hspmbllem2  46548  ovnovollem3  46579  vonvolmbl  46582  vonvol  46583  vonvol2  46585  fsummmodsnunz  47249  edgusgrclnbfin  47714  suppmptcfin  48104  lcosn0  48149  lincext2  48184  snlindsntor  48200