Theorem 0fi 9013

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

Assertion

Ref	Expression
0fi	⊢ ∅ ∈ Fin

Proof of Theorem 0fi

Step	Hyp	Ref	Expression
1		peano1 7865	. . 3 ⊢ ∅ ∈ ω
2		eqid 2729	. . . 4 ⊢ ∅ = ∅
3		en0 8989	. . . 4 ⊢ (∅ ≈ ∅ ↔ ∅ = ∅)
4	2, 3	mpbir 231	. . 3 ⊢ ∅ ≈ ∅
5		breq2 5111	. . . 4 ⊢ (𝑥 = ∅ → (∅ ≈ 𝑥 ↔ ∅ ≈ ∅))
6	5	rspcev 3588	. . 3 ⊢ ((∅ ∈ ω ∧ ∅ ≈ ∅) → ∃𝑥 ∈ ω ∅ ≈ 𝑥)
7	1, 4, 6	mp2an 692	. 2 ⊢ ∃𝑥 ∈ ω ∅ ≈ 𝑥
8		isfi 8947	. 2 ⊢ (∅ ∈ Fin ↔ ∃𝑥 ∈ ω ∅ ≈ 𝑥)
9	7, 8	mpbir 231	1 ⊢ ∅ ∈ Fin

Syntax hints:   = wceq 1540   ∈ wcel 2109  ∃wrex 3053  ∅c0 4296   class class class wbr 5107  ωcom 7842   ≈ cen 8915  Fincfn 8918

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2533  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-ord 6335  df-on 6336  df-lim 6337  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-om 7843  df-en 8919  df-fin 8922

This theorem is referenced by:  snfi  9014  ssfi  9137  cnvfi  9140  fnfi  9142  nneneq  9170  nfielex  9218  imafiOLD  9265  xpfiOLD  9270  fodomfib  9280  iunfi  9294  fczfsuppd  9337  fsuppun  9338  0fsupp  9341  r1fin  9726  acndom  10004  numwdom  10012  ackbij1lem18  10189  sdom2en01  10255  fin23lem26  10278  isfin1-3  10339  gchxpidm  10622  fzfi  13937  fzofi  13939  hasheq0  14328  hashxp  14399  lcmf0  16604  0hashbc  16978  acsfn0  17621  isdrs2  18267  fpwipodrs  18499  symgfisg  19398  dsmm0cl  21649  mplsubg  21911  mpllss  21912  psrbag0  21969  mat0dimbas0  22353  mat0dim0  22354  mat0dimid  22355  mat0dimscm  22356  mat0dimcrng  22357  mat0scmat  22425  mavmul0  22439  mavmul0g  22440  mdet0pr  22479  m1detdiag  22484  d0mat2pmat  22625  chpmat0d  22721  fctop  22891  cmpfi  23295  bwth  23297  comppfsc  23419  ptbasid  23462  cfinfil  23780  ufinffr  23816  fin1aufil  23819  alexsubALTlem2  23935  alexsubALTlem4  23937  ptcmplem2  23940  tsmsfbas  24015  xrge0gsumle  24722  xrge0tsms  24723  fta1  26216  uhgr0edgfi  29167  fusgrfisbase  29255  vtxdg0e  29402  wwlksnfi  29836  mptiffisupp  32616  hashxpe  32732  xrge0tsmsd  33002  elrgspnlem4  33196  esumnul  34038  esum0  34039  esumcst  34053  esumsnf  34054  esumpcvgval  34068  sibf0  34325  eulerpartlemt  34362  derang0  35156  topdifinffinlem  37335  matunitlindf  37612  0totbnd  37767  heiborlem6  37810  mzpcompact2lem  42739  rp-isfinite6  43507  0pwfi  45053  fouriercn  46230  rrxtopn0  46291  salexct  46332  sge0rnn0  46366  sge00  46374  sge0sn  46377  ovn0val  46548  ovn02  46566  hoidmv0val  46581  hoidmvle  46598  hoiqssbl  46623  von0val  46669  vonhoire  46670  vonioo  46680  vonicc  46683  vonsn  46689  lcoc0  48411  lco0  48416