Theorem 0fi 8990

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

Assertion

Ref	Expression
0fi	⊢ ∅ ∈ Fin

Proof of Theorem 0fi

Step	Hyp	Ref	Expression
1		peano1 7845	. . 3 ⊢ ∅ ∈ ω
2		eqid 2729	. . . 4 ⊢ ∅ = ∅
3		en0 8966	. . . 4 ⊢ (∅ ≈ ∅ ↔ ∅ = ∅)
4	2, 3	mpbir 231	. . 3 ⊢ ∅ ≈ ∅
5		breq2 5106	. . . 4 ⊢ (𝑥 = ∅ → (∅ ≈ 𝑥 ↔ ∅ ≈ ∅))
6	5	rspcev 3585	. . 3 ⊢ ((∅ ∈ ω ∧ ∅ ≈ ∅) → ∃𝑥 ∈ ω ∅ ≈ 𝑥)
7	1, 4, 6	mp2an 692	. 2 ⊢ ∃𝑥 ∈ ω ∅ ≈ 𝑥
8		isfi 8924	. 2 ⊢ (∅ ∈ Fin ↔ ∃𝑥 ∈ ω ∅ ≈ 𝑥)
9	7, 8	mpbir 231	1 ⊢ ∅ ∈ Fin

Syntax hints:   = wceq 1540   ∈ wcel 2109  ∃wrex 3053  ∅c0 4292   class class class wbr 5102  ωcom 7822   ≈ cen 8892  Fincfn 8895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-mo 2533  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-tr 5210  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 6323  df-on 6324  df-lim 6325  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-om 7823  df-en 8896  df-fin 8899

This theorem is referenced by:  snfi  8991  ssfi  9114  cnvfi  9117  fnfi  9119  nneneq  9147  nfielex  9194  imafiOLD  9241  xpfiOLD  9246  fodomfib  9256  iunfi  9270  fczfsuppd  9313  fsuppun  9314  0fsupp  9317  r1fin  9702  acndom  9980  numwdom  9988  ackbij1lem18  10165  sdom2en01  10231  fin23lem26  10254  isfin1-3  10315  gchxpidm  10598  fzfi  13913  fzofi  13915  hasheq0  14304  hashxp  14375  lcmf0  16580  0hashbc  16954  acsfn0  17601  isdrs2  18247  fpwipodrs  18481  symgfisg  19382  dsmm0cl  21682  mplsubg  21944  mpllss  21945  psrbag0  22002  mat0dimbas0  22386  mat0dim0  22387  mat0dimid  22388  mat0dimscm  22389  mat0dimcrng  22390  mat0scmat  22458  mavmul0  22472  mavmul0g  22473  mdet0pr  22512  m1detdiag  22517  d0mat2pmat  22658  chpmat0d  22754  fctop  22924  cmpfi  23328  bwth  23330  comppfsc  23452  ptbasid  23495  cfinfil  23813  ufinffr  23849  fin1aufil  23852  alexsubALTlem2  23968  alexsubALTlem4  23970  ptcmplem2  23973  tsmsfbas  24048  xrge0gsumle  24755  xrge0tsms  24756  fta1  26249  uhgr0edgfi  29220  fusgrfisbase  29308  vtxdg0e  29455  wwlksnfi  29886  mptiffisupp  32666  hashxpe  32782  xrge0tsmsd  33045  elrgspnlem4  33212  esumnul  34031  esum0  34032  esumcst  34046  esumsnf  34047  esumpcvgval  34061  sibf0  34318  eulerpartlemt  34355  derang0  35149  topdifinffinlem  37328  matunitlindf  37605  0totbnd  37760  heiborlem6  37803  mzpcompact2lem  42732  rp-isfinite6  43500  0pwfi  45046  fouriercn  46223  rrxtopn0  46284  salexct  46325  sge0rnn0  46359  sge00  46367  sge0sn  46370  ovn0val  46541  ovn02  46559  hoidmv0val  46574  hoidmvle  46591  hoiqssbl  46616  von0val  46662  vonhoire  46663  vonioo  46673  vonicc  46676  vonsn  46682  lcoc0  48404  lco0  48409