Theorem 0fin 8188

Description: The empty set is finite. (Contributed by FL, 14-Jul-2008.)

Assertion

Ref	Expression
0fin	|- (/) e. Fin

Proof of Theorem 0fin

Step	Hyp	Ref	Expression
1		peano1 7085	. 2 |- (/) e. om
2		ssid 3624	. 2 |- (/) C_ (/)
3		ssnnfi 8179	. 2 |- ( ( (/) e. om /\ (/) C_ (/) ) -> (/) e. Fin )
4	1, 2, 3	mp2an 708	1 |- (/) e. Fin

Syntax hints:   e. wcel 1990   C_ wss 3574   (/)c0 3915   omcom 7065   Fincfn 7955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-om 7066  df-en 7956  df-fin 7959

This theorem is referenced by:  nfielex  8189  xpfi  8231  fnfi  8238  iunfi  8254  fczfsuppd  8293  fsuppun  8294  0fsupp  8297  r1fin  8636  acndom  8874  numwdom  8882  ackbij1lem18  9059  sdom2en01  9124  fin23lem26  9147  isfin1-3  9208  gchxpidm  9491  fzfi  12771  fzofi  12773  hasheq0  13154  hashxp  13221  lcmf0  15347  0hashbc  15711  acsfn0  16321  isdrs2  16939  fpwipodrs  17164  symgfisg  17888  mplsubg  19437  mpllss  19438  psrbag0  19494  dsmm0cl  20084  mat0dimbas0  20272  mat0dim0  20273  mat0dimid  20274  mat0dimscm  20275  mat0dimcrng  20276  mat0scmat  20344  mavmul0  20358  mavmul0g  20359  mdet0pr  20398  m1detdiag  20403  d0mat2pmat  20543  chpmat0d  20639  fctop  20808  cmpfi  21211  bwth  21213  comppfsc  21335  ptbasid  21378  cfinfil  21697  ufinffr  21733  fin1aufil  21736  alexsubALTlem2  21852  alexsubALTlem4  21854  ptcmplem2  21857  tsmsfbas  21931  xrge0gsumle  22636  xrge0tsms  22637  fta1  24063  uhgr0edgfi  26132  fusgrfisbase  26220  vtxdg0e  26370  wwlksnfi  26801  wwlksnonfi  26816  clwwlksnfi  26913  numclwwlkffin0  27215  xrge0tsmsd  29785  esumnul  30110  esum0  30111  esumcst  30125  esumsnf  30126  esumpcvgval  30140  sibf0  30396  eulerpartlemt  30433  derang0  31151  topdifinffinlem  33195  matunitlindf  33407  0totbnd  33572  heiborlem6  33615  mzpcompact2lem  37314  rp-isfinite6  37864  0pwfi  39227  fouriercn  40449  rrxtopn0  40513  salexct  40552  sge0rnn0  40585  sge00  40593  sge0sn  40596  ovn0val  40764  ovn02  40782  hoidmv0val  40797  hoidmvle  40814  hoiqssbl  40839  von0val  40885  vonhoire  40886  vonioo  40896  vonicc  40899  vonsn  40905  lcoc0  42211  lco0  42216