Theorem 0fi 9108

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

Assertion

Ref	Expression
0fi	⊢ ∅ ∈ Fin

Proof of Theorem 0fi

Step	Hyp	Ref	Expression
1		peano1 7934	. . 3 ⊢ ∅ ∈ ω
2		eqid 2763	. . . 4 ⊢ ∅ = ∅
3		en0 9083	. . . 4 ⊢ (∅ ≈ ∅ ↔ ∅ = ∅)
4	2, 3	mpbir 234	. . 3 ⊢ ∅ ≈ ∅
5		breq2 5112	. . . 4 ⊢ (𝑥 = ∅ → (∅ ≈ 𝑥 ↔ ∅ ≈ ∅))
6	5	rspcev 3580	. . 3 ⊢ ((∅ ∈ ω ∧ ∅ ≈ ∅) → ∃𝑥 ∈ ω ∅ ≈ 𝑥)
7	1, 4, 6	mp2an 705	. 2 ⊢ ∃𝑥 ∈ ω ∅ ≈ 𝑥
8		isfi 9040	. 2 ⊢ (∅ ∈ Fin ↔ ∃𝑥 ∈ ω ∅ ≈ 𝑥)
9	7, 8	mpbir 234	1 ⊢ ∅ ∈ Fin

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  ∃wrex 3090  ∅c0 4281   class class class wbr 5108  ωcom 7911   ≈ cen 9008  Fincfn 9011

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-ord 6391  df-on 6392  df-lim 6393  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-om 7912  df-en 9012  df-fin 9015

This theorem is used by:  snfi  9109  ssfi  9226  cnvfi  9229  fnfi  9231  nneneq  9259  nfielex  9303  fodomfib  9358  iunfi  9370  fczfsuppd  9415  fsuppun  9416  0fsupp  9419  r1fin  9817  acndom  10169  numwdom  10177  ackbij1lem18  10353  sdom2en01  10419  fin23lem26  10442  isfin1-3  10503  gchxpidm  10793  fzfi  14155  fzofi  14157  hasheq0  14548  hashxp  14620  lcmf0  16853  0hashbc  17229  acsfn0  17884  isdrs2  18530  fpwipodrs  18764  symgfisg  19733  dsmm0cl  22101  mplsubg  22364  mpllss  22365  psrbag0  22426  mat0dimbas0  22836  mat0dim0  22837  mat0dimid  22838  mat0dimscm  22839  mat0dimcrng  22840  mat0scmat  22908  mavmul0  22922  mavmul0g  22923  mdet0pr  22962  m1detdiag  22967  matunitlindf  23051  d0mat2pmat  23111  chpmat0d  23207  fctop  23377  cmpfi  23781  bwth  23783  comppfsc  23906  ptbasid  23949  cfinfil  24267  ufinffr  24303  fin1aufil  24306  alexsubALTlem2  24422  alexsubALTlem4  24424  ptcmplem2  24427  tsmsfbas  24502  xrge0gsumle  25208  xrge0tsms  25209  fta1  26684  uhgr0edgfi  29878  fusgrfisbase  29966  vtxdg0e  30112  wwlksnfi  30552  mptiffisupp  33383  hashxpe  33495  xrge0tsmsd  33733  elrgspnlem4  33905  0mplrim  34257  extvfvcl  34279  vieta  34323  esumnul  34791  esum0  34792  esumcst  34806  esumsnf  34807  esumpcvgval  34821  sibf0  35077  eulerpartlemt  35114  derang0  36142  topdifinffinlem  38538  0totbnd  38973  heiborlem6  39016  mzpcompact2lem  44028  rp-isfinite6  44780  0pwfi  46350  fouriercn  47515  rrxtopn0  47576  salexct  47617  sge0rnn0  47651  sge00  47659  sge0sn  47662  ovn0val  47833  ovn02  47851  hoidmv0val  47866  hoidmvle  47883  hoiqssbl  47908  von0val  47954  vonhoire  47955  vonioo  47965  vonicc  47968  vonsn  47974  lcoc0  49865  lco0  49870