Theorem 0fi 9108

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

Assertion

Ref	Expression
0fi	⊢ ∅ ∈ Fin

Proof of Theorem 0fi

Step	Hyp	Ref	Expression
1		peano1 7927	. . 3 ⊢ ∅ ∈ ω
2		eqid 2740	. . . 4 ⊢ ∅ = ∅
3		en0 9078	. . . 4 ⊢ (∅ ≈ ∅ ↔ ∅ = ∅)
4	2, 3	mpbir 231	. . 3 ⊢ ∅ ≈ ∅
5		breq2 5170	. . . 4 ⊢ (𝑥 = ∅ → (∅ ≈ 𝑥 ↔ ∅ ≈ ∅))
6	5	rspcev 3635	. . 3 ⊢ ((∅ ∈ ω ∧ ∅ ≈ ∅) → ∃𝑥 ∈ ω ∅ ≈ 𝑥)
7	1, 4, 6	mp2an 691	. 2 ⊢ ∃𝑥 ∈ ω ∅ ≈ 𝑥
8		isfi 9036	. 2 ⊢ (∅ ∈ Fin ↔ ∃𝑥 ∈ ω ∅ ≈ 𝑥)
9	7, 8	mpbir 231	1 ⊢ ∅ ∈ Fin

Syntax hints:   = wceq 1537   ∈ wcel 2108  ∃wrex 3076  ∅c0 4352   class class class wbr 5166  ωcom 7903   ≈ cen 9000  Fincfn 9003

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-mo 2543  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-ord 6398  df-on 6399  df-lim 6400  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-om 7904  df-en 9004  df-fin 9007

This theorem is referenced by:  snfi  9109  ssfi  9240  cnvfi  9243  fnfi  9244  nneneq  9272  nfielex  9335  imafiOLD  9382  xpfiOLD  9387  fodomfib  9397  iunfi  9411  fczfsuppd  9455  fsuppun  9456  0fsupp  9459  r1fin  9842  acndom  10120  numwdom  10128  ackbij1lem18  10305  sdom2en01  10371  fin23lem26  10394  isfin1-3  10455  gchxpidm  10738  fzfi  14023  fzofi  14025  hasheq0  14412  hashxp  14483  lcmf0  16681  0hashbc  17054  acsfn0  17718  isdrs2  18376  fpwipodrs  18610  symgfisg  19510  dsmm0cl  21783  mplsubg  22045  mpllss  22046  psrbag0  22109  mat0dimbas0  22493  mat0dim0  22494  mat0dimid  22495  mat0dimscm  22496  mat0dimcrng  22497  mat0scmat  22565  mavmul0  22579  mavmul0g  22580  mdet0pr  22619  m1detdiag  22624  d0mat2pmat  22765  chpmat0d  22861  fctop  23032  cmpfi  23437  bwth  23439  comppfsc  23561  ptbasid  23604  cfinfil  23922  ufinffr  23958  fin1aufil  23961  alexsubALTlem2  24077  alexsubALTlem4  24079  ptcmplem2  24082  tsmsfbas  24157  xrge0gsumle  24874  xrge0tsms  24875  fta1  26368  uhgr0edgfi  29275  fusgrfisbase  29363  vtxdg0e  29510  wwlksnfi  29939  mptiffisupp  32705  hashxpe  32814  xrge0tsmsd  33041  esumnul  34012  esum0  34013  esumcst  34027  esumsnf  34028  esumpcvgval  34042  sibf0  34299  eulerpartlemt  34336  derang0  35137  topdifinffinlem  37313  matunitlindf  37578  0totbnd  37733  heiborlem6  37776  mzpcompact2lem  42707  rp-isfinite6  43480  0pwfi  44961  fouriercn  46153  rrxtopn0  46214  salexct  46255  sge0rnn0  46289  sge00  46297  sge0sn  46300  ovn0val  46471  ovn02  46489  hoidmv0val  46504  hoidmvle  46521  hoiqssbl  46546  von0val  46592  vonhoire  46593  vonioo  46603  vonicc  46606  vonsn  46612  lcoc0  48151  lco0  48156