Theorem 0fi 9049

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

Assertion

Ref	Expression
0fi	⊢ ∅ ∈ Fin

Proof of Theorem 0fi

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  ∃wrex 3086  ∅c0 4279   class class class wbr 5103  ωcom 7862   ≈ cen 8949  Fincfn 8952

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 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

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 2564  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-ord 6360  df-on 6361  df-lim 6362  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-om 7863  df-en 8953  df-fin 8956

This theorem is used by:  snfi  9050  ssfi  9167  cnvfi  9170  fnfi  9172  nneneq  9200  nfielex  9244  fodomfib  9298  iunfi  9310  fczfsuppd  9356  fsuppun  9357  0fsupp  9360  r1fin  9755  acndom  10054  numwdom  10062  ackbij1lem18  10238  sdom2en01  10304  fin23lem26  10327  isfin1-3  10388  gchxpidm  10678  fzfi  14036  fzofi  14038  hasheq0  14427  hashxp  14499  lcmf0  16724  0hashbc  17099  acsfn0  17748  isdrs2  18394  fpwipodrs  18628  symgfisg  19595  dsmm0cl  21953  mplsubg  22216  mpllss  22217  psrbag0  22278  mat0dimbas0  22688  mat0dim0  22689  mat0dimid  22690  mat0dimscm  22691  mat0dimcrng  22692  mat0scmat  22760  mavmul0  22774  mavmul0g  22775  mdet0pr  22814  m1detdiag  22819  matunitlindf  22903  d0mat2pmat  22963  chpmat0d  23059  fctop  23229  cmpfi  23633  bwth  23635  comppfsc  23758  ptbasid  23801  cfinfil  24119  ufinffr  24155  fin1aufil  24158  alexsubALTlem2  24274  alexsubALTlem4  24276  ptcmplem2  24279  tsmsfbas  24354  xrge0gsumle  25060  xrge0tsms  25061  fta1  26538  uhgr0edgfi  29700  fusgrfisbase  29788  vtxdg0e  29934  wwlksnfi  30374  mptiffisupp  33165  hashxpe  33278  xrge0tsmsd  33513  elrgspnlem4  33685  0mplrim  34024  extvfvcl  34046  vieta  34090  esumnul  34558  esum0  34559  esumcst  34573  esumsnf  34574  esumpcvgval  34588  sibf0  34845  eulerpartlemt  34882  derang0  35748  topdifinffinlem  38101  0totbnd  38523  heiborlem6  38566  mzpcompact2lem  43596  rp-isfinite6  44358  0pwfi  45893  fouriercn  47060  rrxtopn0  47121  salexct  47162  sge0rnn0  47196  sge00  47204  sge0sn  47207  ovn0val  47378  ovn02  47396  hoidmv0val  47411  hoidmvle  47428  hoiqssbl  47453  von0val  47499  vonhoire  47500  vonioo  47510  vonicc  47513  vonsn  47519  lcoc0  49352  lco0  49357