Theorem 0fi 9087

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

Assertion

Ref	Expression
0fi	⊢ ∅ ∈ Fin

Proof of Theorem 0fi

Step	Hyp	Ref	Expression
1		peano1 7908	. . 3 ⊢ ∅ ∈ ω
2		eqid 2729	. . . 4 ⊢ ∅ = ∅
3		en0 9057	. . . 4 ⊢ (∅ ≈ ∅ ↔ ∅ = ∅)
4	2, 3	mpbir 230	. . 3 ⊢ ∅ ≈ ∅
5		breq2 5160	. . . 4 ⊢ (𝑥 = ∅ → (∅ ≈ 𝑥 ↔ ∅ ≈ ∅))
6	5	rspcev 3620	. . 3 ⊢ ((∅ ∈ ω ∧ ∅ ≈ ∅) → ∃𝑥 ∈ ω ∅ ≈ 𝑥)
7	1, 4, 6	mp2an 690	. 2 ⊢ ∃𝑥 ∈ ω ∅ ≈ 𝑥
8		isfi 9015	. 2 ⊢ (∅ ∈ Fin ↔ ∃𝑥 ∈ ω ∅ ≈ 𝑥)
9	7, 8	mpbir 230	1 ⊢ ∅ ∈ Fin

Syntax hints:   = wceq 1534   ∈ wcel 2100  ∃wrex 3063  ∅c0 4335   class class class wbr 5156  ωcom 7884   ≈ cen 8979  Fincfn 8982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-12 2170  ax-ext 2700  ax-sep 5307  ax-nul 5314  ax-pr 5437

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2062  df-mo 2532  df-clab 2707  df-cleq 2721  df-clel 2806  df-ne 2934  df-ral 3055  df-rex 3064  df-rab 3429  df-v 3474  df-dif 3962  df-un 3964  df-in 3966  df-ss 3976  df-pss 3979  df-nul 4336  df-if 4537  df-pw 4612  df-sn 4637  df-pr 4639  df-op 4643  df-uni 4919  df-br 5157  df-opab 5219  df-tr 5274  df-id 5584  df-eprel 5590  df-po 5598  df-so 5599  df-fr 5641  df-we 5643  df-xp 5692  df-rel 5693  df-cnv 5694  df-co 5695  df-dm 5696  df-rn 5697  df-ord 6383  df-on 6384  df-lim 6385  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-om 7885  df-en 8983  df-fin 8986

This theorem is referenced by:  snfi  9088  ssfi  9219  cnvfi  9222  fnfi  9223  nneneq  9251  nfielex  9314  imafiOLD  9363  xpfiOLD  9368  fodomfib  9378  iunfi  9392  fczfsuppd  9436  fsuppun  9437  0fsupp  9440  r1fin  9823  acndom  10101  numwdom  10109  ackbij1lem18  10286  sdom2en01  10352  fin23lem26  10375  isfin1-3  10436  gchxpidm  10719  fzfi  14003  fzofi  14005  hasheq0  14392  hashxp  14463  lcmf0  16656  0hashbc  17030  acsfn0  17694  isdrs2  18352  fpwipodrs  18586  symgfisg  19488  dsmm0cl  21760  mplsubg  22033  mpllss  22034  psrbag0  22097  mat0dimbas0  22482  mat0dim0  22483  mat0dimid  22484  mat0dimscm  22485  mat0dimcrng  22486  mat0scmat  22554  mavmul0  22568  mavmul0g  22569  mdet0pr  22608  m1detdiag  22613  d0mat2pmat  22754  chpmat0d  22850  fctop  23021  cmpfi  23426  bwth  23428  comppfsc  23550  ptbasid  23593  cfinfil  23911  ufinffr  23947  fin1aufil  23950  alexsubALTlem2  24066  alexsubALTlem4  24068  ptcmplem2  24071  tsmsfbas  24146  xrge0gsumle  24863  xrge0tsms  24864  fta1  26359  uhgr0edgfi  29199  fusgrfisbase  29287  vtxdg0e  29434  wwlksnfi  29863  mptiffisupp  32630  hashxpe  32739  xrge0tsmsd  32955  esumnul  33919  esum0  33920  esumcst  33934  esumsnf  33935  esumpcvgval  33949  sibf0  34206  eulerpartlemt  34243  derang0  35044  topdifinffinlem  37101  matunitlindf  37366  0totbnd  37521  heiborlem6  37564  mzpcompact2lem  42479  rp-isfinite6  43256  0pwfi  44731  fouriercn  45923  rrxtopn0  45984  salexct  46025  sge0rnn0  46059  sge00  46067  sge0sn  46070  ovn0val  46241  ovn02  46259  hoidmv0val  46274  hoidmvle  46291  hoiqssbl  46316  von0val  46362  vonhoire  46363  vonioo  46373  vonicc  46376  vonsn  46382  lcoc0  47886  lco0  47891