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

Theorem 0fin 8849
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 7667 . 2 ∅ ∈ ω
2 ssid 3923 . 2 ∅ ⊆ ∅
3 ssnnfi 8847 . 2 ((∅ ∈ ω ∧ ∅ ⊆ ∅) → ∅ ∈ Fin)
41, 2, 3mp2an 692 1 ∅ ∈ Fin
Colors of variables: wff setvar class
Syntax hints:  wcel 2110  wss 3866  c0 4237  ωcom 7644  Fincfn 8626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322  ax-un 7523
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-om 7645  df-en 8627  df-fin 8630
This theorem is referenced by:  ssfi  8851  imafi  8853  cnvfi  8857  fnfi  8858  nfielex  8903  xpfi  8942  iunfi  8964  fczfsuppd  9003  fsuppun  9004  0fsupp  9007  r1fin  9389  acndom  9665  numwdom  9673  ackbij1lem18  9851  sdom2en01  9916  fin23lem26  9939  isfin1-3  10000  gchxpidm  10283  fzfi  13545  fzofi  13547  hasheq0  13930  hashxp  14001  lcmf0  16191  0hashbc  16560  acsfn0  17163  isdrs2  17813  fpwipodrs  18046  symgfisg  18860  dsmm0cl  20702  mplsubg  20964  mpllss  20965  psrbag0  21020  mat0dimbas0  21363  mat0dim0  21364  mat0dimid  21365  mat0dimscm  21366  mat0dimcrng  21367  mat0scmat  21435  mavmul0  21449  mavmul0g  21450  mdet0pr  21489  m1detdiag  21494  d0mat2pmat  21635  chpmat0d  21731  fctop  21901  cmpfi  22305  bwth  22307  comppfsc  22429  ptbasid  22472  cfinfil  22790  ufinffr  22826  fin1aufil  22829  alexsubALTlem2  22945  alexsubALTlem4  22947  ptcmplem2  22950  tsmsfbas  23025  xrge0gsumle  23730  xrge0tsms  23731  fta1  25201  uhgr0edgfi  27328  fusgrfisbase  27416  vtxdg0e  27562  wwlksnfi  27990  hashxpe  30847  xrge0tsmsd  31036  esumnul  31728  esum0  31729  esumcst  31743  esumsnf  31744  esumpcvgval  31758  sibf0  32013  eulerpartlemt  32050  derang0  32844  topdifinffinlem  35255  matunitlindf  35512  0totbnd  35668  heiborlem6  35711  mzpcompact2lem  40279  rp-isfinite6  40813  0pwfi  42283  fouriercn  43451  rrxtopn0  43512  salexct  43551  sge0rnn0  43584  sge00  43592  sge0sn  43595  ovn0val  43766  ovn02  43784  hoidmv0val  43799  hoidmvle  43816  hoiqssbl  43841  von0val  43887  vonhoire  43888  vonioo  43898  vonicc  43901  vonsn  43907  lcoc0  45439  lco0  45444
  Copyright terms: Public domain W3C validator