Theorem snfi 9036

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 8622	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 9015	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5113	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3581	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 598	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		isfi 8968	. . 3 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
7	5, 6	sylibr 237	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ Fin)
8		snprc 4683	. . 3 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
9		0fi 9035	. . . 4 ⊢ ∅ ∈ Fin
10		eleq1 2851	. . . 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

Syntax hints:  ¬ wn 3   = wceq 1570   ∈ wcel 2143  ∃wrex 3089  Vcvv 3455  ∅c0 4286  {csn 4589   class class class wbr 5109  ωcom 7858  1_oc1o 8442   ≈ cen 8936  Fincfn 8939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-om 7859  df-1o 8449  df-en 8940  df-fin 8943

This theorem is referenced by:  fiprc  9037  ssfi  9153  cnvfi  9156  fnfi  9158  sucdom2  9183  fodomfi  9268  pwfi  9274  prfi  9279  prfiALT  9280  tpfi  9281  fodomfir  9283  unifpw  9308  snopfsupp  9347  sniffsupp  9356  ssfii  9375  cantnfp1lem1  9643  infpwfidom  10008  ficardadju  10179  ackbij1lem4  10201  ackbij1lem9  10206  ackbij1lem10  10207  fin23lem21  10318  isfin1-3  10365  axcclem  10436  zornn0g  10484  hashsng  14401  hashen1  14402  hashunsng  14424  hashunsngx  14425  hashprg  14427  hashsnlei  14451  hashxplem  14466  hashmap  14468  hashfun  14470  hashbclem  14485  hashf1lem2  14489  hashf1  14490  hash7g  14519  hash3tpexb  14527  s7f1o  14999  fsumsplitsn  15791  fsummsnunz  15801  fsumsplitsnun  15802  fsum2dlem  15817  fsumcom2  15821  ackbijnn  15878  incexclem  15886  isumltss  15898  fprod2dlem  16030  fprodcom2  16034  fprodsplitsn  16039  rexpen  16279  2ebits  16500  lcmfunsnlem2lem1  16691  lcmfunsnlem2lem2  16692  lcmfunsnlem2  16693  lcmfass  16699  phicl2  16822  ramub1lem1  17081  cshwshashnsame  17158  acsfn1  17712  acsfiindd  18604  efmnd1hash  18946  symg1hash  19455  odcau  19669  sylow2alem2  19683  gsumsnfd  20016  gsumzunsnd  20021  gsumunsnfd  20022  gsumpt  20027  ablfac1eu  20140  pgpfaclem2  20149  ablfaclem3  20154  srgbinomlem4  20306  acsfn1p  20902  uvcff  21941  psrlidm  22111  psrridm  22112  mvrcl  22141  mplsubrg  22154  mplmon  22186  mplmonmul  22187  psrbagsn  22214  selvvvval  22293  psr1baslem  22345  mat1dimelbas  22628  mat1dim0  22630  mat1dimid  22631  mat1dimmul  22633  mat1dimcrng  22634  mat1f1o  22635  mat1ghm  22640  mat1mhm  22641  mat1rhm  22642  mat1scmat  22696  mvmumamul1  22711  mdetrsca  22760  mdetunilem9  22777  mdetmul  22780  pmatcoe1fsupp  22858  d1mat2pmat  22896  pmatcollpw3fi1lem1  22943  chpmat1dlem  22992  chpmat1d  22993  0cmp  23551  discmp  23555  bwth  23567  disllycmp  23655  dis1stc  23656  locfincmp  23683  dissnlocfin  23686  comppfsc  23689  1stckgenlem  23710  ptpjpre2  23737  ptopn2  23741  xkohaus  23810  xkoptsub  23811  ptcmpfi  23970  cfinufil  24085  ufinffr  24086  fin1aufil  24089  alexsubALTlem3  24206  ptcmplem5  24213  tmdgsum  24252  tsmsxplem1  24310  tsmsxplem2  24311  prdsmet  24527  imasdsf1olem  24530  prdsbl  24648  icccmplem1  24980  icccmplem2  24981  ovolsn  25654  ovolfiniun  25660  volfiniun  25706  i1f0  25846  fta1glem2  26326  fta1blem  26328  plyn0mulidp  26442  fta1lem  26468  vieta1lem2  26472  vieta1  26473  aalioulem2  26496  tayl0  26525  radcnv0  26579  wilthlem2  27233  fsumvma  27377  dchrfi  27419  cusgrfilem3  29807  eupth2eucrct  30568  trlsegvdeglem7  30577  fusgreghash2wspv  30686  ex-hash  30804  fsupprnfi  33037  ffsrn  33073  fsumiunle  33173  elrgspnlem2  33563  elrgspnlem3  33564  fply1  33848  selvply1rhmlema  33908  selvply1rhmlemb  33909  mplidomlem  33917  mplmulmvr  33929  psrmonmul  33940  mplmonprod  33944  vieta  33970  constrfin  34136  locfinref  34231  esumcst  34453  esumsnf  34454  hasheuni  34475  rossros  34570  sibf0  34724  eulerpartlems  34750  eulerpartlemb  34758  ccatmulgnn0dir  34932  ofcccat  34933  prodfzo03  34990  breprexp  35020  hgt750lemb  35043  hgt750leme  35045  lpadlem2  35070  fineqvnttrclselem1  35534  derangsn  35662  onsucsuccmpi  36954  topdifinffinlem  37993  pibt2  38063  finixpnum  38256  lindsenlbs  38266  poimirlem26  38297  poimirlem27  38298  poimirlem31  38302  poimirlem32  38303  prdsbnd  38444  heiborlem3  38464  heiborlem8  38469  ismrer1  38489  reheibor  38490  pclfinN  40674  frlmvscadiccat  43280  frlmsnic  43308  elrfi  43425  mzpcompact2lem  43482  dfac11  43789  pwslnmlem0  43818  lpirlnr  43844  mpct  45918  cnrefiisplem  46543  dvmptfprodlem  46658  dvnprodlem2  46661  stoweidlem44  46758  fourierdlem51  46871  fourierdlem80  46900  fouriersw  46945  salexct  47048  salexct3  47056  salgencntex  47057  salgensscntex  47058  sge0sn  47093  sge0tsms  47094  sge0cl  47095  sge0sup  47105  sge0iunmptlemfi  47127  sge0splitsn  47155  hoiprodp1  47302  sge0hsphoire  47303  hoidmv1le  47308  hoidmvlelem1  47309  hoidmvlelem2  47310  hoidmvlelem5  47313  hspmbllem2  47341  ovnovollem3  47372  vonvolmbl  47375  vonvol  47376  vonvol2  47378  fsummmodsnunz  48120  edgusgrclnbfin  48607  suppmptcfin  49156  lcosn0  49200  lincext2  49235  snlindsntor  49251