Theorem 0fi 8991

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

Assertion

Ref	Expression
0fi	⊢ ∅ ∈ Fin

Proof of Theorem 0fi

Step	Hyp	Ref	Expression
1		peano1 7841	. . 3 ⊢ ∅ ∈ ω
2		eqid 2737	. . . 4 ⊢ ∅ = ∅
3		en0 8967	. . . 4 ⊢ (∅ ≈ ∅ ↔ ∅ = ∅)
4	2, 3	mpbir 231	. . 3 ⊢ ∅ ≈ ∅
5		breq2 5104	. . . 4 ⊢ (𝑥 = ∅ → (∅ ≈ 𝑥 ↔ ∅ ≈ ∅))
6	5	rspcev 3578	. . 3 ⊢ ((∅ ∈ ω ∧ ∅ ≈ ∅) → ∃𝑥 ∈ ω ∅ ≈ 𝑥)
7	1, 4, 6	mp2an 693	. 2 ⊢ ∃𝑥 ∈ ω ∅ ≈ 𝑥
8		isfi 8924	. 2 ⊢ (∅ ∈ Fin ↔ ∃𝑥 ∈ ω ∅ ≈ 𝑥)
9	7, 8	mpbir 231	1 ⊢ ∅ ∈ Fin

Syntax hints:   = wceq 1542   ∈ wcel 2114  ∃wrex 3062  ∅c0 4287   class class class wbr 5100  ωcom 7818   ≈ cen 8892  Fincfn 8895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-ord 6328  df-on 6329  df-lim 6330  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-om 7819  df-en 8896  df-fin 8899

This theorem is referenced by:  snfi  8992  ssfi  9109  cnvfi  9112  fnfi  9114  nneneq  9142  nfielex  9186  imafiOLD  9228  fodomfib  9241  iunfi  9255  fczfsuppd  9301  fsuppun  9302  0fsupp  9305  r1fin  9697  acndom  9973  numwdom  9981  ackbij1lem18  10158  sdom2en01  10224  fin23lem26  10247  isfin1-3  10308  gchxpidm  10592  fzfi  13907  fzofi  13909  hasheq0  14298  hashxp  14369  lcmf0  16573  0hashbc  16947  acsfn0  17595  isdrs2  18241  fpwipodrs  18475  symgfisg  19409  dsmm0cl  21707  mplsubg  21969  mpllss  21970  psrbag0  22029  mat0dimbas0  22422  mat0dim0  22423  mat0dimid  22424  mat0dimscm  22425  mat0dimcrng  22426  mat0scmat  22494  mavmul0  22508  mavmul0g  22509  mdet0pr  22548  m1detdiag  22553  d0mat2pmat  22694  chpmat0d  22790  fctop  22960  cmpfi  23364  bwth  23366  comppfsc  23488  ptbasid  23531  cfinfil  23849  ufinffr  23885  fin1aufil  23888  alexsubALTlem2  24004  alexsubALTlem4  24006  ptcmplem2  24009  tsmsfbas  24084  xrge0gsumle  24790  xrge0tsms  24791  fta1  26284  uhgr0edgfi  29325  fusgrfisbase  29413  vtxdg0e  29560  wwlksnfi  29991  mptiffisupp  32783  hashxpe  32898  xrge0tsmsd  33167  elrgspnlem4  33339  extvfvcl  33713  vieta  33757  esumnul  34226  esum0  34227  esumcst  34241  esumsnf  34242  esumpcvgval  34256  sibf0  34512  eulerpartlemt  34549  derang0  35385  topdifinffinlem  37602  matunitlindf  37869  0totbnd  38024  heiborlem6  38067  mzpcompact2lem  43108  rp-isfinite6  43874  0pwfi  45419  fouriercn  46590  rrxtopn0  46651  salexct  46692  sge0rnn0  46726  sge00  46734  sge0sn  46737  ovn0val  46908  ovn02  46926  hoidmv0val  46941  hoidmvle  46958  hoiqssbl  46983  von0val  47029  vonhoire  47030  vonioo  47040  vonicc  47043  vonsn  47049  lcoc0  48782  lco0  48787