Theorem snfi 9044

Description: A singleton is finite. (Contributed by NM, 4-Nov-2002.)

Assertion

Ref	Expression
snfi	⊢ {𝐴} ∈ Fin

Proof of Theorem snfi

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		1onn 8639	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 9019	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5153	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3613	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 588	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		snprc 4722	. . . 4 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
7		en0 9013	. . . . 5 ⊢ ({𝐴} ≈ ∅ ↔ {𝐴} = ∅)
8		peano1 7879	. . . . . 6 ⊢ ∅ ∈ ω
9		breq2 5153	. . . . . . 7 ⊢ (𝑥 = ∅ → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ ∅))
10	9	rspcev 3613	. . . . . 6 ⊢ ((∅ ∈ ω ∧ {𝐴} ≈ ∅) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
11	8, 10	mpan 689	. . . . 5 ⊢ ({𝐴} ≈ ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
12	7, 11	sylbir 234	. . . 4 ⊢ ({𝐴} = ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
13	6, 12	sylbi 216	. . 3 ⊢ (¬ 𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
14	5, 13	pm2.61i 182	. 2 ⊢ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥
15		isfi 8972	. 2 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
16	14, 15	mpbir 230	1 ⊢ {𝐴} ∈ Fin

Syntax hints:  ¬ wn 3   = wceq 1542   ∈ wcel 2107  ∃wrex 3071  Vcvv 3475  ∅c0 4323  {csn 4629   class class class wbr 5149  ωcom 7855  1_oc1o 8459   ≈ cen 8936  Fincfn 8939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-mo 2535  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-om 7856  df-1o 8466  df-en 8940  df-fin 8943

This theorem is referenced by:  fiprc  9045  ssfi  9173  imafi  9175  pwfi  9178  cnvfi  9180  fnfi  9181  sucdom2  9206  prfi  9322  tpfi  9323  unifpw  9355  snopfsupp  9386  sniffsupp  9395  ssfii  9414  cantnfp1lem1  9673  infpwfidom  10023  ficardadju  10194  ackbij1lem4  10218  ackbij1lem9  10223  ackbij1lem10  10224  fin23lem21  10334  isfin1-3  10381  axcclem  10452  zornn0g  10500  hashsng  14329  hashen1  14330  hashunsng  14352  hashunsngx  14353  hashprg  14355  hashsnlei  14378  hashxplem  14393  hashmap  14395  hashfun  14397  hashbclem  14411  hashf1lem1OLD  14416  hashf1lem2  14417  hashf1  14418  fsumsplitsn  15690  fsummsnunz  15700  fsumsplitsnun  15701  fsum2dlem  15716  fsumcom2  15720  ackbijnn  15774  incexclem  15782  isumltss  15794  fprod2dlem  15924  fprodcom2  15928  fprodsplitsn  15933  rexpen  16171  2ebits  16388  lcmfunsnlem2lem1  16575  lcmfunsnlem2lem2  16576  lcmfunsnlem2  16577  lcmfass  16583  phicl2  16701  ramub1lem1  16959  cshwshashnsame  17037  acsfn1  17605  acsfiindd  18506  efmnd1hash  18773  symg1hash  19257  odcau  19472  sylow2alem2  19486  gsumsnfd  19819  gsumzunsnd  19824  gsumunsnfd  19825  gsumpt  19830  ablfac1eu  19943  pgpfaclem2  19952  ablfaclem3  19957  srgbinomlem4  20052  acsfn1p  20415  uvcff  21346  psrlidm  21523  psrridm  21524  mvrcl  21551  mplsubrg  21564  mplmon  21590  mplmonmul  21591  psrbagsn  21624  psr1baslem  21709  mat1dimelbas  21973  mat1dim0  21975  mat1dimid  21976  mat1dimmul  21978  mat1dimcrng  21979  mat1f1o  21980  mat1ghm  21985  mat1mhm  21986  mat1rhm  21987  mat1scmat  22041  mvmumamul1  22056  mdetrsca  22105  mdetunilem9  22122  mdetmul  22125  pmatcoe1fsupp  22203  d1mat2pmat  22241  pmatcollpw3fi1lem1  22288  chpmat1dlem  22337  chpmat1d  22338  0cmp  22898  discmp  22902  bwth  22914  disllycmp  23002  dis1stc  23003  locfincmp  23030  dissnlocfin  23033  comppfsc  23036  1stckgenlem  23057  ptpjpre2  23084  ptopn2  23088  xkohaus  23157  xkoptsub  23158  ptcmpfi  23317  cfinufil  23432  ufinffr  23433  fin1aufil  23436  alexsubALTlem3  23553  ptcmplem5  23560  tmdgsum  23599  tsmsxplem1  23657  tsmsxplem2  23658  prdsmet  23876  imasdsf1olem  23879  prdsbl  24000  icccmplem1  24338  icccmplem2  24339  ovolsn  25012  ovolfiniun  25018  volfiniun  25064  i1f0  25204  fta1glem2  25684  fta1blem  25686  fta1lem  25820  vieta1lem2  25824  vieta1  25825  aalioulem2  25846  tayl0  25874  radcnv0  25928  wilthlem2  26573  fsumvma  26716  dchrfi  26758  cusgrfilem3  28714  eupth2eucrct  29470  trlsegvdeglem7  29479  fusgreghash2wspv  29588  ex-hash  29706  fsupprnfi  31914  ffsrn  31954  fsumiunle  32035  fply1  32637  locfinref  32821  esumcst  33061  esumsnf  33062  hasheuni  33083  rossros  33178  sibf0  33333  eulerpartlems  33359  eulerpartlemb  33367  ccatmulgnn0dir  33553  ofcccat  33554  plymulx0  33558  prodfzo03  33615  breprexp  33645  hgt750lemb  33668  hgt750leme  33670  lpadlem2  33692  derangsn  34161  onsucsuccmpi  35328  topdifinffinlem  36228  pibt2  36298  finixpnum  36473  lindsenlbs  36483  poimirlem26  36514  poimirlem27  36515  poimirlem31  36519  poimirlem32  36520  prdsbnd  36661  heiborlem3  36681  heiborlem8  36686  ismrer1  36706  reheibor  36707  pclfinN  38771  frlmvscadiccat  41080  frlmsnic  41110  selvvvval  41157  elrfi  41432  mzpcompact2lem  41489  dfac11  41804  pwslnmlem0  41833  lpirlnr  41859  mpct  43900  cnrefiisplem  44545  dvmptfprodlem  44660  dvnprodlem2  44663  stoweidlem44  44760  fourierdlem51  44873  fourierdlem80  44902  fouriersw  44947  salexct  45050  salexct3  45058  salgencntex  45059  salgensscntex  45060  sge0sn  45095  sge0tsms  45096  sge0cl  45097  sge0sup  45107  sge0iunmptlemfi  45129  sge0splitsn  45157  hoiprodp1  45304  sge0hsphoire  45305  hoidmv1le  45310  hoidmvlelem1  45311  hoidmvlelem2  45312  hoidmvlelem5  45315  hspmbllem2  45343  ovnovollem3  45374  vonvolmbl  45377  vonvol  45378  vonvol2  45380  fsummmodsnunz  46043  suppmptcfin  47055  lcosn0  47101  lincext2  47136  snlindsntor  47152