Theorem 0fi 8983

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

Assertion

Ref	Expression
0fi	⊢ ∅ ∈ Fin

Proof of Theorem 0fi

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

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