Theorem fzfi 13341

Description: A finite interval of integers is finite. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Mar-2015.)

Assertion

Ref	Expression
fzfi	⊢ (𝑀...𝑁) ∈ Fin

Proof of Theorem fzfi

Step	Hyp	Ref	Expression
1		0fin 8746	. . 3 ⊢ ∅ ∈ Fin
2		eleq1 2900	. . 3 ⊢ ((𝑀...𝑁) = ∅ → ((𝑀...𝑁) ∈ Fin ↔ ∅ ∈ Fin))
3	1, 2	mpbiri 260	. 2 ⊢ ((𝑀...𝑁) = ∅ → (𝑀...𝑁) ∈ Fin)
4		fzn0 12922	. . 3 ⊢ ((𝑀...𝑁) ≠ ∅ ↔ 𝑁 ∈ (ℤ≥‘𝑀))
5		onfin2 8710	. . . . . 6 ⊢ ω = (On ∩ Fin)
6		inss2 4206	. . . . . 6 ⊢ (On ∩ Fin) ⊆ Fin
7	5, 6	eqsstri 4001	. . . . 5 ⊢ ω ⊆ Fin
8		eqid 2821	. . . . . . 7 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
9	8	hashgf1o 13340	. . . . . 6 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
10		peano2uz 12302	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
11		uznn0sub 12278	. . . . . . 7 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
12	10, 11	syl 17	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
13		f1ocnvdm 7041	. . . . . 6 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0 ∧ ((𝑁 + 1) − 𝑀) ∈ ℕ0) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
14	9, 12, 13	sylancr 589	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
15	7, 14	sseldi 3965	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin)
16	8	fzen2 13338	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)))
17		enfii 8735	. . . 4 ⊢ (((◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin ∧ (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀))) → (𝑀...𝑁) ∈ Fin)
18	15, 16, 17	syl2anc 586	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ∈ Fin)
19	4, 18	sylbi 219	. 2 ⊢ ((𝑀...𝑁) ≠ ∅ → (𝑀...𝑁) ∈ Fin)
20	3, 19	pm2.61ine 3100	1 ⊢ (𝑀...𝑁) ∈ Fin

Syntax hints:   = wceq 1537   ∈ wcel 2114   ≠ wne 3016  Vcvv 3494   ∩ cin 3935  ∅c0 4291   class class class wbr 5066   ↦ cmpt 5146  ^◡ccnv 5554   ↾ cres 5557  Oncon0 6191  –1-1-onto→wf1o 6354  ‘cfv 6355  (class class class)co 7156  ωcom 7580  reccrdg 8045   ≈ cen 8506  Fincfn 8509  0cc0 10537  1c1 10538   + caddc 10540   − cmin 10870  ℕ₀cn0 11898  ℤ_≥cuz 12244  ...cfz 12893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-1st 7689  df-2nd 7690  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-1o 8102  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-fin 8513  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-nn 11639  df-n0 11899  df-z 11983  df-uz 12245  df-fz 12894

This theorem is referenced by:  fzfid  13342  fzofi  13343  fsequb  13344  fsequb2  13345  fseqsupcl  13346  ssnn0fi  13354  seqf1o  13412  isfinite4  13724  hashdom  13741  fzsdom2  13790  fnfz0hashnn0  13807  seqcoll2  13824  caubnd  14718  limsupgre  14838  summolem3  15071  summolem2  15073  zsum  15075  prodmolem3  15287  prodmolem2  15289  zprod  15291  risefallfac  15378  bpolylem  15402  phicl2  16105  phibnd  16108  hashdvds  16112  phiprmpw  16113  eulerth  16120  phisum  16127  pcfac  16235  prmreclem2  16253  prmreclem3  16254  prmreclem4  16255  prmreclem5  16256  prmrec  16258  1arith  16263  vdwlem6  16322  vdwlem10  16326  vdwlem12  16328  prmdvdsprmo  16378  prmgaplcmlem1  16387  prmgaplcm  16396  isstruct2  16493  gsumval3lem1  19025  gsumval3lem2  19026  gsumval3  19027  coe1mul2  20437  ehleudis  24021  ehleudisval  24022  ovoliunlem2  24104  uniioombllem6  24189  itg0  24380  itgz  24381  coemullem  24840  aannenlem1  24917  aannenlem2  24918  birthdaylem1  25529  birthdaylem2  25530  wilthlem2  25646  wilthlem3  25647  ftalem5  25654  ppifi  25683  prmdvdsfi  25684  chtdif  25735  ppidif  25740  chp1  25744  ppiltx  25754  prmorcht  25755  mumul  25758  sqff1o  25759  ppiub  25780  pclogsum  25791  logexprlim  25801  gausslemma2dlem1  25942  gausslemma2dlem5  25947  gausslemma2dlem6  25948  lgseisenlem2  25952  axlowdimlem16  26743  konigsberglem5  28035  pmtrto1cl  30741  psgnfzto1stlem  30742  fzto1st  30745  psgnfzto1st  30747  smatcl  31067  1smat1  31069  esumpcvgval  31337  esumcvg  31345  carsggect  31576  carsgclctunlem2  31577  oddpwdc  31612  eulerpartlemb  31626  ballotlem1  31744  ballotlem2  31746  ballotlemfelz  31748  ballotlemfp1  31749  ballotlemfc0  31750  ballotlemfcc  31751  ballotlemfmpn  31752  ballotlemiex  31759  ballotlemsup  31762  ballotlemfg  31783  ballotlemfrc  31784  ballotlemfrceq  31786  ballotth  31795  plymulx0  31817  fsum2dsub  31878  reprfi2  31894  breprexpnat  31905  hgt750lemb  31927  hgt750leme  31929  pthhashvtx  32374  subfacf  32422  subfacp1lem1  32426  subfacp1lem3  32429  subfacp1lem5  32431  subfacp1lem6  32432  erdszelem2  32439  erdszelem10  32447  cvmliftlem15  32545  bcprod  32970  ptrecube  34907  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  poimirlem28  34935  poimirlem29  34936  poimirlem30  34937  poimirlem31  34938  poimirlem32  34939  mblfinlem2  34945  volsupnfl  34952  itg2addnclem2  34959  nnubfi  35040  nninfnub  35041  cntotbnd  35089  eldioph2lem1  39377  eldioph2lem2  39378  eldioph2  39379  pellexlem5  39450  pellex  39452  jm2.22  39612  jm2.23  39613  hbt  39750  rp-isfinite6  39904  fzisoeu  41587  sumnnodd  41931  stoweidlem37  42342  stoweidlem44  42349  stoweidlem59  42364  fourierdlem37  42449  fourierdlem103  42514  fourierdlem104  42515  etransclem16  42555  etransclem24  42563  etransclem25  42564  etransclem33  42572  etransclem35  42574  etransclem44  42583  etransclem45  42584  sge0reuz  42749  hoidmvlelem2  42898  aacllem  44922