Theorem 0fi 8989

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

Assertion

Ref	Expression
0fi	⊢ ∅ ∈ Fin

Proof of Theorem 0fi

Step	Hyp	Ref	Expression
1		peano1 7840	. . 3 ⊢ ∅ ∈ ω
2		eqid 2736	. . . 4 ⊢ ∅ = ∅
3		en0 8965	. . . 4 ⊢ (∅ ≈ ∅ ↔ ∅ = ∅)
4	2, 3	mpbir 231	. . 3 ⊢ ∅ ≈ ∅
5		breq2 5089	. . . 4 ⊢ (𝑥 = ∅ → (∅ ≈ 𝑥 ↔ ∅ ≈ ∅))
6	5	rspcev 3564	. . 3 ⊢ ((∅ ∈ ω ∧ ∅ ≈ ∅) → ∃𝑥 ∈ ω ∅ ≈ 𝑥)
7	1, 4, 6	mp2an 693	. 2 ⊢ ∃𝑥 ∈ ω ∅ ≈ 𝑥
8		isfi 8922	. 2 ⊢ (∅ ∈ Fin ↔ ∃𝑥 ∈ ω ∅ ≈ 𝑥)
9	7, 8	mpbir 231	1 ⊢ ∅ ∈ Fin

Syntax hints:   = wceq 1542   ∈ wcel 2114  ∃wrex 3061  ∅c0 4273   class class class wbr 5085  ωcom 7817   ≈ cen 8890  Fincfn 8893

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

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 2539  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-ord 6326  df-on 6327  df-lim 6328  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-om 7818  df-en 8894  df-fin 8897

This theorem is referenced by:  snfi  8990  ssfi  9107  cnvfi  9110  fnfi  9112  nneneq  9140  nfielex  9184  imafiOLD  9226  fodomfib  9239  iunfi  9253  fczfsuppd  9299  fsuppun  9300  0fsupp  9303  r1fin  9697  acndom  9973  numwdom  9981  ackbij1lem18  10158  sdom2en01  10224  fin23lem26  10247  isfin1-3  10308  gchxpidm  10592  fzfi  13934  fzofi  13936  hasheq0  14325  hashxp  14396  lcmf0  16603  0hashbc  16978  acsfn0  17626  isdrs2  18272  fpwipodrs  18506  symgfisg  19443  dsmm0cl  21720  mplsubg  21980  mpllss  21981  psrbag0  22040  mat0dimbas0  22431  mat0dim0  22432  mat0dimid  22433  mat0dimscm  22434  mat0dimcrng  22435  mat0scmat  22503  mavmul0  22517  mavmul0g  22518  mdet0pr  22557  m1detdiag  22562  d0mat2pmat  22703  chpmat0d  22799  fctop  22969  cmpfi  23373  bwth  23375  comppfsc  23497  ptbasid  23540  cfinfil  23858  ufinffr  23894  fin1aufil  23897  alexsubALTlem2  24013  alexsubALTlem4  24015  ptcmplem2  24018  tsmsfbas  24093  xrge0gsumle  24799  xrge0tsms  24800  fta1  26274  uhgr0edgfi  29309  fusgrfisbase  29397  vtxdg0e  29543  wwlksnfi  29974  mptiffisupp  32766  hashxpe  32880  xrge0tsmsd  33134  elrgspnlem4  33306  extvfvcl  33680  vieta  33724  esumnul  34192  esum0  34193  esumcst  34207  esumsnf  34208  esumpcvgval  34222  sibf0  34478  eulerpartlemt  34515  derang0  35351  topdifinffinlem  37663  matunitlindf  37939  0totbnd  38094  heiborlem6  38137  mzpcompact2lem  43183  rp-isfinite6  43945  0pwfi  45490  fouriercn  46660  rrxtopn0  46721  salexct  46762  sge0rnn0  46796  sge00  46804  sge0sn  46807  ovn0val  46978  ovn02  46996  hoidmv0val  47011  hoidmvle  47028  hoiqssbl  47053  von0val  47099  vonhoire  47100  vonioo  47110  vonicc  47113  vonsn  47119  lcoc0  48898  lco0  48903