![]() |
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 7319 | . 2 ⊢ ∅ ∈ ω | |
2 | ssid 3819 | . 2 ⊢ ∅ ⊆ ∅ | |
3 | ssnnfi 8421 | . 2 ⊢ ((∅ ∈ ω ∧ ∅ ⊆ ∅) → ∅ ∈ Fin) | |
4 | 1, 2, 3 | mp2an 684 | 1 ⊢ ∅ ∈ Fin |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2157 ⊆ wss 3769 ∅c0 4115 ωcom 7299 Fincfn 8195 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-sep 4975 ax-nul 4983 ax-pow 5035 ax-pr 5097 ax-un 7183 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3or 1109 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ne 2972 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3387 df-sbc 3634 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-pss 3785 df-nul 4116 df-if 4278 df-pw 4351 df-sn 4369 df-pr 4371 df-tp 4373 df-op 4375 df-uni 4629 df-br 4844 df-opab 4906 df-tr 4946 df-id 5220 df-eprel 5225 df-po 5233 df-so 5234 df-fr 5271 df-we 5273 df-xp 5318 df-rel 5319 df-cnv 5320 df-co 5321 df-dm 5322 df-rn 5323 df-res 5324 df-ima 5325 df-ord 5944 df-on 5945 df-lim 5946 df-suc 5947 df-fun 6103 df-fn 6104 df-f 6105 df-f1 6106 df-fo 6107 df-f1o 6108 df-om 7300 df-en 8196 df-fin 8199 |
This theorem is referenced by: nfielex 8431 xpfi 8473 fnfi 8480 iunfi 8496 fczfsuppd 8535 fsuppun 8536 0fsupp 8539 r1fin 8886 acndom 9160 numwdom 9168 ackbij1lem18 9347 sdom2en01 9412 fin23lem26 9435 isfin1-3 9496 gchxpidm 9779 fzfi 13026 fzofi 13028 hasheq0 13404 hashxp 13470 lcmf0 15682 0hashbc 16044 acsfn0 16635 isdrs2 17254 fpwipodrs 17479 symgfisg 18200 mplsubg 19760 mpllss 19761 psrbag0 19816 dsmm0cl 20409 mat0dimbas0 20598 mat0dim0 20599 mat0dimid 20600 mat0dimscm 20601 mat0dimcrng 20602 mat0scmat 20670 mavmul0 20684 mavmul0g 20685 mdet0pr 20724 m1detdiag 20729 d0mat2pmat 20871 chpmat0d 20967 fctop 21137 cmpfi 21540 bwth 21542 comppfsc 21664 ptbasid 21707 cfinfil 22025 ufinffr 22061 fin1aufil 22064 alexsubALTlem2 22180 alexsubALTlem4 22182 ptcmplem2 22185 tsmsfbas 22259 xrge0gsumle 22964 xrge0tsms 22965 fta1 24404 uhgr0edgfi 26474 fusgrfisbase 26562 vtxdg0e 26724 wwlksnfi 27186 clwwlknfi 27354 xrge0tsmsd 30301 esumnul 30626 esum0 30627 esumcst 30641 esumsnf 30642 esumpcvgval 30656 sibf0 30912 eulerpartlemt 30949 derang0 31668 topdifinffinlem 33693 matunitlindf 33896 0totbnd 34059 heiborlem6 34102 mzpcompact2lem 38096 rp-isfinite6 38643 0pwfi 39982 fouriercn 41188 rrxtopn0 41252 salexct 41291 sge0rnn0 41324 sge00 41332 sge0sn 41335 ovn0val 41506 ovn02 41524 hoidmv0val 41539 hoidmvle 41556 hoiqssbl 41581 von0val 41627 vonhoire 41628 vonioo 41638 vonicc 41641 vonsn 41647 lcoc0 43006 lco0 43011 |
Copyright terms: Public domain | W3C validator |