Theorem 0fi 8964

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

Assertion

Ref	Expression
0fi	⊢ ∅ ∈ Fin

Proof of Theorem 0fi

Step	Hyp	Ref	Expression
1		peano1 7819	. . 3 ⊢ ∅ ∈ ω
2		eqid 2731	. . . 4 ⊢ ∅ = ∅
3		en0 8940	. . . 4 ⊢ (∅ ≈ ∅ ↔ ∅ = ∅)
4	2, 3	mpbir 231	. . 3 ⊢ ∅ ≈ ∅
5		breq2 5093	. . . 4 ⊢ (𝑥 = ∅ → (∅ ≈ 𝑥 ↔ ∅ ≈ ∅))
6	5	rspcev 3572	. . 3 ⊢ ((∅ ∈ ω ∧ ∅ ≈ ∅) → ∃𝑥 ∈ ω ∅ ≈ 𝑥)
7	1, 4, 6	mp2an 692	. 2 ⊢ ∃𝑥 ∈ ω ∅ ≈ 𝑥
8		isfi 8898	. 2 ⊢ (∅ ∈ Fin ↔ ∃𝑥 ∈ ω ∅ ≈ 𝑥)
9	7, 8	mpbir 231	1 ⊢ ∅ ∈ Fin

Syntax hints:   = wceq 1541   ∈ wcel 2111  ∃wrex 3056  ∅c0 4280   class class class wbr 5089  ωcom 7796   ≈ cen 8866  Fincfn 8869

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-mo 2535  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-ord 6309  df-on 6310  df-lim 6311  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-om 7797  df-en 8870  df-fin 8873

This theorem is referenced by:  snfi  8965  ssfi  9082  cnvfi  9085  fnfi  9087  nneneq  9115  nfielex  9158  imafiOLD  9200  fodomfib  9213  iunfi  9227  fczfsuppd  9270  fsuppun  9271  0fsupp  9274  r1fin  9666  acndom  9942  numwdom  9950  ackbij1lem18  10127  sdom2en01  10193  fin23lem26  10216  isfin1-3  10277  gchxpidm  10560  fzfi  13879  fzofi  13881  hasheq0  14270  hashxp  14341  lcmf0  16545  0hashbc  16919  acsfn0  17566  isdrs2  18212  fpwipodrs  18446  symgfisg  19380  dsmm0cl  21677  mplsubg  21939  mpllss  21940  psrbag0  21997  mat0dimbas0  22381  mat0dim0  22382  mat0dimid  22383  mat0dimscm  22384  mat0dimcrng  22385  mat0scmat  22453  mavmul0  22467  mavmul0g  22468  mdet0pr  22507  m1detdiag  22512  d0mat2pmat  22653  chpmat0d  22749  fctop  22919  cmpfi  23323  bwth  23325  comppfsc  23447  ptbasid  23490  cfinfil  23808  ufinffr  23844  fin1aufil  23847  alexsubALTlem2  23963  alexsubALTlem4  23965  ptcmplem2  23968  tsmsfbas  24043  xrge0gsumle  24749  xrge0tsms  24750  fta1  26243  uhgr0edgfi  29218  fusgrfisbase  29306  vtxdg0e  29453  wwlksnfi  29884  mptiffisupp  32674  hashxpe  32789  xrge0tsmsd  33042  elrgspnlem4  33212  esumnul  34061  esum0  34062  esumcst  34076  esumsnf  34077  esumpcvgval  34091  sibf0  34347  eulerpartlemt  34384  derang0  35213  topdifinffinlem  37389  matunitlindf  37666  0totbnd  37821  heiborlem6  37864  mzpcompact2lem  42792  rp-isfinite6  43559  0pwfi  45104  fouriercn  46278  rrxtopn0  46339  salexct  46380  sge0rnn0  46414  sge00  46422  sge0sn  46425  ovn0val  46596  ovn02  46614  hoidmv0val  46629  hoidmvle  46646  hoiqssbl  46671  von0val  46717  vonhoire  46718  vonioo  46728  vonicc  46731  vonsn  46737  lcoc0  48462  lco0  48467