Theorem snfi 9073

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 8662	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 9047	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5149	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3607	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 585	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 8999	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 233	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4716	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 9072	. . . 4 ⊢ ∅ ∈ Fin
10		eleq1 2814	. . . 4 ⊢ ({𝐴} = ∅ → ({𝐴} ∈ Fin ↔ ∅ ∈ Fin))
11	9, 10	mpbiri 257	. . 3 ⊢ ({𝐴} = ∅ → {𝐴} ∈ Fin)
12	8, 11	sylbi 216	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴} ∈ Fin)
13	7, 12	pm2.61i 182	1 ⊢ {𝐴} ∈ Fin

Syntax hints:  ¬ wn 3   = wceq 1534   ∈ wcel 2099  ∃wrex 3060  Vcvv 3462  ∅c0 4322  {csn 4623   class class class wbr 5145  ωcom 7868  1_oc1o 8481   ≈ cen 8963  Fincfn 8966

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-12 2167  ax-ext 2697  ax-sep 5296  ax-nul 5303  ax-pr 5425

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-mo 2529  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-br 5146  df-opab 5208  df-tr 5263  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5629  df-we 5631  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-om 7869  df-1o 8488  df-en 8967  df-fin 8970

This theorem is referenced by:  fiprc  9075  ssfi  9204  cnvfi  9207  fnfi  9208  sucdom2  9233  fodomfi  9345  imafiOLD  9349  pwfi  9352  prfi  9358  prfiALT  9359  tpfi  9360  fodomfir  9363  unifpw  9392  snopfsupp  9427  sniffsupp  9436  ssfii  9455  cantnfp1lem1  9714  infpwfidom  10064  ficardadju  10235  ackbij1lem4  10257  ackbij1lem9  10262  ackbij1lem10  10263  fin23lem21  10373  isfin1-3  10420  axcclem  10491  zornn0g  10539  hashsng  14381  hashen1  14382  hashunsng  14404  hashunsngx  14405  hashprg  14407  hashsnlei  14430  hashxplem  14445  hashmap  14447  hashfun  14449  hashbclem  14464  hashf1lem1OLD  14469  hashf1lem2  14470  hashf1  14471  fsumsplitsn  15743  fsummsnunz  15753  fsumsplitsnun  15754  fsum2dlem  15769  fsumcom2  15773  ackbijnn  15827  incexclem  15835  isumltss  15847  fprod2dlem  15977  fprodcom2  15981  fprodsplitsn  15986  rexpen  16225  2ebits  16442  lcmfunsnlem2lem1  16634  lcmfunsnlem2lem2  16635  lcmfunsnlem2  16636  lcmfass  16642  phicl2  16765  ramub1lem1  17023  cshwshashnsame  17101  acsfn1  17669  acsfiindd  18573  efmnd1hash  18877  symg1hash  19383  odcau  19598  sylow2alem2  19612  gsumsnfd  19945  gsumzunsnd  19950  gsumunsnfd  19951  gsumpt  19956  ablfac1eu  20069  pgpfaclem2  20078  ablfaclem3  20083  srgbinomlem4  20208  acsfn1p  20774  uvcff  21785  psrlidm  21967  psrridm  21968  mvrcl  21997  mplsubrg  22010  mplmon  22038  mplmonmul  22039  psrbagsn  22072  psr1baslem  22170  mat1dimelbas  22461  mat1dim0  22463  mat1dimid  22464  mat1dimmul  22466  mat1dimcrng  22467  mat1f1o  22468  mat1ghm  22473  mat1mhm  22474  mat1rhm  22475  mat1scmat  22529  mvmumamul1  22544  mdetrsca  22593  mdetunilem9  22610  mdetmul  22613  pmatcoe1fsupp  22691  d1mat2pmat  22729  pmatcollpw3fi1lem1  22776  chpmat1dlem  22825  chpmat1d  22826  0cmp  23386  discmp  23390  bwth  23402  disllycmp  23490  dis1stc  23491  locfincmp  23518  dissnlocfin  23521  comppfsc  23524  1stckgenlem  23545  ptpjpre2  23572  ptopn2  23576  xkohaus  23645  xkoptsub  23646  ptcmpfi  23805  cfinufil  23920  ufinffr  23921  fin1aufil  23924  alexsubALTlem3  24041  ptcmplem5  24048  tmdgsum  24087  tsmsxplem1  24145  tsmsxplem2  24146  prdsmet  24364  imasdsf1olem  24367  prdsbl  24488  icccmplem1  24826  icccmplem2  24827  ovolsn  25512  ovolfiniun  25518  volfiniun  25564  i1f0  25704  fta1glem2  26193  fta1blem  26195  fta1lem  26332  vieta1lem2  26336  vieta1  26337  aalioulem2  26358  tayl0  26386  radcnv0  26442  wilthlem2  27094  fsumvma  27239  dchrfi  27281  cusgrfilem3  29391  eupth2eucrct  30147  trlsegvdeglem7  30156  fusgreghash2wspv  30265  ex-hash  30383  fsupprnfi  32604  ffsrn  32643  fsumiunle  32733  fply1  33437  constrfin  33618  locfinref  33669  esumcst  33909  esumsnf  33910  hasheuni  33931  rossros  34026  sibf0  34181  eulerpartlems  34207  eulerpartlemb  34215  ccatmulgnn0dir  34401  ofcccat  34402  plymulx0  34406  prodfzo03  34462  breprexp  34492  hgt750lemb  34515  hgt750leme  34517  lpadlem2  34539  derangsn  35011  onsucsuccmpi  36168  topdifinffinlem  37067  pibt2  37137  finixpnum  37319  lindsenlbs  37329  poimirlem26  37360  poimirlem27  37361  poimirlem31  37365  poimirlem32  37366  prdsbnd  37507  heiborlem3  37527  heiborlem8  37532  ismrer1  37552  reheibor  37553  pclfinN  39612  frlmvscadiccat  42196  frlmsnic  42230  selvvvval  42275  elrfi  42388  mzpcompact2lem  42445  dfac11  42760  pwslnmlem0  42789  lpirlnr  42815  mpct  44844  cnrefiisplem  45486  dvmptfprodlem  45601  dvnprodlem2  45604  stoweidlem44  45701  fourierdlem51  45814  fourierdlem80  45843  fouriersw  45888  salexct  45991  salexct3  45999  salgencntex  46000  salgensscntex  46001  sge0sn  46036  sge0tsms  46037  sge0cl  46038  sge0sup  46048  sge0iunmptlemfi  46070  sge0splitsn  46098  hoiprodp1  46245  sge0hsphoire  46246  hoidmv1le  46251  hoidmvlelem1  46252  hoidmvlelem2  46253  hoidmvlelem5  46256  hspmbllem2  46284  ovnovollem3  46315  vonvolmbl  46318  vonvol  46319  vonvol2  46321  fsummmodsnunz  46983  edgusgrclnbfin  47445  suppmptcfin  47794  lcosn0  47839  lincext2  47874  snlindsntor  47890