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

Theorem 0fin 8140
Description: The empty set is finite. (Contributed by FL, 14-Jul-2008.)
Assertion
Ref Expression
0fin ∅ ∈ Fin

Proof of Theorem 0fin
StepHypRef Expression
1 peano1 7039 . 2 ∅ ∈ ω
2 ssid 3608 . 2 ∅ ⊆ ∅
3 ssnnfi 8131 . 2 ((∅ ∈ ω ∧ ∅ ⊆ ∅) → ∅ ∈ Fin)
41, 2, 3mp2an 707 1 ∅ ∈ Fin
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  wss 3559  c0 3896  ωcom 7019  Fincfn 7907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-om 7020  df-en 7908  df-fin 7911
This theorem is referenced by:  nfielex  8141  xpfi  8183  fnfi  8190  iunfi  8206  fczfsuppd  8245  fsuppun  8246  0fsupp  8249  r1fin  8588  acndom  8826  numwdom  8834  ackbij1lem18  9011  sdom2en01  9076  fin23lem26  9099  isfin1-3  9160  gchxpidm  9443  fzfi  12719  fzofi  12721  hasheq0  13102  hashxp  13169  lcmf0  15282  0hashbc  15646  acsfn0  16253  isdrs2  16871  fpwipodrs  17096  symgfisg  17820  mplsubg  19369  mpllss  19370  psrbag0  19426  dsmm0cl  20016  mat0dimbas0  20204  mat0dim0  20205  mat0dimid  20206  mat0dimscm  20207  mat0dimcrng  20208  mat0scmat  20276  mavmul0  20290  mavmul0g  20291  mdet0pr  20330  m1detdiag  20335  d0mat2pmat  20475  chpmat0d  20571  fctop  20731  cmpfi  21134  bwth  21136  comppfsc  21258  ptbasid  21301  cfinfil  21620  ufinffr  21656  fin1aufil  21659  alexsubALTlem2  21775  alexsubALTlem4  21777  ptcmplem2  21780  tsmsfbas  21854  xrge0gsumle  22559  xrge0tsms  22560  fta1  23984  uhgr0edgfi  26042  fusgrfisbase  26125  vtxdg0e  26273  wwlksnfi  26687  wwlksnonfi  26702  clwwlksnfi  26796  numclwwlkffin0  27088  xrge0tsmsd  29594  esumnul  29915  esum0  29916  esumcst  29930  esumsnf  29931  esumpcvgval  29945  sibf0  30201  eulerpartlemt  30238  derang0  30894  topdifinffinlem  32862  matunitlindf  33074  0totbnd  33239  heiborlem6  33282  mzpcompact2lem  36829  rp-isfinite6  37380  0pwfi  38745  fouriercn  39782  rrxtopn0  39846  salexct  39885  sge0rnn0  39918  sge00  39926  sge0sn  39929  ovn0val  40097  ovn02  40115  hoidmv0val  40130  hoidmvle  40147  hoiqssbl  40172  von0val  40218  vonhoire  40219  vonioo  40229  vonicc  40232  vonsn  40238  lcoc0  41525  lco0  41530
  Copyright terms: Public domain W3C validator