Theorem snfi 8992

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 8578	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 8971	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5104	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3578	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 588	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 8924	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 234	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4676	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 8991	. . . 4 ⊢ ∅ ∈ Fin
10		eleq1 2825	. . . 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 1542   ∈ wcel 2114  ∃wrex 3062  Vcvv 3442  ∅c0 4287  {csn 4582   class class class wbr 5100  ωcom 7818  1_oc1o 8400   ≈ cen 8892  Fincfn 8895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-om 7819  df-1o 8407  df-en 8896  df-fin 8899

This theorem is referenced by:  fiprc  8993  ssfi  9109  cnvfi  9112  fnfi  9114  sucdom2  9139  fodomfi  9224  imafiOLD  9228  pwfi  9231  prfi  9236  prfiALT  9237  tpfi  9238  fodomfir  9240  unifpw  9267  snopfsupp  9306  sniffsupp  9315  ssfii  9334  cantnfp1lem1  9599  infpwfidom  9950  ficardadju  10122  ackbij1lem4  10144  ackbij1lem9  10149  ackbij1lem10  10150  fin23lem21  10261  isfin1-3  10308  axcclem  10379  zornn0g  10427  hashsng  14304  hashen1  14305  hashunsng  14327  hashunsngx  14328  hashprg  14330  hashsnlei  14353  hashxplem  14368  hashmap  14370  hashfun  14372  hashbclem  14387  hashf1lem2  14391  hashf1  14392  hash7g  14421  hash3tpexb  14429  s7f1o  14901  fsumsplitsn  15679  fsummsnunz  15689  fsumsplitsnun  15690  fsum2dlem  15705  fsumcom2  15709  ackbijnn  15763  incexclem  15771  isumltss  15783  fprod2dlem  15915  fprodcom2  15919  fprodsplitsn  15924  rexpen  16165  2ebits  16386  lcmfunsnlem2lem1  16577  lcmfunsnlem2lem2  16578  lcmfunsnlem2  16579  lcmfass  16585  phicl2  16707  ramub1lem1  16966  cshwshashnsame  17043  acsfn1  17596  acsfiindd  18488  efmnd1hash  18829  symg1hash  19331  odcau  19545  sylow2alem2  19559  gsumsnfd  19892  gsumzunsnd  19897  gsumunsnfd  19898  gsumpt  19903  ablfac1eu  20016  pgpfaclem2  20025  ablfaclem3  20030  srgbinomlem4  20176  acsfn1p  20744  uvcff  21758  psrlidm  21929  psrridm  21930  mvrcl  21959  mplsubrg  21972  mplmon  22002  mplmonmul  22003  psrbagsn  22030  psr1baslem  22137  mat1dimelbas  22427  mat1dim0  22429  mat1dimid  22430  mat1dimmul  22432  mat1dimcrng  22433  mat1f1o  22434  mat1ghm  22439  mat1mhm  22440  mat1rhm  22441  mat1scmat  22495  mvmumamul1  22510  mdetrsca  22559  mdetunilem9  22576  mdetmul  22579  pmatcoe1fsupp  22657  d1mat2pmat  22695  pmatcollpw3fi1lem1  22742  chpmat1dlem  22791  chpmat1d  22792  0cmp  23350  discmp  23354  bwth  23366  disllycmp  23454  dis1stc  23455  locfincmp  23482  dissnlocfin  23485  comppfsc  23488  1stckgenlem  23509  ptpjpre2  23536  ptopn2  23540  xkohaus  23609  xkoptsub  23610  ptcmpfi  23769  cfinufil  23884  ufinffr  23885  fin1aufil  23888  alexsubALTlem3  24005  ptcmplem5  24012  tmdgsum  24051  tsmsxplem1  24109  tsmsxplem2  24110  prdsmet  24326  imasdsf1olem  24329  prdsbl  24447  icccmplem1  24779  icccmplem2  24780  ovolsn  25464  ovolfiniun  25470  volfiniun  25516  i1f0  25656  fta1glem2  26142  fta1blem  26144  fta1lem  26283  vieta1lem2  26287  vieta1  26288  aalioulem2  26309  tayl0  26337  radcnv0  26393  wilthlem2  27047  fsumvma  27192  dchrfi  27234  cusgrfilem3  29543  eupth2eucrct  30304  trlsegvdeglem7  30313  fusgreghash2wspv  30422  ex-hash  30540  fsupprnfi  32782  ffsrn  32818  fsumiunle  32921  elrgspnlem2  33337  elrgspnlem3  33338  fply1  33651  mplmulmvr  33716  psrmonmul  33727  mplmonprod  33731  vieta  33757  constrfin  33924  locfinref  34019  esumcst  34241  esumsnf  34242  hasheuni  34263  rossros  34358  sibf0  34512  eulerpartlems  34538  eulerpartlemb  34546  ccatmulgnn0dir  34720  ofcccat  34721  plymulx0  34725  prodfzo03  34781  breprexp  34811  hgt750lemb  34834  hgt750leme  34836  lpadlem2  34858  fineqvnttrclselem1  35299  derangsn  35386  onsucsuccmpi  36659  topdifinffinlem  37602  pibt2  37672  finixpnum  37856  lindsenlbs  37866  poimirlem26  37897  poimirlem27  37898  poimirlem31  37902  poimirlem32  37903  prdsbnd  38044  heiborlem3  38064  heiborlem8  38069  ismrer1  38089  reheibor  38090  pclfinN  40276  frlmvscadiccat  42876  frlmsnic  42910  selvvvval  42943  elrfi  43051  mzpcompact2lem  43108  dfac11  43419  pwslnmlem0  43448  lpirlnr  43474  mpct  45559  cnrefiisplem  46187  dvmptfprodlem  46302  dvnprodlem2  46305  stoweidlem44  46402  fourierdlem51  46515  fourierdlem80  46544  fouriersw  46589  salexct  46692  salexct3  46700  salgencntex  46701  salgensscntex  46702  sge0sn  46737  sge0tsms  46738  sge0cl  46739  sge0sup  46749  sge0iunmptlemfi  46771  sge0splitsn  46799  hoiprodp1  46946  sge0hsphoire  46947  hoidmv1le  46952  hoidmvlelem1  46953  hoidmvlelem2  46954  hoidmvlelem5  46957  hspmbllem2  46985  ovnovollem3  47016  vonvolmbl  47019  vonvol  47020  vonvol2  47022  fsummmodsnunz  47735  edgusgrclnbfin  48202  suppmptcfin  48736  lcosn0  48780  lincext2  48815  snlindsntor  48831