Theorem snfi 8038

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 7719	. . . 4 ⊢ 1𝑜 ∈ ω
2		ensn1g 8021	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1𝑜)
3		breq2 4657	. . . . 5 ⊢ (𝑥 = 1𝑜 → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1𝑜))
4	3	rspcev 3309	. . . 4 ⊢ ((1𝑜 ∈ ω ∧ {𝐴} ≈ 1𝑜) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 695	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		snprc 4253	. . . 4 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
7		en0 8019	. . . . 5 ⊢ ({𝐴} ≈ ∅ ↔ {𝐴} = ∅)
8		peano1 7085	. . . . . 6 ⊢ ∅ ∈ ω
9		breq2 4657	. . . . . . 7 ⊢ (𝑥 = ∅ → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ ∅))
10	9	rspcev 3309	. . . . . 6 ⊢ ((∅ ∈ ω ∧ {𝐴} ≈ ∅) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
11	8, 10	mpan 706	. . . . 5 ⊢ ({𝐴} ≈ ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
12	7, 11	sylbir 225	. . . 4 ⊢ ({𝐴} = ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
13	6, 12	sylbi 207	. . 3 ⊢ (¬ 𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
14	5, 13	pm2.61i 176	. 2 ⊢ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥
15		isfi 7979	. 2 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
16	14, 15	mpbir 221	1 ⊢ {𝐴} ∈ Fin

Syntax hints:  ¬ wn 3   = wceq 1483   ∈ wcel 1990  ∃wrex 2913  Vcvv 3200  ∅c0 3915  {csn 4177   class class class wbr 4653  ωcom 7065  1_𝑜c1o 7553   ≈ cen 7952  Fincfn 7955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-om 7066  df-1o 7560  df-en 7956  df-fin 7959

This theorem is referenced by:  fiprc  8039  prfi  8235  tpfi  8236  fnfi  8238  unifpw  8269  snopfsupp  8298  sniffsupp  8315  ssfii  8325  cantnfp1lem1  8575  infpwfidom  8851  ackbij1lem4  9045  ackbij1lem9  9050  ackbij1lem10  9051  fin23lem21  9161  isfin1-3  9208  axcclem  9279  zornn0g  9327  hashsng  13159  hashen1  13160  hashunsng  13181  hashprg  13182  hashprgOLD  13183  hashsnlei  13206  hashxplem  13220  hashmap  13222  hashfun  13224  hashbclem  13236  hashf1lem1  13239  hashf1lem2  13240  hashf1  13241  fsumsplitsn  14474  fsummsnunz  14483  fsumsplitsnun  14484  fsummsnunzOLD  14485  fsumsplitsnunOLD  14486  fsum2dlem  14501  fsumcom2  14505  fsumcom2OLD  14506  ackbijnn  14560  incexclem  14568  isumltss  14580  fprod2dlem  14710  fprodcom2  14714  fprodcom2OLD  14715  fprodsplitsn  14720  rexpen  14957  2ebits  15169  lcmfunsnlem2lem1  15351  lcmfunsnlem2lem2  15352  lcmfunsnlem2  15353  lcmfass  15359  phicl2  15473  ramub1lem1  15730  cshwshashnsame  15810  acsfn1  16322  acsfiindd  17177  symg1hash  17815  odcau  18019  sylow2alem2  18033  gsumsnfd  18351  gsumzunsnd  18355  gsumunsnfd  18356  gsumpt  18361  ablfac1eu  18472  pgpfaclem2  18481  ablfaclem3  18486  srgbinomlem4  18543  psrlidm  19403  psrridm  19404  mplsubrg  19440  mvrcl  19449  mplmon  19463  mplmonmul  19464  psrbagsn  19495  psr1baslem  19555  uvcff  20130  mat1dimelbas  20277  mat1dim0  20279  mat1dimid  20280  mat1dimmul  20282  mat1dimcrng  20283  mat1f1o  20284  mat1ghm  20289  mat1mhm  20290  mat1rhm  20291  mat1rngiso  20292  mat1scmat  20345  mvmumamul1  20360  mdetrsca  20409  mdetunilem9  20426  mdetmul  20429  pmatcoe1fsupp  20506  d1mat2pmat  20544  pmatcollpw3fi1lem1  20591  chpmat1dlem  20640  chpmat1d  20641  0cmp  21197  discmp  21201  bwth  21213  disllycmp  21301  dis1stc  21302  locfincmp  21329  dissnlocfin  21332  comppfsc  21335  1stckgenlem  21356  ptpjpre2  21383  ptopn2  21387  xkohaus  21456  xkoptsub  21457  ptcmpfi  21616  cfinufil  21732  ufinffr  21733  fin1aufil  21736  alexsubALTlem3  21853  ptcmplem5  21860  tmdgsum  21899  tsmsxplem1  21956  tsmsxplem2  21957  prdsmet  22175  imasdsf1olem  22178  prdsbl  22296  icccmplem1  22625  icccmplem2  22626  ovolsn  23263  ovolfiniun  23269  volfiniun  23315  i1f0  23454  fta1glem2  23926  fta1blem  23928  fta1lem  24062  vieta1lem2  24066  vieta1  24067  aalioulem2  24088  tayl0  24116  radcnv0  24170  wilthlem2  24795  fsumvma  24938  dchrfi  24980  cusgrfilem3  26353  eupth2eucrct  27077  trlsegvdeglem7  27086  fusgreghash2wspv  27199  ex-hash  27310  ffsrn  29504  fsumiunle  29575  locfinref  29908  esumcst  30125  esumsnf  30126  hasheuni  30147  rossros  30243  sibf0  30396  eulerpartlems  30422  eulerpartlemb  30430  ccatmulgnn0dir  30619  ofcccat  30620  plymulx0  30624  prodfzo03  30681  breprexp  30711  hgt750lemb  30734  hgt750leme  30736  derangsn  31152  onsucsuccmpi  32442  topdifinffinlem  33195  finixpnum  33394  lindsenlbs  33404  poimirlem26  33435  poimirlem27  33436  poimirlem31  33440  poimirlem32  33441  prdsbnd  33592  heiborlem3  33612  heiborlem8  33617  ismrer1  33637  reheibor  33638  pclfinN  35186  elrfi  37257  mzpcompact2lem  37314  dfac11  37632  pwslnmlem0  37661  lpirlnr  37687  acsfn1p  37769  mpct  39393  cnrefiisplem  40055  dvmptfprodlem  40159  dvnprodlem2  40162  stoweidlem44  40261  fourierdlem51  40374  fourierdlem80  40403  fouriersw  40448  salexct  40552  salexct3  40560  salgencntex  40561  salgensscntex  40562  sge0sn  40596  sge0tsms  40597  sge0cl  40598  sge0sup  40608  sge0iunmptlemfi  40630  sge0splitsn  40658  hoiprodp1  40802  sge0hsphoire  40803  hoidmv1le  40808  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem5  40813  hspmbllem2  40841  ovnovollem3  40872  vonvolmbl  40875  vonvol  40876  vonvol2  40878  fsummmodsnunz  41345  suppmptcfin  42160  lcosn0  42209  lincext2  42244  snlindsntor  42260