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  17598  acsfiindd  18488  efmnd1hash  18795  symg1hash  19296  odcau  19510  sylow2alem2  19524  gsumsnfd  19857  gsumzunsnd  19862  gsumunsnfd  19863  gsumpt  19868  ablfac1eu  19981  pgpfaclem2  19990  ablfaclem3  19995  srgbinomlem4  20114  acsfn1p  20684  uvcff  21676  psrlidm  21847  psrridm  21848  mvrcl  21877  mplsubrg  21890  mplmon  21918  mplmonmul  21919  psrbagsn  21946  psr1baslem  22045  mat1dimelbas  22334  mat1dim0  22336  mat1dimid  22337  mat1dimmul  22339  mat1dimcrng  22340  mat1f1o  22341  mat1ghm  22346  mat1mhm  22347  mat1rhm  22348  mat1scmat  22402  mvmumamul1  22417  mdetrsca  22466  mdetunilem9  22483  mdetmul  22486  pmatcoe1fsupp  22564  d1mat2pmat  22602  pmatcollpw3fi1lem1  22649  chpmat1dlem  22698  chpmat1d  22699  0cmp  23257  discmp  23261  bwth  23273  disllycmp  23361  dis1stc  23362  locfincmp  23389  dissnlocfin  23392  comppfsc  23395  1stckgenlem  23416  ptpjpre2  23443  ptopn2  23447  xkohaus  23516  xkoptsub  23517  ptcmpfi  23676  cfinufil  23791  ufinffr  23792  fin1aufil  23795  alexsubALTlem3  23912  ptcmplem5  23919  tmdgsum  23958  tsmsxplem1  24016  tsmsxplem2  24017  prdsmet  24234  imasdsf1olem  24237  prdsbl  24355  icccmplem1  24687  icccmplem2  24688  ovolsn  25372  ovolfiniun  25378  volfiniun  25424  i1f0  25564  fta1glem2  26050  fta1blem  26052  fta1lem  26191  vieta1lem2  26195  vieta1  26196  aalioulem2  26217  tayl0  26245  radcnv0  26301  wilthlem2  26955  fsumvma  27100  dchrfi  27142  cusgrfilem3  29361  eupth2eucrct  30119  trlsegvdeglem7  30128  fusgreghash2wspv  30237  ex-hash  30355  fsupprnfi  32588  ffsrn  32625  fsumiunle  32727  elrgspnlem2  33167  elrgspnlem3  33168  fply1  33500  constrfin  33709  locfinref  33804  esumcst  34026  esumsnf  34027  hasheuni  34048  rossros  34143  sibf0  34298  eulerpartlems  34324  eulerpartlemb  34332  ccatmulgnn0dir  34506  ofcccat  34507  plymulx0  34511  prodfzo03  34567  breprexp  34597  hgt750lemb  34620  hgt750leme  34622  lpadlem2  34644  derangsn  35130  onsucsuccmpi  36404  topdifinffinlem  37308  pibt2  37378  finixpnum  37572  lindsenlbs  37582  poimirlem26  37613  poimirlem27  37614  poimirlem31  37618  poimirlem32  37619  prdsbnd  37760  heiborlem3  37780  heiborlem8  37785  ismrer1  37805  reheibor  37806  pclfinN  39867  frlmvscadiccat  42467  frlmsnic  42501  selvvvval  42546  elrfi  42655  mzpcompact2lem  42712  dfac11  43024  pwslnmlem0  43053  lpirlnr  43079  mpct  45168  cnrefiisplem  45800  dvmptfprodlem  45915  dvnprodlem2  45918  stoweidlem44  46015  fourierdlem51  46128  fourierdlem80  46157  fouriersw  46202  salexct  46305  salexct3  46313  salgencntex  46314  salgensscntex  46315  sge0sn  46350  sge0tsms  46351  sge0cl  46352  sge0sup  46362  sge0iunmptlemfi  46384  sge0splitsn  46412  hoiprodp1  46559  sge0hsphoire  46560  hoidmv1le  46565  hoidmvlelem1  46566  hoidmvlelem2  46567  hoidmvlelem5  46570  hspmbllem2  46598  ovnovollem3  46629  vonvolmbl  46632  vonvol  46633  vonvol2  46635  fsummmodsnunz  47349  edgusgrclnbfin  47815  suppmptcfin  48337  lcosn0  48382  lincext2  48417  snlindsntor  48433