Theorem 0fi 9035

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

Assertion

Ref	Expression
0fi	⊢ ∅ ∈ Fin

Proof of Theorem 0fi

Step	Hyp	Ref	Expression
1		peano1 7881	. . 3 ⊢ ∅ ∈ ω
2		eqid 2763	. . . 4 ⊢ ∅ = ∅
3		en0 9011	. . . 4 ⊢ (∅ ≈ ∅ ↔ ∅ = ∅)
4	2, 3	mpbir 234	. . 3 ⊢ ∅ ≈ ∅
5		breq2 5113	. . . 4 ⊢ (𝑥 = ∅ → (∅ ≈ 𝑥 ↔ ∅ ≈ ∅))
6	5	rspcev 3581	. . 3 ⊢ ((∅ ∈ ω ∧ ∅ ≈ ∅) → ∃𝑥 ∈ ω ∅ ≈ 𝑥)
7	1, 4, 6	mp2an 704	. 2 ⊢ ∃𝑥 ∈ ω ∅ ≈ 𝑥
8		isfi 8968	. 2 ⊢ (∅ ∈ Fin ↔ ∃𝑥 ∈ ω ∅ ≈ 𝑥)
9	7, 8	mpbir 234	1 ⊢ ∅ ∈ Fin

Syntax hints:   = wceq 1570   ∈ wcel 2143  ∃wrex 3089  ∅c0 4286   class class class wbr 5109  ωcom 7858   ≈ cen 8936  Fincfn 8939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-ord 6363  df-on 6364  df-lim 6365  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-om 7859  df-en 8940  df-fin 8943

This theorem is referenced by:  snfi  9036  ssfi  9153  cnvfi  9156  fnfi  9158  nneneq  9186  nfielex  9230  fodomfib  9284  iunfi  9296  fczfsuppd  9342  fsuppun  9343  0fsupp  9346  r1fin  9741  acndom  10031  numwdom  10039  ackbij1lem18  10215  sdom2en01  10281  fin23lem26  10304  isfin1-3  10365  gchxpidm  10649  fzfi  14004  fzofi  14006  hasheq0  14395  hashxp  14467  lcmf0  16687  0hashbc  17062  acsfn0  17711  isdrs2  18357  fpwipodrs  18591  symgfisg  19533  dsmm0cl  21890  mplsubg  22151  mpllss  22152  psrbag0  22213  mat0dimbas0  22623  mat0dim0  22624  mat0dimid  22625  mat0dimscm  22626  mat0dimcrng  22627  mat0scmat  22695  mavmul0  22709  mavmul0g  22710  mdet0pr  22749  m1detdiag  22754  d0mat2pmat  22895  chpmat0d  22991  fctop  23161  cmpfi  23565  bwth  23567  comppfsc  23689  ptbasid  23732  cfinfil  24050  ufinffr  24086  fin1aufil  24089  alexsubALTlem2  24205  alexsubALTlem4  24207  ptcmplem2  24210  tsmsfbas  24285  xrge0gsumle  24991  xrge0tsms  24992  fta1  26469  uhgr0edgfi  29590  fusgrfisbase  29678  vtxdg0e  29824  wwlksnfi  30255  mptiffisupp  33038  hashxpe  33152  xrge0tsmsd  33393  elrgspnlem4  33565  0mplrim  33904  extvfvcl  33926  vieta  33970  esumnul  34438  esum0  34439  esumcst  34453  esumsnf  34454  esumpcvgval  34468  sibf0  34724  eulerpartlemt  34761  derang0  35661  topdifinffinlem  37993  matunitlindf  38269  0totbnd  38424  heiborlem6  38467  mzpcompact2lem  43482  rp-isfinite6  44244  0pwfi  45779  fouriercn  46946  rrxtopn0  47007  salexct  47048  sge0rnn0  47082  sge00  47090  sge0sn  47093  ovn0val  47264  ovn02  47282  hoidmv0val  47297  hoidmvle  47314  hoiqssbl  47339  von0val  47385  vonhoire  47386  vonioo  47396  vonicc  47399  vonsn  47405  lcoc0  49202  lco0  49207