Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 0fin | Structured version Visualization version GIF version |
Description: The empty set is finite. (Contributed by FL, 14-Jul-2008.) |
Ref | Expression |
---|---|
0fin | ⊢ ∅ ∈ Fin |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | peano1 7589 | . 2 ⊢ ∅ ∈ ω | |
2 | ssid 3988 | . 2 ⊢ ∅ ⊆ ∅ | |
3 | ssnnfi 8726 | . 2 ⊢ ((∅ ∈ ω ∧ ∅ ⊆ ∅) → ∅ ∈ Fin) | |
4 | 1, 2, 3 | mp2an 688 | 1 ⊢ ∅ ∈ Fin |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 ⊆ wss 3935 ∅c0 4290 ωcom 7568 Fincfn 8498 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7450 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3or 1080 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3497 df-sbc 3772 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4466 df-pw 4539 df-sn 4560 df-pr 4562 df-tp 4564 df-op 4566 df-uni 4833 df-br 5059 df-opab 5121 df-tr 5165 df-id 5454 df-eprel 5459 df-po 5468 df-so 5469 df-fr 5508 df-we 5510 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-ord 6188 df-on 6189 df-lim 6190 df-suc 6191 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-om 7569 df-en 8499 df-fin 8502 |
This theorem is referenced by: nfielex 8736 xpfi 8778 fnfi 8785 iunfi 8801 fczfsuppd 8840 fsuppun 8841 0fsupp 8844 r1fin 9191 acndom 9466 numwdom 9474 ackbij1lem18 9648 sdom2en01 9713 fin23lem26 9736 isfin1-3 9797 gchxpidm 10080 fzfi 13330 fzofi 13332 hasheq0 13714 hashxp 13785 lcmf0 15968 0hashbc 16333 acsfn0 16921 isdrs2 17539 fpwipodrs 17764 symgfisg 18527 mplsubg 20147 mpllss 20148 psrbag0 20204 dsmm0cl 20814 mat0dimbas0 21005 mat0dim0 21006 mat0dimid 21007 mat0dimscm 21008 mat0dimcrng 21009 mat0scmat 21077 mavmul0 21091 mavmul0g 21092 mdet0pr 21131 m1detdiag 21136 d0mat2pmat 21276 chpmat0d 21372 fctop 21542 cmpfi 21946 bwth 21948 comppfsc 22070 ptbasid 22113 cfinfil 22431 ufinffr 22467 fin1aufil 22470 alexsubALTlem2 22586 alexsubALTlem4 22588 ptcmplem2 22591 tsmsfbas 22665 xrge0gsumle 23370 xrge0tsms 23371 fta1 24826 uhgr0edgfi 26950 fusgrfisbase 27038 vtxdg0e 27184 wwlksnfi 27612 wwlksnfiOLD 27613 clwwlknfiOLD 27752 hashxpe 30456 xrge0tsmsd 30620 esumnul 31207 esum0 31208 esumcst 31222 esumsnf 31223 esumpcvgval 31237 sibf0 31492 eulerpartlemt 31529 derang0 32314 topdifinffinlem 34511 matunitlindf 34772 0totbnd 34934 heiborlem6 34977 mzpcompact2lem 39228 rp-isfinite6 39764 0pwfi 41201 fouriercn 42398 rrxtopn0 42459 salexct 42498 sge0rnn0 42531 sge00 42539 sge0sn 42542 ovn0val 42713 ovn02 42731 hoidmv0val 42746 hoidmvle 42763 hoiqssbl 42788 von0val 42834 vonhoire 42835 vonioo 42845 vonicc 42848 vonsn 42854 lcoc0 44375 lco0 44380 |
Copyright terms: Public domain | W3C validator |