Theorem 0fi 8977

Description: The empty set is finite. (Contributed by FL, 14-Jul-2008.) Avoid ax-10 2146, ax-un 7678. (Revised by BTernaryTau, 13-Jan-2025.)

Assertion

Ref	Expression
0fi	⊢ ∅ ∈ Fin

Proof of Theorem 0fi

Step	Hyp	Ref	Expression
1		peano1 7829	. . 3 ⊢ ∅ ∈ ω
2		eqid 2734	. . . 4 ⊢ ∅ = ∅
3		en0 8953	. . . 4 ⊢ (∅ ≈ ∅ ↔ ∅ = ∅)
4	2, 3	mpbir 231	. . 3 ⊢ ∅ ≈ ∅
5		breq2 5100	. . . 4 ⊢ (𝑥 = ∅ → (∅ ≈ 𝑥 ↔ ∅ ≈ ∅))
6	5	rspcev 3574	. . 3 ⊢ ((∅ ∈ ω ∧ ∅ ≈ ∅) → ∃𝑥 ∈ ω ∅ ≈ 𝑥)
7	1, 4, 6	mp2an 692	. 2 ⊢ ∃𝑥 ∈ ω ∅ ≈ 𝑥
8		isfi 8910	. 2 ⊢ (∅ ∈ Fin ↔ ∃𝑥 ∈ ω ∅ ≈ 𝑥)
9	7, 8	mpbir 231	1 ⊢ ∅ ∈ Fin

Syntax hints:   = wceq 1541   ∈ wcel 2113  ∃wrex 3058  ∅c0 4283   class class class wbr 5096  ωcom 7806   ≈ cen 8878  Fincfn 8881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-mo 2537  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-ord 6318  df-on 6319  df-lim 6320  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-om 7807  df-en 8882  df-fin 8885

This theorem is referenced by:  snfi  8978  ssfi  9095  cnvfi  9098  fnfi  9100  nneneq  9128  nfielex  9172  imafiOLD  9214  fodomfib  9227  iunfi  9241  fczfsuppd  9287  fsuppun  9288  0fsupp  9291  r1fin  9683  acndom  9959  numwdom  9967  ackbij1lem18  10144  sdom2en01  10210  fin23lem26  10233  isfin1-3  10294  gchxpidm  10578  fzfi  13893  fzofi  13895  hasheq0  14284  hashxp  14355  lcmf0  16559  0hashbc  16933  acsfn0  17581  isdrs2  18227  fpwipodrs  18461  symgfisg  19395  dsmm0cl  21693  mplsubg  21955  mpllss  21956  psrbag0  22015  mat0dimbas0  22408  mat0dim0  22409  mat0dimid  22410  mat0dimscm  22411  mat0dimcrng  22412  mat0scmat  22480  mavmul0  22494  mavmul0g  22495  mdet0pr  22534  m1detdiag  22539  d0mat2pmat  22680  chpmat0d  22776  fctop  22946  cmpfi  23350  bwth  23352  comppfsc  23474  ptbasid  23517  cfinfil  23835  ufinffr  23871  fin1aufil  23874  alexsubALTlem2  23990  alexsubALTlem4  23992  ptcmplem2  23995  tsmsfbas  24070  xrge0gsumle  24776  xrge0tsms  24777  fta1  26270  uhgr0edgfi  29262  fusgrfisbase  29350  vtxdg0e  29497  wwlksnfi  29928  mptiffisupp  32721  hashxpe  32836  xrge0tsmsd  33104  elrgspnlem4  33276  extvfvcl  33650  vieta  33685  esumnul  34154  esum0  34155  esumcst  34169  esumsnf  34170  esumpcvgval  34184  sibf0  34440  eulerpartlemt  34477  derang0  35312  topdifinffinlem  37491  matunitlindf  37758  0totbnd  37913  heiborlem6  37956  mzpcompact2lem  42935  rp-isfinite6  43701  0pwfi  45246  fouriercn  46418  rrxtopn0  46479  salexct  46520  sge0rnn0  46554  sge00  46562  sge0sn  46565  ovn0val  46736  ovn02  46754  hoidmv0val  46769  hoidmvle  46786  hoiqssbl  46811  von0val  46857  vonhoire  46858  vonioo  46868  vonicc  46871  vonsn  46877  lcoc0  48610  lco0  48615