MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  snfi Structured version   Visualization version   GIF version

Theorem snfi 8280
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.
StepHypRef Expression
1 1onn 7959 . . . 4 1𝑜 ∈ ω
2 ensn1g 8260 . . . 4 (𝐴 ∈ V → {𝐴} ≈ 1𝑜)
3 breq2 4855 . . . . 5 (𝑥 = 1𝑜 → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ 1𝑜))
43rspcev 3509 . . . 4 ((1𝑜 ∈ ω ∧ {𝐴} ≈ 1𝑜) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
51, 2, 4sylancr 577 . . 3 (𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
6 snprc 4451 . . . 4 𝐴 ∈ V ↔ {𝐴} = ∅)
7 en0 8258 . . . . 5 ({𝐴} ≈ ∅ ↔ {𝐴} = ∅)
8 peano1 7318 . . . . . 6 ∅ ∈ ω
9 breq2 4855 . . . . . . 7 (𝑥 = ∅ → ({𝐴} ≈ 𝑥 ↔ {𝐴} ≈ ∅))
109rspcev 3509 . . . . . 6 ((∅ ∈ ω ∧ {𝐴} ≈ ∅) → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
118, 10mpan 673 . . . . 5 ({𝐴} ≈ ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
127, 11sylbir 226 . . . 4 ({𝐴} = ∅ → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
136, 12sylbi 208 . . 3 𝐴 ∈ V → ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
145, 13pm2.61i 176 . 2 𝑥 ∈ ω {𝐴} ≈ 𝑥
15 isfi 8219 . 2 ({𝐴} ∈ Fin ↔ ∃𝑥 ∈ ω {𝐴} ≈ 𝑥)
1614, 15mpbir 222 1 {𝐴} ∈ Fin
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1637  wcel 2157  wrex 3104  Vcvv 3398  c0 4123  {csn 4377   class class class wbr 4851  ωcom 7298  1𝑜c1o 7792  cen 8192  Fincfn 8195
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3400  df-sbc 3641  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-br 4852  df-opab 4914  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-ord 5946  df-on 5947  df-lim 5948  df-suc 5949  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-om 7299  df-1o 7799  df-en 8196  df-fin 8199
This theorem is referenced by:  fiprc  8281  prfi  8477  tpfi  8478  fnfi  8480  unifpw  8511  snopfsupp  8540  sniffsupp  8557  ssfii  8567  cantnfp1lem1  8825  infpwfidom  9137  ackbij1lem4  9333  ackbij1lem9  9338  ackbij1lem10  9339  fin23lem21  9449  isfin1-3  9496  axcclem  9567  zornn0g  9615  hashsng  13380  hashen1  13381  hashunsng  13402  hashprg  13403  hashsnlei  13426  hashxplem  13440  hashmap  13442  hashfun  13444  hashbclem  13456  hashf1lem1  13459  hashf1lem2  13460  hashf1  13461  fsumsplitsn  14700  fsummsnunz  14709  fsumsplitsnun  14710  fsummsnunzOLD  14711  fsumsplitsnunOLD  14712  fsum2dlem  14727  fsumcom2  14731  ackbijnn  14785  incexclem  14793  isumltss  14805  fprod2dlem  14934  fprodcom2  14938  fprodsplitsn  14943  rexpen  15180  2ebits  15391  lcmfunsnlem2lem1  15573  lcmfunsnlem2lem2  15574  lcmfunsnlem2  15575  lcmfass  15581  phicl2  15693  ramub1lem1  15950  cshwshashnsame  16025  acsfn1  16529  acsfiindd  17385  symg1hash  18019  odcau  18223  sylow2alem2  18237  gsumsnfd  18555  gsumzunsnd  18559  gsumunsnfd  18560  gsumpt  18565  ablfac1eu  18677  pgpfaclem2  18686  ablfaclem3  18691  srgbinomlem4  18748  psrlidm  19615  psrridm  19616  mplsubrg  19652  mvrcl  19661  mplmon  19675  mplmonmul  19676  psrbagsn  19706  psr1baslem  19766  uvcff  20344  mat1dimelbas  20492  mat1dim0  20494  mat1dimid  20495  mat1dimmul  20497  mat1dimcrng  20498  mat1f1o  20499  mat1ghm  20504  mat1mhm  20505  mat1rhm  20506  mat1rngiso  20507  mat1scmat  20560  mvmumamul1  20575  mdetrsca  20624  mdetunilem9  20641  mdetmul  20644  pmatcoe1fsupp  20723  d1mat2pmat  20761  pmatcollpw3fi1lem1  20808  chpmat1dlem  20857  chpmat1d  20858  0cmp  21415  discmp  21419  bwth  21431  disllycmp  21519  dis1stc  21520  locfincmp  21547  dissnlocfin  21550  comppfsc  21553  1stckgenlem  21574  ptpjpre2  21601  ptopn2  21605  xkohaus  21674  xkoptsub  21675  ptcmpfi  21834  cfinufil  21949  ufinffr  21950  fin1aufil  21953  alexsubALTlem3  22070  ptcmplem5  22077  tmdgsum  22116  tsmsxplem1  22173  tsmsxplem2  22174  prdsmet  22392  imasdsf1olem  22395  prdsbl  22513  icccmplem1  22842  icccmplem2  22843  ovolsn  23482  ovolfiniun  23488  volfiniun  23534  i1f0  23674  fta1glem2  24146  fta1blem  24148  fta1lem  24282  vieta1lem2  24286  vieta1  24287  aalioulem2  24308  tayl0  24336  radcnv0  24390  wilthlem2  25015  fsumvma  25158  dchrfi  25200  cusgrfilem3  26587  eupth2eucrct  27396  trlsegvdeglem7  27405  fusgreghash2wspv  27516  ex-hash  27647  ffsrn  29837  fsumiunle  29908  locfinref  30239  esumcst  30456  esumsnf  30457  hasheuni  30478  rossros  30574  sibf0  30727  eulerpartlems  30753  eulerpartlemb  30761  ccatmulgnn0dir  30950  ofcccat  30951  plymulx0  30955  prodfzo03  31012  breprexp  31042  hgt750lemb  31065  hgt750leme  31067  derangsn  31480  onsucsuccmpi  32764  topdifinffinlem  33513  finixpnum  33709  lindsenlbs  33719  poimirlem26  33750  poimirlem27  33751  poimirlem31  33755  poimirlem32  33756  prdsbnd  33905  heiborlem3  33925  heiborlem8  33930  ismrer1  33950  reheibor  33951  pclfinN  35682  elrfi  37760  mzpcompact2lem  37817  dfac11  38134  pwslnmlem0  38163  lpirlnr  38189  acsfn1p  38271  mpct  39881  cnrefiisplem  40536  dvmptfprodlem  40640  dvnprodlem2  40643  stoweidlem44  40741  fourierdlem51  40854  fourierdlem80  40883  fouriersw  40928  salexct  41032  salexct3  41040  salgencntex  41041  salgensscntex  41042  sge0sn  41076  sge0tsms  41077  sge0cl  41078  sge0sup  41088  sge0iunmptlemfi  41110  sge0splitsn  41138  hoiprodp1  41285  sge0hsphoire  41286  hoidmv1le  41291  hoidmvlelem1  41292  hoidmvlelem2  41293  hoidmvlelem5  41296  hspmbllem2  41324  ovnovollem3  41355  vonvolmbl  41358  vonvol  41359  vonvol2  41361  fsummmodsnunz  41921  suppmptcfin  42729  lcosn0  42778  lincext2  42813  snlindsntor  42829
  Copyright terms: Public domain W3C validator