Theorem 0fi 8993

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

Assertion

Ref	Expression
0fi	⊢ ∅ ∈ Fin

Proof of Theorem 0fi

Step	Hyp	Ref	Expression
1		peano1 7843	. . 3 ⊢ ∅ ∈ ω
2		eqid 2737	. . . 4 ⊢ ∅ = ∅
3		en0 8969	. . . 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 8926	. 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 7820   ≈ cen 8894  Fincfn 8897

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 5245  ax-nul 5255  ax-pr 5381

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 5529  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5587  df-we 5589  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-ord 6330  df-on 6331  df-lim 6332  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-om 7821  df-en 8898  df-fin 8901

This theorem is referenced by:  snfi  8994  ssfi  9111  cnvfi  9114  fnfi  9116  nneneq  9144  nfielex  9188  imafiOLD  9230  fodomfib  9243  iunfi  9257  fczfsuppd  9303  fsuppun  9304  0fsupp  9307  r1fin  9699  acndom  9975  numwdom  9983  ackbij1lem18  10160  sdom2en01  10226  fin23lem26  10249  isfin1-3  10310  gchxpidm  10594  fzfi  13909  fzofi  13911  hasheq0  14300  hashxp  14371  lcmf0  16575  0hashbc  16949  acsfn0  17597  isdrs2  18243  fpwipodrs  18477  symgfisg  19414  dsmm0cl  21712  mplsubg  21974  mpllss  21975  psrbag0  22034  mat0dimbas0  22427  mat0dim0  22428  mat0dimid  22429  mat0dimscm  22430  mat0dimcrng  22431  mat0scmat  22499  mavmul0  22513  mavmul0g  22514  mdet0pr  22553  m1detdiag  22558  d0mat2pmat  22699  chpmat0d  22795  fctop  22965  cmpfi  23369  bwth  23371  comppfsc  23493  ptbasid  23536  cfinfil  23854  ufinffr  23890  fin1aufil  23893  alexsubALTlem2  24009  alexsubALTlem4  24011  ptcmplem2  24014  tsmsfbas  24089  xrge0gsumle  24795  xrge0tsms  24796  fta1  26289  uhgr0edgfi  29331  fusgrfisbase  29419  vtxdg0e  29566  wwlksnfi  29997  mptiffisupp  32789  hashxpe  32904  xrge0tsmsd  33173  elrgspnlem4  33345  extvfvcl  33719  vieta  33763  esumnul  34232  esum0  34233  esumcst  34247  esumsnf  34248  esumpcvgval  34262  sibf0  34518  eulerpartlemt  34555  derang0  35391  topdifinffinlem  37629  matunitlindf  37898  0totbnd  38053  heiborlem6  38096  mzpcompact2lem  43137  rp-isfinite6  43903  0pwfi  45448  fouriercn  46619  rrxtopn0  46680  salexct  46721  sge0rnn0  46755  sge00  46763  sge0sn  46766  ovn0val  46937  ovn02  46955  hoidmv0val  46970  hoidmvle  46987  hoiqssbl  47012  von0val  47058  vonhoire  47059  vonioo  47069  vonicc  47072  vonsn  47078  lcoc0  48811  lco0  48816