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 7601 | . 2 ⊢ ∅ ∈ ω | |
2 | ssid 3989 | . 2 ⊢ ∅ ⊆ ∅ | |
3 | ssnnfi 8737 | . 2 ⊢ ((∅ ∈ ω ∧ ∅ ⊆ ∅) → ∅ ∈ Fin) | |
4 | 1, 2, 3 | mp2an 690 | 1 ⊢ ∅ ∈ Fin |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2114 ⊆ wss 3936 ∅c0 4291 ωcom 7580 Fincfn 8509 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 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 3496 df-sbc 3773 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-br 5067 df-opab 5129 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-om 7581 df-en 8510 df-fin 8513 |
This theorem is referenced by: nfielex 8747 xpfi 8789 fnfi 8796 iunfi 8812 fczfsuppd 8851 fsuppun 8852 0fsupp 8855 r1fin 9202 acndom 9477 numwdom 9485 ackbij1lem18 9659 sdom2en01 9724 fin23lem26 9747 isfin1-3 9808 gchxpidm 10091 fzfi 13341 fzofi 13343 hasheq0 13725 hashxp 13796 lcmf0 15978 0hashbc 16343 acsfn0 16931 isdrs2 17549 fpwipodrs 17774 symgfisg 18596 mplsubg 20217 mpllss 20218 psrbag0 20274 dsmm0cl 20884 mat0dimbas0 21075 mat0dim0 21076 mat0dimid 21077 mat0dimscm 21078 mat0dimcrng 21079 mat0scmat 21147 mavmul0 21161 mavmul0g 21162 mdet0pr 21201 m1detdiag 21206 d0mat2pmat 21346 chpmat0d 21442 fctop 21612 cmpfi 22016 bwth 22018 comppfsc 22140 ptbasid 22183 cfinfil 22501 ufinffr 22537 fin1aufil 22540 alexsubALTlem2 22656 alexsubALTlem4 22658 ptcmplem2 22661 tsmsfbas 22736 xrge0gsumle 23441 xrge0tsms 23442 fta1 24897 uhgr0edgfi 27022 fusgrfisbase 27110 vtxdg0e 27256 wwlksnfi 27684 wwlksnfiOLD 27685 clwwlknfiOLD 27824 hashxpe 30529 xrge0tsmsd 30692 esumnul 31307 esum0 31308 esumcst 31322 esumsnf 31323 esumpcvgval 31337 sibf0 31592 eulerpartlemt 31629 derang0 32416 topdifinffinlem 34631 matunitlindf 34905 0totbnd 35066 heiborlem6 35109 mzpcompact2lem 39368 rp-isfinite6 39904 0pwfi 41341 fouriercn 42537 rrxtopn0 42598 salexct 42637 sge0rnn0 42670 sge00 42678 sge0sn 42681 ovn0val 42852 ovn02 42870 hoidmv0val 42885 hoidmvle 42902 hoiqssbl 42927 von0val 42973 vonhoire 42974 vonioo 42984 vonicc 42987 vonsn 42993 lcoc0 44497 lco0 44502 |
Copyright terms: Public domain | W3C validator |