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 7667 | . 2 ⊢ ∅ ∈ ω | |
2 | ssid 3923 | . 2 ⊢ ∅ ⊆ ∅ | |
3 | ssnnfi 8847 | . 2 ⊢ ((∅ ∈ ω ∧ ∅ ⊆ ∅) → ∅ ∈ Fin) | |
4 | 1, 2, 3 | mp2an 692 | 1 ⊢ ∅ ∈ Fin |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2110 ⊆ wss 3866 ∅c0 4237 ωcom 7644 Fincfn 8626 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-sep 5192 ax-nul 5199 ax-pr 5322 ax-un 7523 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ne 2941 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3410 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 df-pss 3885 df-nul 4238 df-if 4440 df-pw 4515 df-sn 4542 df-pr 4544 df-tp 4546 df-op 4548 df-uni 4820 df-br 5054 df-opab 5116 df-tr 5162 df-id 5455 df-eprel 5460 df-po 5468 df-so 5469 df-fr 5509 df-we 5511 df-xp 5557 df-rel 5558 df-cnv 5559 df-co 5560 df-dm 5561 df-rn 5562 df-ord 6216 df-on 6217 df-lim 6218 df-suc 6219 df-fun 6382 df-fn 6383 df-f 6384 df-f1 6385 df-fo 6386 df-f1o 6387 df-om 7645 df-en 8627 df-fin 8630 |
This theorem is referenced by: ssfi 8851 imafi 8853 cnvfi 8857 fnfi 8858 nfielex 8903 xpfi 8942 iunfi 8964 fczfsuppd 9003 fsuppun 9004 0fsupp 9007 r1fin 9389 acndom 9665 numwdom 9673 ackbij1lem18 9851 sdom2en01 9916 fin23lem26 9939 isfin1-3 10000 gchxpidm 10283 fzfi 13545 fzofi 13547 hasheq0 13930 hashxp 14001 lcmf0 16191 0hashbc 16560 acsfn0 17163 isdrs2 17813 fpwipodrs 18046 symgfisg 18860 dsmm0cl 20702 mplsubg 20964 mpllss 20965 psrbag0 21020 mat0dimbas0 21363 mat0dim0 21364 mat0dimid 21365 mat0dimscm 21366 mat0dimcrng 21367 mat0scmat 21435 mavmul0 21449 mavmul0g 21450 mdet0pr 21489 m1detdiag 21494 d0mat2pmat 21635 chpmat0d 21731 fctop 21901 cmpfi 22305 bwth 22307 comppfsc 22429 ptbasid 22472 cfinfil 22790 ufinffr 22826 fin1aufil 22829 alexsubALTlem2 22945 alexsubALTlem4 22947 ptcmplem2 22950 tsmsfbas 23025 xrge0gsumle 23730 xrge0tsms 23731 fta1 25201 uhgr0edgfi 27328 fusgrfisbase 27416 vtxdg0e 27562 wwlksnfi 27990 hashxpe 30847 xrge0tsmsd 31036 esumnul 31728 esum0 31729 esumcst 31743 esumsnf 31744 esumpcvgval 31758 sibf0 32013 eulerpartlemt 32050 derang0 32844 topdifinffinlem 35255 matunitlindf 35512 0totbnd 35668 heiborlem6 35711 mzpcompact2lem 40279 rp-isfinite6 40813 0pwfi 42283 fouriercn 43451 rrxtopn0 43512 salexct 43551 sge0rnn0 43584 sge00 43592 sge0sn 43595 ovn0val 43766 ovn02 43784 hoidmv0val 43799 hoidmvle 43816 hoiqssbl 43841 von0val 43887 vonhoire 43888 vonioo 43898 vonicc 43901 vonsn 43907 lcoc0 45439 lco0 45444 |
Copyright terms: Public domain | W3C validator |