| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 0fi | Structured version Visualization version GIF version | ||
| Description: The empty set is finite. (Contributed by FL, 14-Jul-2008.) Avoid ax-10 2147, ax-un 7683. (Revised by BTernaryTau, 13-Jan-2025.) |
| Ref | Expression |
|---|---|
| 0fi | ⊢ ∅ ∈ Fin |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | peano1 7834 | . . 3 ⊢ ∅ ∈ ω | |
| 2 | eqid 2737 | . . . 4 ⊢ ∅ = ∅ | |
| 3 | en0 8959 | . . . 4 ⊢ (∅ ≈ ∅ ↔ ∅ = ∅) | |
| 4 | 2, 3 | mpbir 231 | . . 3 ⊢ ∅ ≈ ∅ |
| 5 | breq2 5090 | . . . 4 ⊢ (𝑥 = ∅ → (∅ ≈ 𝑥 ↔ ∅ ≈ ∅)) | |
| 6 | 5 | rspcev 3565 | . . 3 ⊢ ((∅ ∈ ω ∧ ∅ ≈ ∅) → ∃𝑥 ∈ ω ∅ ≈ 𝑥) |
| 7 | 1, 4, 6 | mp2an 693 | . 2 ⊢ ∃𝑥 ∈ ω ∅ ≈ 𝑥 |
| 8 | isfi 8916 | . 2 ⊢ (∅ ∈ Fin ↔ ∃𝑥 ∈ ω ∅ ≈ 𝑥) | |
| 9 | 7, 8 | mpbir 231 | 1 ⊢ ∅ ∈ Fin |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1542 ∈ wcel 2114 ∃wrex 3062 ∅c0 4274 class class class wbr 5086 ωcom 7811 ≈ cen 8884 Fincfn 8887 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-ext 2709 ax-sep 5232 ax-nul 5242 ax-pr 5371 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-sb 2069 df-mo 2540 df-clab 2716 df-cleq 2729 df-clel 2812 df-ne 2934 df-ral 3053 df-rex 3063 df-rab 3391 df-v 3432 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-br 5087 df-opab 5149 df-tr 5194 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-ord 6321 df-on 6322 df-lim 6323 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-om 7812 df-en 8888 df-fin 8891 |
| This theorem is referenced by: snfi 8984 ssfi 9101 cnvfi 9104 fnfi 9106 nneneq 9134 nfielex 9178 imafiOLD 9220 fodomfib 9233 iunfi 9247 fczfsuppd 9293 fsuppun 9294 0fsupp 9297 r1fin 9691 acndom 9967 numwdom 9975 ackbij1lem18 10152 sdom2en01 10218 fin23lem26 10241 isfin1-3 10302 gchxpidm 10586 fzfi 13928 fzofi 13930 hasheq0 14319 hashxp 14390 lcmf0 16597 0hashbc 16972 acsfn0 17620 isdrs2 18266 fpwipodrs 18500 symgfisg 19437 dsmm0cl 21733 mplsubg 21993 mpllss 21994 psrbag0 22053 mat0dimbas0 22444 mat0dim0 22445 mat0dimid 22446 mat0dimscm 22447 mat0dimcrng 22448 mat0scmat 22516 mavmul0 22530 mavmul0g 22531 mdet0pr 22570 m1detdiag 22575 d0mat2pmat 22716 chpmat0d 22812 fctop 22982 cmpfi 23386 bwth 23388 comppfsc 23510 ptbasid 23553 cfinfil 23871 ufinffr 23907 fin1aufil 23910 alexsubALTlem2 24026 alexsubALTlem4 24028 ptcmplem2 24031 tsmsfbas 24106 xrge0gsumle 24812 xrge0tsms 24813 fta1 26288 uhgr0edgfi 29326 fusgrfisbase 29414 vtxdg0e 29561 wwlksnfi 29992 mptiffisupp 32784 hashxpe 32898 xrge0tsmsd 33152 elrgspnlem4 33324 extvfvcl 33698 vieta 33742 esumnul 34211 esum0 34212 esumcst 34226 esumsnf 34227 esumpcvgval 34241 sibf0 34497 eulerpartlemt 34534 derang0 35370 topdifinffinlem 37680 matunitlindf 37956 0totbnd 38111 heiborlem6 38154 mzpcompact2lem 43200 rp-isfinite6 43966 0pwfi 45511 fouriercn 46681 rrxtopn0 46742 salexct 46783 sge0rnn0 46817 sge00 46825 sge0sn 46828 ovn0val 46999 ovn02 47017 hoidmv0val 47032 hoidmvle 47049 hoiqssbl 47074 von0val 47120 vonhoire 47121 vonioo 47131 vonicc 47134 vonsn 47140 lcoc0 48913 lco0 48918 |
| Copyright terms: Public domain | W3C validator |