Theorem snfi 8788

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 8432	. . . 4 ⊢ 1o ∈ ω
2		ensn1g 8763	. . . 4 ⊢ (𝐴 ∈ V → {𝐴} ≈ 1o)
3		breq2 5074	. . . . 5 ⊢ (𝑥 = 1o → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1o))
4	3	rspcev 3552	. . . 4 ⊢ ((1o ∈ ω ∧ {𝐴} ≈ 1o) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
5	1, 2, 4	sylancr 586	. . 3 ⊢ (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6		snprc 4650	. . . 4 ⊢ (¬ 𝐴 ∈ V ↔ {𝐴} = ∅)
7		en0 8758	. . . . 5 ⊢ ({𝐴} ≈ ∅ ↔ {𝐴} = ∅)
8		peano1 7710	. . . . . 6 ⊢ ∅ ∈ ω
9		breq2 5074	. . . . . . 7 ⊢ (𝑥 = ∅ → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ ∅))
10	9	rspcev 3552	. . . . . 6 ⊢ ((∅ ∈ ω ∧ {𝐴} ≈ ∅) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
11	8, 10	mpan 686	. . . . 5 ⊢ ({𝐴} ≈ ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
12	7, 11	sylbir 234	. . . 4 ⊢ ({𝐴} = ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
13	6, 12	sylbi 216	. . 3 ⊢ (¬ 𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
14	5, 13	pm2.61i 182	. 2 ⊢ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥
15		isfi 8719	. 2 ⊢ ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
16	14, 15	mpbir 230	1 ⊢ {𝐴} ∈ Fin

Syntax hints:  ¬ wn 3   = wceq 1539   ∈ wcel 2108  ∃wrex 3064  Vcvv 3422  ∅c0 4253  {csn 4558   class class class wbr 5070  ωcom 7687  1_oc1o 8260   ≈ cen 8688  Fincfn 8691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-om 7688  df-1o 8267  df-en 8692  df-fin 8695

This theorem is referenced by:  fiprc  8789  ssfi  8918  imafi  8920  pwfi  8923  cnvfi  8924  fnfi  8925  prfi  9019  tpfi  9020  unifpw  9052  snopfsupp  9081  sniffsupp  9089  ssfii  9108  cantnfp1lem1  9366  infpwfidom  9715  ficardadju  9886  ackbij1lem4  9910  ackbij1lem9  9915  ackbij1lem10  9916  fin23lem21  10026  isfin1-3  10073  axcclem  10144  zornn0g  10192  hashsng  14012  hashen1  14013  hashunsng  14035  hashunsngx  14036  hashprg  14038  hashsnlei  14061  hashxplem  14076  hashmap  14078  hashfun  14080  hashbclem  14092  hashf1lem1OLD  14097  hashf1lem2  14098  hashf1  14099  fsumsplitsn  15384  fsummsnunz  15394  fsumsplitsnun  15395  fsum2dlem  15410  fsumcom2  15414  ackbijnn  15468  incexclem  15476  isumltss  15488  fprod2dlem  15618  fprodcom2  15622  fprodsplitsn  15627  rexpen  15865  2ebits  16082  lcmfunsnlem2lem1  16271  lcmfunsnlem2lem2  16272  lcmfunsnlem2  16273  lcmfass  16279  phicl2  16397  ramub1lem1  16655  cshwshashnsame  16733  acsfn1  17287  acsfiindd  18186  efmnd1hash  18446  symg1hash  18912  odcau  19124  sylow2alem2  19138  gsumsnfd  19467  gsumzunsnd  19472  gsumunsnfd  19473  gsumpt  19478  ablfac1eu  19591  pgpfaclem2  19600  ablfaclem3  19605  srgbinomlem4  19694  acsfn1p  19982  uvcff  20908  psrlidm  21082  psrridm  21083  mplsubrg  21121  mvrcl  21131  mplmon  21146  mplmonmul  21147  psrbagsn  21181  psr1baslem  21266  mat1dimelbas  21528  mat1dim0  21530  mat1dimid  21531  mat1dimmul  21533  mat1dimcrng  21534  mat1f1o  21535  mat1ghm  21540  mat1mhm  21541  mat1rhm  21542  mat1rngiso  21543  mat1scmat  21596  mvmumamul1  21611  mdetrsca  21660  mdetunilem9  21677  mdetmul  21680  pmatcoe1fsupp  21758  d1mat2pmat  21796  pmatcollpw3fi1lem1  21843  chpmat1dlem  21892  chpmat1d  21893  0cmp  22453  discmp  22457  bwth  22469  disllycmp  22557  dis1stc  22558  locfincmp  22585  dissnlocfin  22588  comppfsc  22591  1stckgenlem  22612  ptpjpre2  22639  ptopn2  22643  xkohaus  22712  xkoptsub  22713  ptcmpfi  22872  cfinufil  22987  ufinffr  22988  fin1aufil  22991  alexsubALTlem3  23108  ptcmplem5  23115  tmdgsum  23154  tsmsxplem1  23212  tsmsxplem2  23213  prdsmet  23431  imasdsf1olem  23434  prdsbl  23553  icccmplem1  23891  icccmplem2  23892  ovolsn  24564  ovolfiniun  24570  volfiniun  24616  i1f0  24756  fta1glem2  25236  fta1blem  25238  fta1lem  25372  vieta1lem2  25376  vieta1  25377  aalioulem2  25398  tayl0  25426  radcnv0  25480  wilthlem2  26123  fsumvma  26266  dchrfi  26308  cusgrfilem3  27727  eupth2eucrct  28482  trlsegvdeglem7  28491  fusgreghash2wspv  28600  ex-hash  28718  fsupprnfi  30928  ffsrn  30966  fsumiunle  31045  fply1  31569  locfinref  31693  esumcst  31931  esumsnf  31932  hasheuni  31953  rossros  32048  sibf0  32201  eulerpartlems  32227  eulerpartlemb  32235  ccatmulgnn0dir  32421  ofcccat  32422  plymulx0  32426  prodfzo03  32483  breprexp  32513  hgt750lemb  32536  hgt750leme  32538  lpadlem2  32560  derangsn  33032  onsucsuccmpi  34559  topdifinffinlem  35445  pibt2  35515  finixpnum  35689  lindsenlbs  35699  poimirlem26  35730  poimirlem27  35731  poimirlem31  35735  poimirlem32  35736  prdsbnd  35878  heiborlem3  35898  heiborlem8  35903  ismrer1  35923  reheibor  35924  pclfinN  37841  frlmvscadiccat  40163  frlmsnic  40188  evlsbagval  40198  mhphf  40208  elrfi  40432  mzpcompact2lem  40489  dfac11  40803  pwslnmlem0  40832  lpirlnr  40858  mpct  42630  cnrefiisplem  43260  dvmptfprodlem  43375  dvnprodlem2  43378  stoweidlem44  43475  fourierdlem51  43588  fourierdlem80  43617  fouriersw  43662  salexct  43763  salexct3  43771  salgencntex  43772  salgensscntex  43773  sge0sn  43807  sge0tsms  43808  sge0cl  43809  sge0sup  43819  sge0iunmptlemfi  43841  sge0splitsn  43869  hoiprodp1  44016  sge0hsphoire  44017  hoidmv1le  44022  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem5  44027  hspmbllem2  44055  ovnovollem3  44086  vonvolmbl  44089  vonvol  44090  vonvol2  44092  fsummmodsnunz  44715  suppmptcfin  45603  lcosn0  45649  lincext2  45684  snlindsntor  45700