Theorem snfi 9055

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 8650	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 9034	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5123	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3601	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 587	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 8988	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 234	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4693	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 9054	. . . 4 ⊢ ∅ ∈ Fin
10		eleq1 2822	. . . 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 2108  ∃wrex 3060  Vcvv 3459  ∅c0 4308  {csn 4601   class class class wbr 5119  ωcom 7859  1_oc1o 8471   ≈ cen 8954  Fincfn 8957

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 2007  ax-8 2110  ax-9 2118  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-om 7860  df-1o 8478  df-en 8958  df-fin 8961

This theorem is referenced by:  fiprc  9057  ssfi  9185  cnvfi  9188  fnfi  9190  sucdom2  9215  fodomfi  9320  imafiOLD  9324  pwfi  9327  prfi  9333  prfiALT  9334  tpfi  9335  fodomfir  9338  unifpw  9365  snopfsupp  9401  sniffsupp  9410  ssfii  9429  cantnfp1lem1  9690  infpwfidom  10040  ficardadju  10212  ackbij1lem4  10234  ackbij1lem9  10239  ackbij1lem10  10240  fin23lem21  10351  isfin1-3  10398  axcclem  10469  zornn0g  10517  hashsng  14385  hashen1  14386  hashunsng  14408  hashunsngx  14409  hashprg  14411  hashsnlei  14434  hashxplem  14449  hashmap  14451  hashfun  14453  hashbclem  14468  hashf1lem2  14472  hashf1  14473  hash7g  14502  hash3tpexb  14510  s7f1o  14983  fsumsplitsn  15758  fsummsnunz  15768  fsumsplitsnun  15769  fsum2dlem  15784  fsumcom2  15788  ackbijnn  15842  incexclem  15850  isumltss  15862  fprod2dlem  15994  fprodcom2  15998  fprodsplitsn  16003  rexpen  16244  2ebits  16464  lcmfunsnlem2lem1  16655  lcmfunsnlem2lem2  16656  lcmfunsnlem2  16657  lcmfass  16663  phicl2  16785  ramub1lem1  17044  cshwshashnsame  17121  acsfn1  17671  acsfiindd  18561  efmnd1hash  18868  symg1hash  19369  odcau  19583  sylow2alem2  19597  gsumsnfd  19930  gsumzunsnd  19935  gsumunsnfd  19936  gsumpt  19941  ablfac1eu  20054  pgpfaclem2  20063  ablfaclem3  20068  srgbinomlem4  20187  acsfn1p  20757  uvcff  21749  psrlidm  21920  psrridm  21921  mvrcl  21950  mplsubrg  21963  mplmon  21991  mplmonmul  21992  psrbagsn  22019  psr1baslem  22118  mat1dimelbas  22407  mat1dim0  22409  mat1dimid  22410  mat1dimmul  22412  mat1dimcrng  22413  mat1f1o  22414  mat1ghm  22419  mat1mhm  22420  mat1rhm  22421  mat1scmat  22475  mvmumamul1  22490  mdetrsca  22539  mdetunilem9  22556  mdetmul  22559  pmatcoe1fsupp  22637  d1mat2pmat  22675  pmatcollpw3fi1lem1  22722  chpmat1dlem  22771  chpmat1d  22772  0cmp  23330  discmp  23334  bwth  23346  disllycmp  23434  dis1stc  23435  locfincmp  23462  dissnlocfin  23465  comppfsc  23468  1stckgenlem  23489  ptpjpre2  23516  ptopn2  23520  xkohaus  23589  xkoptsub  23590  ptcmpfi  23749  cfinufil  23864  ufinffr  23865  fin1aufil  23868  alexsubALTlem3  23985  ptcmplem5  23992  tmdgsum  24031  tsmsxplem1  24089  tsmsxplem2  24090  prdsmet  24307  imasdsf1olem  24310  prdsbl  24428  icccmplem1  24760  icccmplem2  24761  ovolsn  25446  ovolfiniun  25452  volfiniun  25498  i1f0  25638  fta1glem2  26124  fta1blem  26126  fta1lem  26265  vieta1lem2  26269  vieta1  26270  aalioulem2  26291  tayl0  26319  radcnv0  26375  wilthlem2  27029  fsumvma  27174  dchrfi  27216  cusgrfilem3  29383  eupth2eucrct  30144  trlsegvdeglem7  30153  fusgreghash2wspv  30262  ex-hash  30380  fsupprnfi  32615  ffsrn  32652  fsumiunle  32754  elrgspnlem2  33184  elrgspnlem3  33185  fply1  33517  constrfin  33726  locfinref  33818  esumcst  34040  esumsnf  34041  hasheuni  34062  rossros  34157  sibf0  34312  eulerpartlems  34338  eulerpartlemb  34346  ccatmulgnn0dir  34520  ofcccat  34521  plymulx0  34525  prodfzo03  34581  breprexp  34611  hgt750lemb  34634  hgt750leme  34636  lpadlem2  34658  derangsn  35138  onsucsuccmpi  36407  topdifinffinlem  37311  pibt2  37381  finixpnum  37575  lindsenlbs  37585  poimirlem26  37616  poimirlem27  37617  poimirlem31  37621  poimirlem32  37622  prdsbnd  37763  heiborlem3  37783  heiborlem8  37788  ismrer1  37808  reheibor  37809  pclfinN  39865  frlmvscadiccat  42476  frlmsnic  42510  selvvvval  42555  elrfi  42664  mzpcompact2lem  42721  dfac11  43033  pwslnmlem0  43062  lpirlnr  43088  mpct  45173  cnrefiisplem  45806  dvmptfprodlem  45921  dvnprodlem2  45924  stoweidlem44  46021  fourierdlem51  46134  fourierdlem80  46163  fouriersw  46208  salexct  46311  salexct3  46319  salgencntex  46320  salgensscntex  46321  sge0sn  46356  sge0tsms  46357  sge0cl  46358  sge0sup  46368  sge0iunmptlemfi  46390  sge0splitsn  46418  hoiprodp1  46565  sge0hsphoire  46566  hoidmv1le  46571  hoidmvlelem1  46572  hoidmvlelem2  46573  hoidmvlelem5  46576  hspmbllem2  46604  ovnovollem3  46635  vonvolmbl  46638  vonvol  46639  vonvol2  46641  fsummmodsnunz  47337  edgusgrclnbfin  47803  suppmptcfin  48299  lcosn0  48344  lincext2  48379  snlindsntor  48395