Theorem 0fi 8979

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

Assertion

Ref	Expression
0fi	⊢ ∅ ∈ Fin

Proof of Theorem 0fi

Step	Hyp	Ref	Expression
1		peano1 7829	. . 3 ⊢ ∅ ∈ ω
2		eqid 2739	. . . 4 ⊢ ∅ = ∅
3		en0 8955	. . . 4 ⊢ (∅ ≈ ∅ ↔ ∅ = ∅)
4	2, 3	mpbir 232	. . 3 ⊢ ∅ ≈ ∅
5		breq2 5076	. . . 4 ⊢ (𝑥 = ∅ → (∅ ≈ 𝑥 ↔ ∅ ≈ ∅))
6	5	rspcev 3560	. . 3 ⊢ ((∅ ∈ ω ∧ ∅ ≈ ∅) → ∃𝑥 ∈ ω ∅ ≈ 𝑥)
7	1, 4, 6	mp2an 698	. 2 ⊢ ∃𝑥 ∈ ω ∅ ≈ 𝑥
8		isfi 8912	. 2 ⊢ (∅ ∈ Fin ↔ ∃𝑥 ∈ ω ∅ ≈ 𝑥)
9	7, 8	mpbir 232	1 ⊢ ∅ ∈ Fin

Syntax hints:   = wceq 1547   ∈ wcel 2119  ∃wrex 3063  ∅c0 4261   class class class wbr 5072  ωcom 7806   ≈ cen 8880  Fincfn 8883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-mo 2543  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-ord 6313  df-on 6314  df-lim 6315  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-om 7807  df-en 8884  df-fin 8887

This theorem is referenced by:  snfi  8980  ssfi  9097  cnvfi  9100  fnfi  9102  nneneq  9130  nfielex  9174  imafiOLD  9216  fodomfib  9229  iunfi  9243  fczfsuppd  9289  fsuppun  9290  0fsupp  9293  r1fin  9688  acndom  9964  numwdom  9972  ackbij1lem18  10149  sdom2en01  10215  fin23lem26  10238  isfin1-3  10299  gchxpidm  10583  fzfi  13925  fzofi  13927  hasheq0  14316  hashxp  14387  lcmf0  16594  0hashbc  16969  acsfn0  17617  isdrs2  18263  fpwipodrs  18497  symgfisg  19434  dsmm0cl  21715  mplsubg  21976  mpllss  21977  psrbag0  22038  mat0dimbas0  22449  mat0dim0  22450  mat0dimid  22451  mat0dimscm  22452  mat0dimcrng  22453  mat0scmat  22521  mavmul0  22535  mavmul0g  22536  mdet0pr  22575  m1detdiag  22580  d0mat2pmat  22721  chpmat0d  22817  fctop  22987  cmpfi  23391  bwth  23393  comppfsc  23515  ptbasid  23558  cfinfil  23876  ufinffr  23912  fin1aufil  23915  alexsubALTlem2  24031  alexsubALTlem4  24033  ptcmplem2  24036  tsmsfbas  24111  xrge0gsumle  24817  xrge0tsms  24818  fta1  26292  uhgr0edgfi  29327  fusgrfisbase  29415  vtxdg0e  29561  wwlksnfi  29992  mptiffisupp  32785  hashxpe  32899  xrge0tsmsd  33154  elrgspnlem4  33326  0mplrim  33698  extvfvcl  33720  vieta  33764  esumnul  34232  esum0  34233  esumcst  34247  esumsnf  34248  esumpcvgval  34262  sibf0  34518  eulerpartlemt  34555  derang0  35397  topdifinffinlem  37709  matunitlindf  37985  0totbnd  38140  heiborlem6  38183  mzpcompact2lem  43200  rp-isfinite6  43962  0pwfi  45507  fouriercn  46675  rrxtopn0  46736  salexct  46777  sge0rnn0  46811  sge00  46819  sge0sn  46822  ovn0val  46993  ovn02  47011  hoidmv0val  47026  hoidmvle  47043  hoiqssbl  47068  von0val  47114  vonhoire  47115  vonioo  47125  vonicc  47128  vonsn  47134  lcoc0  48913  lco0  48918