![]() |
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 7894 | . 2 ⊢ ∅ ∈ ω | |
2 | ssid 4002 | . 2 ⊢ ∅ ⊆ ∅ | |
3 | ssnnfi 9194 | . 2 ⊢ ((∅ ∈ ω ∧ ∅ ⊆ ∅) → ∅ ∈ Fin) | |
4 | 1, 2, 3 | mp2an 691 | 1 ⊢ ∅ ∈ Fin |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 ⊆ wss 3947 ∅c0 4323 ωcom 7870 Fincfn 8964 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-12 2167 ax-ext 2699 ax-sep 5299 ax-nul 5306 ax-pr 5429 ax-un 7740 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2530 df-clab 2706 df-cleq 2720 df-clel 2806 df-ne 2938 df-ral 3059 df-rex 3068 df-rab 3430 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-br 5149 df-opab 5211 df-tr 5266 df-id 5576 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5633 df-we 5635 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-ord 6372 df-on 6373 df-lim 6374 df-suc 6375 df-fun 6550 df-fn 6551 df-f 6552 df-f1 6553 df-fo 6554 df-f1o 6555 df-om 7871 df-en 8965 df-fin 8968 |
This theorem is referenced by: ssfi 9198 imafi 9200 cnvfi 9205 fnfi 9206 nneneq 9234 nfielex 9298 xpfiOLD 9343 iunfi 9365 fczfsuppd 9410 fsuppun 9411 0fsupp 9414 r1fin 9797 acndom 10075 numwdom 10083 ackbij1lem18 10261 sdom2en01 10326 fin23lem26 10349 isfin1-3 10410 gchxpidm 10693 fzfi 13970 fzofi 13972 hasheq0 14355 hashxp 14426 lcmf0 16605 0hashbc 16976 acsfn0 17640 isdrs2 18298 fpwipodrs 18532 symgfisg 19423 dsmm0cl 21674 mplsubg 21944 mpllss 21945 psrbag0 22006 mat0dimbas0 22381 mat0dim0 22382 mat0dimid 22383 mat0dimscm 22384 mat0dimcrng 22385 mat0scmat 22453 mavmul0 22467 mavmul0g 22468 mdet0pr 22507 m1detdiag 22512 d0mat2pmat 22653 chpmat0d 22749 fctop 22920 cmpfi 23325 bwth 23327 comppfsc 23449 ptbasid 23492 cfinfil 23810 ufinffr 23846 fin1aufil 23849 alexsubALTlem2 23965 alexsubALTlem4 23967 ptcmplem2 23970 tsmsfbas 24045 xrge0gsumle 24762 xrge0tsms 24763 fta1 26256 uhgr0edgfi 29066 fusgrfisbase 29154 vtxdg0e 29301 wwlksnfi 29730 mptiffisupp 32486 hashxpe 32589 xrge0tsmsd 32784 esumnul 33667 esum0 33668 esumcst 33682 esumsnf 33683 esumpcvgval 33697 sibf0 33954 eulerpartlemt 33991 derang0 34779 topdifinffinlem 36826 matunitlindf 37091 0totbnd 37246 heiborlem6 37289 mzpcompact2lem 42171 rp-isfinite6 42948 0pwfi 44423 fouriercn 45620 rrxtopn0 45681 salexct 45722 sge0rnn0 45756 sge00 45764 sge0sn 45767 ovn0val 45938 ovn02 45956 hoidmv0val 45971 hoidmvle 45988 hoiqssbl 46013 von0val 46059 vonhoire 46060 vonioo 46070 vonicc 46073 vonsn 46079 lcoc0 47490 lco0 47495 |
Copyright terms: Public domain | W3C validator |