| 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 7682. (Revised by BTernaryTau, 13-Jan-2025.) |
| Ref | Expression |
|---|---|
| 0fi | ⊢ ∅ ∈ Fin |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | peano1 7833 | . . 3 ⊢ ∅ ∈ ω | |
| 2 | eqid 2737 | . . . 4 ⊢ ∅ = ∅ | |
| 3 | en0 8958 | . . . 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 8915 | . 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 7810 ≈ cen 8883 Fincfn 8886 |
| 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 5231 ax-nul 5241 ax-pr 5370 |
| 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 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-ord 6320 df-on 6321 df-lim 6322 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-om 7811 df-en 8887 df-fin 8890 |
| This theorem is referenced by: snfi 8983 ssfi 9100 cnvfi 9103 fnfi 9105 nneneq 9133 nfielex 9177 imafiOLD 9219 fodomfib 9232 iunfi 9246 fczfsuppd 9292 fsuppun 9293 0fsupp 9296 r1fin 9688 acndom 9964 numwdom 9972 ackbij1lem18 10149 sdom2en01 10215 fin23lem26 10238 isfin1-3 10299 gchxpidm 10583 fzfi 13925 fzofi 13927 hasheq0 14316 hashxp 14387 lcmf0 16594 0hashbc 16969 acsfn0 17617 isdrs2 18263 fpwipodrs 18497 symgfisg 19434 dsmm0cl 21730 mplsubg 21990 mpllss 21991 psrbag0 22050 mat0dimbas0 22441 mat0dim0 22442 mat0dimid 22443 mat0dimscm 22444 mat0dimcrng 22445 mat0scmat 22513 mavmul0 22527 mavmul0g 22528 mdet0pr 22567 m1detdiag 22572 d0mat2pmat 22713 chpmat0d 22809 fctop 22979 cmpfi 23383 bwth 23385 comppfsc 23507 ptbasid 23550 cfinfil 23868 ufinffr 23904 fin1aufil 23907 alexsubALTlem2 24023 alexsubALTlem4 24025 ptcmplem2 24028 tsmsfbas 24103 xrge0gsumle 24809 xrge0tsms 24810 fta1 26285 uhgr0edgfi 29323 fusgrfisbase 29411 vtxdg0e 29558 wwlksnfi 29989 mptiffisupp 32781 hashxpe 32895 xrge0tsmsd 33149 elrgspnlem4 33321 extvfvcl 33695 vieta 33739 esumnul 34208 esum0 34209 esumcst 34223 esumsnf 34224 esumpcvgval 34238 sibf0 34494 eulerpartlemt 34531 derang0 35367 topdifinffinlem 37677 matunitlindf 37953 0totbnd 38108 heiborlem6 38151 mzpcompact2lem 43197 rp-isfinite6 43963 0pwfi 45508 fouriercn 46678 rrxtopn0 46739 salexct 46780 sge0rnn0 46814 sge00 46822 sge0sn 46825 ovn0val 46996 ovn02 47014 hoidmv0val 47029 hoidmvle 47046 hoiqssbl 47071 von0val 47117 vonhoire 47118 vonioo 47128 vonicc 47131 vonsn 47137 lcoc0 48910 lco0 48915 |
| Copyright terms: Public domain | W3C validator |