Theorem 0fi 9063

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

Assertion

Ref	Expression
0fi	⊢ ∅ ∈ Fin

Proof of Theorem 0fi

Step	Hyp	Ref	Expression
1		peano1 7898	. . 3 ⊢ ∅ ∈ ω
2		eqid 2761	. . . 4 ⊢ ∅ = ∅
3		en0 9038	. . . 4 ⊢ (∅ ≈ ∅ ↔ ∅ = ∅)
4	2, 3	mpbir 234	. . 3 ⊢ ∅ ≈ ∅
5		breq2 5107	. . . 4 ⊢ (𝑥 = ∅ → (∅ ≈ 𝑥 ↔ ∅ ≈ ∅))
6	5	rspcev 3577	. . 3 ⊢ ((∅ ∈ ω ∧ ∅ ≈ ∅) → ∃𝑥 ∈ ω ∅ ≈ 𝑥)
7	1, 4, 6	mp2an 705	. 2 ⊢ ∃𝑥 ∈ ω ∅ ≈ 𝑥
8		isfi 8995	. 2 ⊢ (∅ ∈ Fin ↔ ∃𝑥 ∈ ω ∅ ≈ 𝑥)
9	7, 8	mpbir 234	1 ⊢ ∅ ∈ Fin

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  ∃wrex 3087  ∅c0 4279   class class class wbr 5103  ωcom 7875   ≈ cen 8963  Fincfn 8966

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2100  df-mo 2565  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-ord 6364  df-on 6365  df-lim 6366  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-om 7876  df-en 8967  df-fin 8970

This theorem is used by:  snfi  9064  ssfi  9181  cnvfi  9184  fnfi  9186  nneneq  9214  nfielex  9258  fodomfib  9313  iunfi  9325  fczfsuppd  9371  fsuppun  9372  0fsupp  9375  r1fin  9773  acndom  10123  numwdom  10131  ackbij1lem18  10307  sdom2en01  10373  fin23lem26  10396  isfin1-3  10457  gchxpidm  10747  fzfi  14108  fzofi  14110  hasheq0  14500  hashxp  14572  lcmf0  16802  0hashbc  17178  acsfn0  17827  isdrs2  18473  fpwipodrs  18707  symgfisg  19675  dsmm0cl  22039  mplsubg  22302  mpllss  22303  psrbag0  22364  mat0dimbas0  22774  mat0dim0  22775  mat0dimid  22776  mat0dimscm  22777  mat0dimcrng  22778  mat0scmat  22846  mavmul0  22860  mavmul0g  22861  mdet0pr  22900  m1detdiag  22905  matunitlindf  22989  d0mat2pmat  23049  chpmat0d  23145  fctop  23315  cmpfi  23719  bwth  23721  comppfsc  23844  ptbasid  23887  cfinfil  24205  ufinffr  24241  fin1aufil  24244  alexsubALTlem2  24360  alexsubALTlem4  24362  ptcmplem2  24365  tsmsfbas  24440  xrge0gsumle  25146  xrge0tsms  25147  fta1  26622  uhgr0edgfi  29814  fusgrfisbase  29902  vtxdg0e  30048  wwlksnfi  30488  mptiffisupp  33279  hashxpe  33392  xrge0tsmsd  33627  elrgspnlem4  33799  0mplrim  34139  extvfvcl  34161  vieta  34205  esumnul  34673  esum0  34674  esumcst  34688  esumsnf  34689  esumpcvgval  34703  sibf0  34959  eulerpartlemt  34996  derang0  35913  topdifinffinlem  38250  0totbnd  38687  heiborlem6  38730  mzpcompact2lem  43741  rp-isfinite6  44503  0pwfi  46045  fouriercn  47211  rrxtopn0  47272  salexct  47313  sge0rnn0  47347  sge00  47355  sge0sn  47358  ovn0val  47529  ovn02  47547  hoidmv0val  47562  hoidmvle  47579  hoiqssbl  47604  von0val  47650  vonhoire  47651  vonioo  47661  vonicc  47664  vonsn  47670  lcoc0  49503  lco0  49508