Theorem 0fi 9080

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

Assertion

Ref	Expression
0fi	⊢ ∅ ∈ Fin

Proof of Theorem 0fi

Step	Hyp	Ref	Expression
1		peano1 7910	. . 3 ⊢ ∅ ∈ ω
2		eqid 2734	. . . 4 ⊢ ∅ = ∅
3		en0 9056	. . . 4 ⊢ (∅ ≈ ∅ ↔ ∅ = ∅)
4	2, 3	mpbir 231	. . 3 ⊢ ∅ ≈ ∅
5		breq2 5151	. . . 4 ⊢ (𝑥 = ∅ → (∅ ≈ 𝑥 ↔ ∅ ≈ ∅))
6	5	rspcev 3621	. . 3 ⊢ ((∅ ∈ ω ∧ ∅ ≈ ∅) → ∃𝑥 ∈ ω ∅ ≈ 𝑥)
7	1, 4, 6	mp2an 692	. 2 ⊢ ∃𝑥 ∈ ω ∅ ≈ 𝑥
8		isfi 9014	. 2 ⊢ (∅ ∈ Fin ↔ ∃𝑥 ∈ ω ∅ ≈ 𝑥)
9	7, 8	mpbir 231	1 ⊢ ∅ ∈ Fin

Syntax hints:   = wceq 1536   ∈ wcel 2105  ∃wrex 3067  ∅c0 4338   class class class wbr 5147  ωcom 7886   ≈ cen 8980  Fincfn 8983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-mo 2537  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-ord 6388  df-on 6389  df-lim 6390  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-om 7887  df-en 8984  df-fin 8987

This theorem is referenced by:  snfi  9081  ssfi  9211  cnvfi  9214  fnfi  9215  nneneq  9243  nfielex  9304  imafiOLD  9351  xpfiOLD  9356  fodomfib  9366  iunfi  9380  fczfsuppd  9423  fsuppun  9424  0fsupp  9427  r1fin  9810  acndom  10088  numwdom  10096  ackbij1lem18  10273  sdom2en01  10339  fin23lem26  10362  isfin1-3  10423  gchxpidm  10706  fzfi  14009  fzofi  14011  hasheq0  14398  hashxp  14469  lcmf0  16667  0hashbc  17040  acsfn0  17704  isdrs2  18363  fpwipodrs  18597  symgfisg  19500  dsmm0cl  21777  mplsubg  22039  mpllss  22040  psrbag0  22103  mat0dimbas0  22487  mat0dim0  22488  mat0dimid  22489  mat0dimscm  22490  mat0dimcrng  22491  mat0scmat  22559  mavmul0  22573  mavmul0g  22574  mdet0pr  22613  m1detdiag  22618  d0mat2pmat  22759  chpmat0d  22855  fctop  23026  cmpfi  23431  bwth  23433  comppfsc  23555  ptbasid  23598  cfinfil  23916  ufinffr  23952  fin1aufil  23955  alexsubALTlem2  24071  alexsubALTlem4  24073  ptcmplem2  24076  tsmsfbas  24151  xrge0gsumle  24868  xrge0tsms  24869  fta1  26364  uhgr0edgfi  29271  fusgrfisbase  29359  vtxdg0e  29506  wwlksnfi  29935  mptiffisupp  32707  hashxpe  32816  xrge0tsmsd  33047  elrgspnlem4  33234  esumnul  34028  esum0  34029  esumcst  34043  esumsnf  34044  esumpcvgval  34058  sibf0  34315  eulerpartlemt  34352  derang0  35153  topdifinffinlem  37329  matunitlindf  37604  0totbnd  37759  heiborlem6  37802  mzpcompact2lem  42738  rp-isfinite6  43507  0pwfi  44998  fouriercn  46187  rrxtopn0  46248  salexct  46289  sge0rnn0  46323  sge00  46331  sge0sn  46334  ovn0val  46505  ovn02  46523  hoidmv0val  46538  hoidmvle  46555  hoiqssbl  46580  von0val  46626  vonhoire  46627  vonioo  46637  vonicc  46640  vonsn  46646  lcoc0  48267  lco0  48272