Theorem 0fi 9023

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

Assertion

Ref	Expression
0fi	⊢ ∅ ∈ Fin

Proof of Theorem 0fi

Step	Hyp	Ref	Expression
1		peano1 7869	. . 3 ⊢ ∅ ∈ ω
2		eqid 2762	. . . 4 ⊢ ∅ = ∅
3		en0 8999	. . . 4 ⊢ (∅ ≈ ∅ ↔ ∅ = ∅)
4	2, 3	mpbir 233	. . 3 ⊢ ∅ ≈ ∅
5		breq2 5104	. . . 4 ⊢ (𝑥 = ∅ → (∅ ≈ 𝑥 ↔ ∅ ≈ ∅))
6	5	rspcev 3581	. . 3 ⊢ ((∅ ∈ ω ∧ ∅ ≈ ∅) → ∃𝑥 ∈ ω ∅ ≈ 𝑥)
7	1, 4, 6	mp2an 702	. 2 ⊢ ∃𝑥 ∈ ω ∅ ≈ 𝑥
8		isfi 8956	. 2 ⊢ (∅ ∈ Fin ↔ ∃𝑥 ∈ ω ∅ ≈ 𝑥)
9	7, 8	mpbir 233	1 ⊢ ∅ ∈ Fin

Syntax hints:   = wceq 1560   ∈ wcel 2142  ∃wrex 3086  ∅c0 4285   class class class wbr 5100  ωcom 7846   ≈ cen 8924  Fincfn 8927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-mo 2566  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-ord 6349  df-on 6350  df-lim 6351  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-om 7847  df-en 8928  df-fin 8931

This theorem is referenced by:  snfi  9024  ssfi  9141  cnvfi  9144  fnfi  9146  nneneq  9174  nfielex  9218  imafiOLD  9260  fodomfib  9273  iunfi  9286  fczfsuppd  9332  fsuppun  9333  0fsupp  9336  r1fin  9731  acndom  10007  numwdom  10015  ackbij1lem18  10192  sdom2en01  10259  fin23lem26  10282  isfin1-3  10343  gchxpidm  10627  fzfi  13985  fzofi  13987  hasheq0  14376  hashxp  14447  lcmf0  16668  0hashbc  17043  acsfn0  17692  isdrs2  18338  fpwipodrs  18572  symgfisg  19508  dsmm0cl  21789  mplsubg  22050  mpllss  22051  psrbag0  22112  mat0dimbas0  22523  mat0dim0  22524  mat0dimid  22525  mat0dimscm  22526  mat0dimcrng  22527  mat0scmat  22595  mavmul0  22609  mavmul0g  22610  mdet0pr  22649  m1detdiag  22654  d0mat2pmat  22795  chpmat0d  22891  fctop  23061  cmpfi  23465  bwth  23467  comppfsc  23589  ptbasid  23632  cfinfil  23950  ufinffr  23986  fin1aufil  23989  alexsubALTlem2  24105  alexsubALTlem4  24107  ptcmplem2  24110  tsmsfbas  24185  xrge0gsumle  24891  xrge0tsms  24892  fta1  26369  uhgr0edgfi  29438  fusgrfisbase  29526  vtxdg0e  29672  wwlksnfi  30103  mptiffisupp  32892  hashxpe  33006  xrge0tsmsd  33250  elrgspnlem4  33423  0mplrim  33808  extvfvcl  33830  vieta  33874  esumnul  34342  esum0  34343  esumcst  34357  esumsnf  34358  esumpcvgval  34372  sibf0  34628  eulerpartlemt  34665  derang0  35516  topdifinffinlem  37838  matunitlindf  38114  0totbnd  38269  heiborlem6  38312  mzpcompact2lem  43329  rp-isfinite6  44091  0pwfi  45636  fouriercn  46803  rrxtopn0  46864  salexct  46905  sge0rnn0  46939  sge00  46947  sge0sn  46950  ovn0val  47121  ovn02  47139  hoidmv0val  47154  hoidmvle  47171  hoiqssbl  47196  von0val  47242  vonhoire  47243  vonioo  47253  vonicc  47256  vonsn  47262  lcoc0  49041  lco0  49046