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

Theorem 0fin 8749
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 7604 . 2 ∅ ∈ ω
2 ssid 3992 . 2 ∅ ⊆ ∅
3 ssnnfi 8740 . 2 ((∅ ∈ ω ∧ ∅ ⊆ ∅) → ∅ ∈ Fin)
41, 2, 3mp2an 690 1 ∅ ∈ Fin
Colors of variables: wff setvar class
Syntax hints:  wcel 2113  wss 3939  c0 4294  ωcom 7583  Fincfn 8512
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-tp 4575  df-op 4577  df-uni 4842  df-br 5070  df-opab 5132  df-tr 5176  df-id 5463  df-eprel 5468  df-po 5477  df-so 5478  df-fr 5517  df-we 5519  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-ord 6197  df-on 6198  df-lim 6199  df-suc 6200  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-om 7584  df-en 8513  df-fin 8516
This theorem is referenced by:  nfielex  8750  xpfi  8792  fnfi  8799  iunfi  8815  fczfsuppd  8854  fsuppun  8855  0fsupp  8858  r1fin  9205  acndom  9480  numwdom  9488  ackbij1lem18  9662  sdom2en01  9727  fin23lem26  9750  isfin1-3  9811  gchxpidm  10094  fzfi  13343  fzofi  13345  hasheq0  13727  hashxp  13798  lcmf0  15981  0hashbc  16346  acsfn0  16934  isdrs2  17552  fpwipodrs  17777  symgfisg  18599  mplsubg  20220  mpllss  20221  psrbag0  20277  dsmm0cl  20887  mat0dimbas0  21078  mat0dim0  21079  mat0dimid  21080  mat0dimscm  21081  mat0dimcrng  21082  mat0scmat  21150  mavmul0  21164  mavmul0g  21165  mdet0pr  21204  m1detdiag  21209  d0mat2pmat  21349  chpmat0d  21445  fctop  21615  cmpfi  22019  bwth  22021  comppfsc  22143  ptbasid  22186  cfinfil  22504  ufinffr  22540  fin1aufil  22543  alexsubALTlem2  22659  alexsubALTlem4  22661  ptcmplem2  22664  tsmsfbas  22739  xrge0gsumle  23444  xrge0tsms  23445  fta1  24900  uhgr0edgfi  27025  fusgrfisbase  27113  vtxdg0e  27259  wwlksnfi  27687  wwlksnfiOLD  27688  clwwlknfiOLD  27827  hashxpe  30532  xrge0tsmsd  30696  esumnul  31311  esum0  31312  esumcst  31326  esumsnf  31327  esumpcvgval  31341  sibf0  31596  eulerpartlemt  31633  derang0  32420  topdifinffinlem  34632  matunitlindf  34894  0totbnd  35055  heiborlem6  35098  mzpcompact2lem  39354  rp-isfinite6  39890  0pwfi  41327  fouriercn  42524  rrxtopn0  42585  salexct  42624  sge0rnn0  42657  sge00  42665  sge0sn  42668  ovn0val  42839  ovn02  42857  hoidmv0val  42872  hoidmvle  42889  hoiqssbl  42914  von0val  42960  vonhoire  42961  vonioo  42971  vonicc  42974  vonsn  42980  lcoc0  44484  lco0  44489
  Copyright terms: Public domain W3C validator