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

Theorem 0fin 8073
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 6977 . 2 ∅ ∈ ω
2 ssid 3587 . 2 ∅ ⊆ ∅
3 ssnnfi 8064 . 2 ((∅ ∈ ω ∧ ∅ ⊆ ∅) → ∅ ∈ Fin)
41, 2, 3mp2an 704 1 ∅ ∈ Fin
Colors of variables: wff setvar class
Syntax hints:  wcel 1977  wss 3540  c0 3874  ωcom 6957  Fincfn 7841
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-om 6958  df-en 7842  df-fin 7845
This theorem is referenced by:  nfielex  8074  xpfi  8116  fnfi  8123  iunfi  8137  fczfsuppd  8176  fsuppun  8177  0fsupp  8180  r1fin  8519  acndom  8757  numwdom  8765  ackbij1lem18  8942  sdom2en01  9007  fin23lem26  9030  isfin1-3  9091  gchxpidm  9370  fzfi  12633  fzofi  12635  hasheq0  13015  hashxp  13081  lcmf0  15185  0hashbc  15549  acsfn0  16144  isdrs2  16762  fpwipodrs  16987  symgfisg  17711  mplsubg  19258  mpllss  19259  psrbag0  19315  dsmm0cl  19903  mat0dimbas0  20091  mat0dim0  20092  mat0dimid  20093  mat0dimscm  20094  mat0dimcrng  20095  mat0scmat  20163  mavmul0  20177  mavmul0g  20178  mdet0pr  20217  m1detdiag  20222  d0mat2pmat  20362  chpmat0d  20458  fctop  20618  cmpfi  21021  bwth  21023  comppfsc  21145  ptbasid  21188  cfinfil  21507  ufinffr  21543  fin1aufil  21546  alexsubALTlem2  21662  alexsubALTlem4  21664  ptcmplem2  21667  tsmsfbas  21741  xrge0gsumle  22444  xrge0tsms  22445  fta1  23867  wwlknfi  26266  xrge0tsmsd  29116  esumnul  29437  esum0  29438  esumcst  29452  esumsnf  29453  esumpcvgval  29467  sibf0  29723  eulerpartlemt  29760  derang0  30405  topdifinffinlem  32371  matunitlindf  32577  0totbnd  32742  heiborlem6  32785  mzpcompact2lem  36332  rp-isfinite6  36883  0pwfi  38252  fouriercn  39125  rrxtopn0  39189  salexct  39228  sge0rnn0  39261  sge00  39269  sge0sn  39272  ovn0val  39440  ovn02  39458  hoidmv0val  39473  hoidmvle  39490  hoiqssbl  39515  von0val  39562  vonhoire  39563  vonioo  39573  vonicc  39576  vonsn  39582  uhgr0edgfi  40466  fusgrfisbase  40547  vtxdg0e  40689  wwlksnfi  41112  wwlksnonfi  41127  clwwlksnfi  41220  av-numclwwlkffin0  41513  lcoc0  42005  lco0  42010
  Copyright terms: Public domain W3C validator