Theorem 0fi 9082

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

Assertion

Ref	Expression
0fi	⊢ ∅ ∈ Fin

Proof of Theorem 0fi

Step	Hyp	Ref	Expression
1		peano1 7910	. . 3 ⊢ ∅ ∈ ω
2		eqid 2737	. . . 4 ⊢ ∅ = ∅
3		en0 9058	. . . 4 ⊢ (∅ ≈ ∅ ↔ ∅ = ∅)
4	2, 3	mpbir 231	. . 3 ⊢ ∅ ≈ ∅
5		breq2 5147	. . . 4 ⊢ (𝑥 = ∅ → (∅ ≈ 𝑥 ↔ ∅ ≈ ∅))
6	5	rspcev 3622	. . 3 ⊢ ((∅ ∈ ω ∧ ∅ ≈ ∅) → ∃𝑥 ∈ ω ∅ ≈ 𝑥)
7	1, 4, 6	mp2an 692	. 2 ⊢ ∃𝑥 ∈ ω ∅ ≈ 𝑥
8		isfi 9016	. 2 ⊢ (∅ ∈ Fin ↔ ∃𝑥 ∈ ω ∅ ≈ 𝑥)
9	7, 8	mpbir 231	1 ⊢ ∅ ∈ Fin

Syntax hints:   = wceq 1540   ∈ wcel 2108  ∃wrex 3070  ∅c0 4333   class class class wbr 5143  ωcom 7887   ≈ cen 8982  Fincfn 8985

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 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-mo 2540  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-ord 6387  df-on 6388  df-lim 6389  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-om 7888  df-en 8986  df-fin 8989

This theorem is referenced by:  snfi  9083  ssfi  9213  cnvfi  9216  fnfi  9218  nneneq  9246  nfielex  9307  imafiOLD  9354  xpfiOLD  9359  fodomfib  9369  iunfi  9383  fczfsuppd  9426  fsuppun  9427  0fsupp  9430  r1fin  9813  acndom  10091  numwdom  10099  ackbij1lem18  10276  sdom2en01  10342  fin23lem26  10365  isfin1-3  10426  gchxpidm  10709  fzfi  14013  fzofi  14015  hasheq0  14402  hashxp  14473  lcmf0  16671  0hashbc  17045  acsfn0  17703  isdrs2  18352  fpwipodrs  18585  symgfisg  19486  dsmm0cl  21760  mplsubg  22022  mpllss  22023  psrbag0  22086  mat0dimbas0  22472  mat0dim0  22473  mat0dimid  22474  mat0dimscm  22475  mat0dimcrng  22476  mat0scmat  22544  mavmul0  22558  mavmul0g  22559  mdet0pr  22598  m1detdiag  22603  d0mat2pmat  22744  chpmat0d  22840  fctop  23011  cmpfi  23416  bwth  23418  comppfsc  23540  ptbasid  23583  cfinfil  23901  ufinffr  23937  fin1aufil  23940  alexsubALTlem2  24056  alexsubALTlem4  24058  ptcmplem2  24061  tsmsfbas  24136  xrge0gsumle  24855  xrge0tsms  24856  fta1  26350  uhgr0edgfi  29257  fusgrfisbase  29345  vtxdg0e  29492  wwlksnfi  29926  mptiffisupp  32702  hashxpe  32811  xrge0tsmsd  33065  elrgspnlem4  33249  esumnul  34049  esum0  34050  esumcst  34064  esumsnf  34065  esumpcvgval  34079  sibf0  34336  eulerpartlemt  34373  derang0  35174  topdifinffinlem  37348  matunitlindf  37625  0totbnd  37780  heiborlem6  37823  mzpcompact2lem  42762  rp-isfinite6  43531  0pwfi  45064  fouriercn  46247  rrxtopn0  46308  salexct  46349  sge0rnn0  46383  sge00  46391  sge0sn  46394  ovn0val  46565  ovn02  46583  hoidmv0val  46598  hoidmvle  46615  hoiqssbl  46640  von0val  46686  vonhoire  46687  vonioo  46697  vonicc  46700  vonsn  46706  lcoc0  48339  lco0  48344