Theorem 0fi 9054

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

Assertion

Ref	Expression
0fi	⊢ ∅ ∈ Fin

Proof of Theorem 0fi

Step	Hyp	Ref	Expression
1		peano1 7882	. . 3 ⊢ ∅ ∈ ω
2		eqid 2735	. . . 4 ⊢ ∅ = ∅
3		en0 9030	. . . 4 ⊢ (∅ ≈ ∅ ↔ ∅ = ∅)
4	2, 3	mpbir 231	. . 3 ⊢ ∅ ≈ ∅
5		breq2 5123	. . . 4 ⊢ (𝑥 = ∅ → (∅ ≈ 𝑥 ↔ ∅ ≈ ∅))
6	5	rspcev 3601	. . 3 ⊢ ((∅ ∈ ω ∧ ∅ ≈ ∅) → ∃𝑥 ∈ ω ∅ ≈ 𝑥)
7	1, 4, 6	mp2an 692	. 2 ⊢ ∃𝑥 ∈ ω ∅ ≈ 𝑥
8		isfi 8988	. 2 ⊢ (∅ ∈ Fin ↔ ∃𝑥 ∈ ω ∅ ≈ 𝑥)
9	7, 8	mpbir 231	1 ⊢ ∅ ∈ Fin

Syntax hints:   = wceq 1540   ∈ wcel 2108  ∃wrex 3060  ∅c0 4308   class class class wbr 5119  ωcom 7859   ≈ cen 8954  Fincfn 8957

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 2007  ax-8 2110  ax-9 2118  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-ord 6355  df-on 6356  df-lim 6357  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-om 7860  df-en 8958  df-fin 8961

This theorem is referenced by:  snfi  9055  ssfi  9185  cnvfi  9188  fnfi  9190  nneneq  9218  nfielex  9277  imafiOLD  9324  xpfiOLD  9329  fodomfib  9339  iunfi  9353  fczfsuppd  9396  fsuppun  9397  0fsupp  9400  r1fin  9785  acndom  10063  numwdom  10071  ackbij1lem18  10248  sdom2en01  10314  fin23lem26  10337  isfin1-3  10398  gchxpidm  10681  fzfi  13988  fzofi  13990  hasheq0  14379  hashxp  14450  lcmf0  16651  0hashbc  17025  acsfn0  17670  isdrs2  18316  fpwipodrs  18548  symgfisg  19447  dsmm0cl  21698  mplsubg  21960  mpllss  21961  psrbag0  22018  mat0dimbas0  22402  mat0dim0  22403  mat0dimid  22404  mat0dimscm  22405  mat0dimcrng  22406  mat0scmat  22474  mavmul0  22488  mavmul0g  22489  mdet0pr  22528  m1detdiag  22533  d0mat2pmat  22674  chpmat0d  22770  fctop  22940  cmpfi  23344  bwth  23346  comppfsc  23468  ptbasid  23511  cfinfil  23829  ufinffr  23865  fin1aufil  23868  alexsubALTlem2  23984  alexsubALTlem4  23986  ptcmplem2  23989  tsmsfbas  24064  xrge0gsumle  24771  xrge0tsms  24772  fta1  26266  uhgr0edgfi  29165  fusgrfisbase  29253  vtxdg0e  29400  wwlksnfi  29834  mptiffisupp  32616  hashxpe  32732  xrge0tsmsd  33002  elrgspnlem4  33186  esumnul  34025  esum0  34026  esumcst  34040  esumsnf  34041  esumpcvgval  34055  sibf0  34312  eulerpartlemt  34349  derang0  35137  topdifinffinlem  37311  matunitlindf  37588  0totbnd  37743  heiborlem6  37786  mzpcompact2lem  42721  rp-isfinite6  43489  0pwfi  45031  fouriercn  46209  rrxtopn0  46270  salexct  46311  sge0rnn0  46345  sge00  46353  sge0sn  46356  ovn0val  46527  ovn02  46545  hoidmv0val  46560  hoidmvle  46577  hoiqssbl  46602  von0val  46648  vonhoire  46649  vonioo  46659  vonicc  46662  vonsn  46668  lcoc0  48346  lco0  48351