Theorem 0fi 9077

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

Assertion

Ref	Expression
0fi	⊢ ∅ ∈ Fin

Proof of Theorem 0fi

Step	Hyp	Ref	Expression
1		peano1 7904	. . 3 ⊢ ∅ ∈ ω
2		eqid 2760	. . . 4 ⊢ ∅ = ∅
3		en0 9052	. . . 4 ⊢ (∅ ≈ ∅ ↔ ∅ = ∅)
4	2, 3	mpbir 234	. . 3 ⊢ ∅ ≈ ∅
5		breq2 5106	. . . 4 ⊢ (𝑥 = ∅ → (∅ ≈ 𝑥 ↔ ∅ ≈ ∅))
6	5	rspcev 3576	. . 3 ⊢ ((∅ ∈ ω ∧ ∅ ≈ ∅) → ∃𝑥 ∈ ω ∅ ≈ 𝑥)
7	1, 4, 6	mp2an 705	. 2 ⊢ ∃𝑥 ∈ ω ∅ ≈ 𝑥
8		isfi 9009	. 2 ⊢ (∅ ∈ Fin ↔ ∃𝑥 ∈ ω ∅ ≈ 𝑥)
9	7, 8	mpbir 234	1 ⊢ ∅ ∈ Fin

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144  ∃wrex 3086  ∅c0 4277   class class class wbr 5102  ωcom 7881   ≈ cen 8977  Fincfn 8980

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-mo 2564  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-ord 6368  df-on 6369  df-lim 6370  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-om 7882  df-en 8981  df-fin 8984

This theorem is used by:  snfi  9078  ssfi  9195  cnvfi  9198  fnfi  9200  nneneq  9228  nfielex  9272  fodomfib  9327  iunfi  9339  fczfsuppd  9385  fsuppun  9386  0fsupp  9389  r1fin  9787  acndom  10137  numwdom  10145  ackbij1lem18  10321  sdom2en01  10387  fin23lem26  10410  isfin1-3  10471  gchxpidm  10761  fzfi  14122  fzofi  14124  hasheq0  14514  hashxp  14586  lcmf0  16818  0hashbc  17194  acsfn0  17843  isdrs2  18489  fpwipodrs  18723  symgfisg  19691  dsmm0cl  22055  mplsubg  22318  mpllss  22319  psrbag0  22380  mat0dimbas0  22790  mat0dim0  22791  mat0dimid  22792  mat0dimscm  22793  mat0dimcrng  22794  mat0scmat  22862  mavmul0  22876  mavmul0g  22877  mdet0pr  22916  m1detdiag  22921  matunitlindf  23005  d0mat2pmat  23065  chpmat0d  23161  fctop  23331  cmpfi  23735  bwth  23737  comppfsc  23860  ptbasid  23903  cfinfil  24221  ufinffr  24257  fin1aufil  24260  alexsubALTlem2  24376  alexsubALTlem4  24378  ptcmplem2  24381  tsmsfbas  24456  xrge0gsumle  25162  xrge0tsms  25163  fta1  26638  uhgr0edgfi  29830  fusgrfisbase  29918  vtxdg0e  30064  wwlksnfi  30504  mptiffisupp  33337  hashxpe  33449  xrge0tsmsd  33684  elrgspnlem4  33856  0mplrim  34196  extvfvcl  34218  vieta  34262  esumnul  34730  esum0  34731  esumcst  34745  esumsnf  34746  esumpcvgval  34760  sibf0  35016  eulerpartlemt  35053  derang0  36024  topdifinffinlem  38379  0totbnd  38816  heiborlem6  38859  mzpcompact2lem  43871  rp-isfinite6  44628  0pwfi  46184  fouriercn  47350  rrxtopn0  47411  salexct  47452  sge0rnn0  47486  sge00  47494  sge0sn  47497  ovn0val  47668  ovn02  47686  hoidmv0val  47701  hoidmvle  47718  hoiqssbl  47743  von0val  47789  vonhoire  47790  vonioo  47800  vonicc  47803  vonsn  47809  lcoc0  49642  lco0  49647