Theorem 0fi 8982

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.)

Assertion

Ref	Expression
0fi	⊢ ∅ ∈ Fin

Proof of Theorem 0fi

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

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