Theorem snfi 9071

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 8649	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 9049	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5107	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3577	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 599	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 9002	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 237	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4678	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 9070	. . . 4 ⊢ ∅ ∈ Fin
10		eleq1 2849	. . . 4 ⊢ ({𝐴} = ∅ → ({𝐴} ∈ Fin ↔ ∅ ∈ Fin))
11	9, 10	mpbiri 261	. . 3 ⊢ ({𝐴} = ∅ → {𝐴} ∈ Fin)
12	8, 11	sylbi 220	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴} ∈ Fin)
13	7, 12	pm2.61i 184	1 ⊢ {𝐴} ∈ Fin

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ∈ wcel 2145  ∃wrex 3087  Vcvv 3451  ∅c0 4279  {csn 4584   class class class wbr 5103  ωcom 7877  1_oc1o 8469   ≈ cen 8970  Fincfn 8973

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-mo 2565  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-om 7878  df-1o 8476  df-en 8974  df-fin 8977

This theorem is used by:  fiprc  9072  ssfi  9188  cnvfi  9191  fnfi  9193  sucdom2  9218  fodomfi  9304  pwfi  9310  prfi  9315  prfiALT  9316  tpfi  9317  fodomfir  9319  unifpw  9344  snopfsupp  9383  sniffsupp  9392  ssfii  9411  cantnfp1lem1  9679  hfsn  9920  infpwfidom  10107  ficardadju  10278  ackbij1lem4  10300  ackbij1lem9  10305  ackbij1lem10  10306  fin23lem21  10417  isfin1-3  10464  axcclem  10535  zornn0g  10583  hashsng  14513  hashen1  14514  hashunsng  14536  hashunsngx  14537  hashprg  14539  hashsnlei  14563  hashxplem  14578  hashmap  14580  hashfun  14582  hashbclem  14597  hashf1lem2  14601  hashf1  14602  hash7g  14631  hash3tpexb  14639  s7f1o  15119  fsumsplitsn  15910  fsummsnunz  15920  fsumsplitsnun  15921  fsum2dlem  15936  fsumcom2  15940  ackbijnn  15997  incexclem  16005  isumltss  16017  fprod2dlem  16147  fprodcom2  16151  fprodsplitsn  16156  rexpen  16396  2ebits  16617  lcmfunsnlem2lem1  16813  lcmfunsnlem2lem2  16814  lcmfunsnlem2  16815  lcmfass  16821  phicl2  16945  ramub1lem1  17204  cshwshashnsame  17281  acsfn1  17835  acsfiindd  18727  efmnd1hash  19088  symg1hash  19604  odcau  19818  sylow2alem2  19832  gsumsnfd  20165  gsumzunsnd  20170  gsumunsnfd  20171  gsumpt  20176  ablfac1eu  20289  pgpfaclem2  20298  ablfaclem3  20303  srgbinomlem4  20455  acsfn1p  21056  uvcff  22097  lindsenlbs  22157  psrlidm  22269  psrridm  22270  mvrcl  22299  mplsubrg  22312  mplmon  22344  mplmonmul  22345  psrbagsn  22372  selvvvval  22451  psr1baslem  22503  mat1dimelbas  22786  mat1dim0  22788  mat1dimid  22789  mat1dimmul  22791  mat1dimcrng  22792  mat1f1o  22793  mat1ghm  22798  mat1mhm  22799  mat1rhm  22800  mat1scmat  22854  mvmumamul1  22869  mdetrsca  22918  mdetunilem9  22935  mdetmul  22938  pmatcoe1fsupp  23019  d1mat2pmat  23057  pmatcollpw3fi1lem1  23104  chpmat1dlem  23153  chpmat1d  23154  0cmp  23712  discmp  23716  bwth  23728  disllycmp  23817  dis1stc  23818  locfincmp  23845  dissnlocfin  23848  comppfsc  23851  1stckgenlem  23872  ptpjpre2  23899  ptopn2  23903  xkohaus  23972  xkoptsub  23973  ptcmpfi  24132  cfinufil  24247  ufinffr  24248  fin1aufil  24251  alexsubALTlem3  24368  ptcmplem5  24375  tmdgsum  24414  tsmsxplem1  24472  tsmsxplem2  24473  prdsmet  24689  imasdsf1olem  24692  prdsbl  24810  icccmplem1  25142  icccmplem2  25143  ovolsn  25816  ovolfiniun  25822  volfiniun  25868  i1f0  26008  fta1glem2  26487  fta1blem  26489  plyn0mulidp  26602  fta1lem  26628  vieta1lem2  26634  vieta1  26635  aalioulem2  26660  tayl0  26689  radcnv0  26743  wilthlem2  27396  fsumvma  27540  dchrfi  27582  cusgrfilem3  30038  eupth2eucrct  30818  trlsegvdeglem7  30827  fusgreghash2wspv  30936  ex-hash  31054  fsupprnfi  33285  ffsrn  33320  fsumiunle  33420  elrgspnlem2  33804  elrgspnlem3  33805  fply1  34090  selvply1rhmlema  34150  selvply1rhmlemb  34151  mplidomlem  34159  mplmulmvr  34171  psrmonmul  34182  mplmonprod  34186  vieta  34212  constrfin  34378  locfinref  34473  esumcst  34695  esumsnf  34696  hasheuni  34717  rossros  34813  sibf0  34966  eulerpartlems  34992  eulerpartlemb  35000  ccatmulgnn0dir  35174  ofcccat  35175  prodfzo03  35232  breprexp  35262  hgt750lemb  35285  hgt750leme  35287  lpadlem2  35312  fineqvnttrclselem1  35789  derangsn  35935  onsucsuccmpi  37231  topdifinffinlem  38270  pibt2  38340  finixpnum  38528  poimirlem26  38564  poimirlem27  38565  poimirlem31  38569  poimirlem32  38570  prdsbnd  38727  heiborlem3  38747  heiborlem8  38752  ismrer1  38772  reheibor  38773  pclfinN  40957  frlmvscadiccat  43573  frlmsnic  43604  elrfi  43704  mzpcompact2lem  43761  dfac11  44063  pwslnmlem0  44092  lpirlnr  44118  mpct  46214  cnrefiisplem  46838  dvmptfprodlem  46953  dvnprodlem2  46956  stoweidlem44  47053  fourierdlem51  47166  fourierdlem80  47195  fouriersw  47240  salexct  47343  salexct3  47351  salgencntex  47352  salgensscntex  47353  sge0sn  47388  sge0tsms  47389  sge0cl  47390  sge0sup  47400  sge0iunmptlemfi  47422  sge0splitsn  47450  hoiprodp1  47597  sge0hsphoire  47598  hoidmv1le  47603  hoidmvlelem1  47604  hoidmvlelem2  47605  hoidmvlelem5  47608  hspmbllem2  47636  ovnovollem3  47667  vonvolmbl  47670  vonvol  47671  vonvol2  47673  tmachlem-agreeprod  47946  tmachlem-agreefin  47957  fsummmodsnunz  48452  edgusgrclnbfin  48939  suppmptcfin  49487  lcosn0  49531  lincext2  49566  snlindsntor  49582