Theorem 0fi 9016

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

Assertion

Ref	Expression
0fi	⊢ ∅ ∈ Fin

Proof of Theorem 0fi

Step	Hyp	Ref	Expression
1		peano1 7868	. . 3 ⊢ ∅ ∈ ω
2		eqid 2730	. . . 4 ⊢ ∅ = ∅
3		en0 8992	. . . 4 ⊢ (∅ ≈ ∅ ↔ ∅ = ∅)
4	2, 3	mpbir 231	. . 3 ⊢ ∅ ≈ ∅
5		breq2 5114	. . . 4 ⊢ (𝑥 = ∅ → (∅ ≈ 𝑥 ↔ ∅ ≈ ∅))
6	5	rspcev 3591	. . 3 ⊢ ((∅ ∈ ω ∧ ∅ ≈ ∅) → ∃𝑥 ∈ ω ∅ ≈ 𝑥)
7	1, 4, 6	mp2an 692	. 2 ⊢ ∃𝑥 ∈ ω ∅ ≈ 𝑥
8		isfi 8950	. 2 ⊢ (∅ ∈ Fin ↔ ∃𝑥 ∈ ω ∅ ≈ 𝑥)
9	7, 8	mpbir 231	1 ⊢ ∅ ∈ Fin

Syntax hints:   = wceq 1540   ∈ wcel 2109  ∃wrex 3054  ∅c0 4299   class class class wbr 5110  ωcom 7845   ≈ cen 8918  Fincfn 8921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-mo 2534  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-ord 6338  df-on 6339  df-lim 6340  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-om 7846  df-en 8922  df-fin 8925

This theorem is referenced by:  snfi  9017  ssfi  9143  cnvfi  9146  fnfi  9148  nneneq  9176  nfielex  9225  imafiOLD  9272  xpfiOLD  9277  fodomfib  9287  iunfi  9301  fczfsuppd  9344  fsuppun  9345  0fsupp  9348  r1fin  9733  acndom  10011  numwdom  10019  ackbij1lem18  10196  sdom2en01  10262  fin23lem26  10285  isfin1-3  10346  gchxpidm  10629  fzfi  13944  fzofi  13946  hasheq0  14335  hashxp  14406  lcmf0  16611  0hashbc  16985  acsfn0  17628  isdrs2  18274  fpwipodrs  18506  symgfisg  19405  dsmm0cl  21656  mplsubg  21918  mpllss  21919  psrbag0  21976  mat0dimbas0  22360  mat0dim0  22361  mat0dimid  22362  mat0dimscm  22363  mat0dimcrng  22364  mat0scmat  22432  mavmul0  22446  mavmul0g  22447  mdet0pr  22486  m1detdiag  22491  d0mat2pmat  22632  chpmat0d  22728  fctop  22898  cmpfi  23302  bwth  23304  comppfsc  23426  ptbasid  23469  cfinfil  23787  ufinffr  23823  fin1aufil  23826  alexsubALTlem2  23942  alexsubALTlem4  23944  ptcmplem2  23947  tsmsfbas  24022  xrge0gsumle  24729  xrge0tsms  24730  fta1  26223  uhgr0edgfi  29174  fusgrfisbase  29262  vtxdg0e  29409  wwlksnfi  29843  mptiffisupp  32623  hashxpe  32739  xrge0tsmsd  33009  elrgspnlem4  33203  esumnul  34045  esum0  34046  esumcst  34060  esumsnf  34061  esumpcvgval  34075  sibf0  34332  eulerpartlemt  34369  derang0  35163  topdifinffinlem  37342  matunitlindf  37619  0totbnd  37774  heiborlem6  37817  mzpcompact2lem  42746  rp-isfinite6  43514  0pwfi  45060  fouriercn  46237  rrxtopn0  46298  salexct  46339  sge0rnn0  46373  sge00  46381  sge0sn  46384  ovn0val  46555  ovn02  46573  hoidmv0val  46588  hoidmvle  46605  hoiqssbl  46630  von0val  46676  vonhoire  46677  vonioo  46687  vonicc  46690  vonsn  46696  lcoc0  48415  lco0  48420