Theorem snfi 8991

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 8581	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 8970	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5106	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3585	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 587	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 8924	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 234	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4677	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 8990	. . . 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 3444  ∅c0 4292  {csn 4585   class class class wbr 5102  ωcom 7822  1_oc1o 8404   ≈ cen 8892  Fincfn 8895

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-tr 5210  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 6323  df-on 6324  df-lim 6325  df-suc 6326  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-om 7823  df-1o 8411  df-en 8896  df-fin 8899

This theorem is referenced by:  fiprc  8993  ssfi  9114  cnvfi  9117  fnfi  9119  sucdom2  9144  fodomfi  9237  imafiOLD  9241  pwfi  9244  prfi  9250  prfiALT  9251  tpfi  9252  fodomfir  9255  unifpw  9282  snopfsupp  9318  sniffsupp  9327  ssfii  9346  cantnfp1lem1  9607  infpwfidom  9957  ficardadju  10129  ackbij1lem4  10151  ackbij1lem9  10156  ackbij1lem10  10157  fin23lem21  10268  isfin1-3  10315  axcclem  10386  zornn0g  10434  hashsng  14310  hashen1  14311  hashunsng  14333  hashunsngx  14334  hashprg  14336  hashsnlei  14359  hashxplem  14374  hashmap  14376  hashfun  14378  hashbclem  14393  hashf1lem2  14397  hashf1  14398  hash7g  14427  hash3tpexb  14435  s7f1o  14908  fsumsplitsn  15686  fsummsnunz  15696  fsumsplitsnun  15697  fsum2dlem  15712  fsumcom2  15716  ackbijnn  15770  incexclem  15778  isumltss  15790  fprod2dlem  15922  fprodcom2  15926  fprodsplitsn  15931  rexpen  16172  2ebits  16393  lcmfunsnlem2lem1  16584  lcmfunsnlem2lem2  16585  lcmfunsnlem2  16586  lcmfass  16592  phicl2  16714  ramub1lem1  16973  cshwshashnsame  17050  acsfn1  17602  acsfiindd  18494  efmnd1hash  18801  symg1hash  19304  odcau  19518  sylow2alem2  19532  gsumsnfd  19865  gsumzunsnd  19870  gsumunsnfd  19871  gsumpt  19876  ablfac1eu  19989  pgpfaclem2  19998  ablfaclem3  20003  srgbinomlem4  20149  acsfn1p  20719  uvcff  21733  psrlidm  21904  psrridm  21905  mvrcl  21934  mplsubrg  21947  mplmon  21975  mplmonmul  21976  psrbagsn  22003  psr1baslem  22102  mat1dimelbas  22391  mat1dim0  22393  mat1dimid  22394  mat1dimmul  22396  mat1dimcrng  22397  mat1f1o  22398  mat1ghm  22403  mat1mhm  22404  mat1rhm  22405  mat1scmat  22459  mvmumamul1  22474  mdetrsca  22523  mdetunilem9  22540  mdetmul  22543  pmatcoe1fsupp  22621  d1mat2pmat  22659  pmatcollpw3fi1lem1  22706  chpmat1dlem  22755  chpmat1d  22756  0cmp  23314  discmp  23318  bwth  23330  disllycmp  23418  dis1stc  23419  locfincmp  23446  dissnlocfin  23449  comppfsc  23452  1stckgenlem  23473  ptpjpre2  23500  ptopn2  23504  xkohaus  23573  xkoptsub  23574  ptcmpfi  23733  cfinufil  23848  ufinffr  23849  fin1aufil  23852  alexsubALTlem3  23969  ptcmplem5  23976  tmdgsum  24015  tsmsxplem1  24073  tsmsxplem2  24074  prdsmet  24291  imasdsf1olem  24294  prdsbl  24412  icccmplem1  24744  icccmplem2  24745  ovolsn  25429  ovolfiniun  25435  volfiniun  25481  i1f0  25621  fta1glem2  26107  fta1blem  26109  fta1lem  26248  vieta1lem2  26252  vieta1  26253  aalioulem2  26274  tayl0  26302  radcnv0  26358  wilthlem2  27012  fsumvma  27157  dchrfi  27199  cusgrfilem3  29438  eupth2eucrct  30196  trlsegvdeglem7  30205  fusgreghash2wspv  30314  ex-hash  30432  fsupprnfi  32665  ffsrn  32702  fsumiunle  32804  elrgspnlem2  33210  elrgspnlem3  33211  fply1  33520  constrfin  33729  locfinref  33824  esumcst  34046  esumsnf  34047  hasheuni  34068  rossros  34163  sibf0  34318  eulerpartlems  34344  eulerpartlemb  34352  ccatmulgnn0dir  34526  ofcccat  34527  plymulx0  34531  prodfzo03  34587  breprexp  34617  hgt750lemb  34640  hgt750leme  34642  lpadlem2  34664  derangsn  35150  onsucsuccmpi  36424  topdifinffinlem  37328  pibt2  37398  finixpnum  37592  lindsenlbs  37602  poimirlem26  37633  poimirlem27  37634  poimirlem31  37638  poimirlem32  37639  prdsbnd  37780  heiborlem3  37800  heiborlem8  37805  ismrer1  37825  reheibor  37826  pclfinN  39887  frlmvscadiccat  42487  frlmsnic  42521  selvvvval  42566  elrfi  42675  mzpcompact2lem  42732  dfac11  43044  pwslnmlem0  43073  lpirlnr  43099  mpct  45188  cnrefiisplem  45820  dvmptfprodlem  45935  dvnprodlem2  45938  stoweidlem44  46035  fourierdlem51  46148  fourierdlem80  46177  fouriersw  46222  salexct  46325  salexct3  46333  salgencntex  46334  salgensscntex  46335  sge0sn  46370  sge0tsms  46371  sge0cl  46372  sge0sup  46382  sge0iunmptlemfi  46404  sge0splitsn  46432  hoiprodp1  46579  sge0hsphoire  46580  hoidmv1le  46585  hoidmvlelem1  46586  hoidmvlelem2  46587  hoidmvlelem5  46590  hspmbllem2  46618  ovnovollem3  46649  vonvolmbl  46652  vonvol  46653  vonvol2  46655  fsummmodsnunz  47369  edgusgrclnbfin  47835  suppmptcfin  48357  lcosn0  48402  lincext2  48437  snlindsntor  48453