Theorem fzfi 13988

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		0fi 9054	. . 3 ⊢ ∅ ∈ Fin
2		eleq1 2822	. . 3 ⊢ ((𝑀...𝑁) = ∅ → ((𝑀...𝑁) ∈ Fin ↔ ∅ ∈ Fin))
3	1, 2	mpbiri 258	. 2 ⊢ ((𝑀...𝑁) = ∅ → (𝑀...𝑁) ∈ Fin)
4		fzn0 13553	. . 3 ⊢ ((𝑀...𝑁) ≠ ∅ ↔ 𝑁 ∈ (ℤ≥‘𝑀))
5		onfin2 9238	. . . . . 6 ⊢ ω = (On ∩ Fin)
6		inss2 4213	. . . . . 6 ⊢ (On ∩ Fin) ⊆ Fin
7	5, 6	eqsstri 4005	. . . . 5 ⊢ ω ⊆ Fin
8		eqid 2735	. . . . . . 7 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
9	8	hashgf1o 13987	. . . . . 6 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
10		peano2uz 12915	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
11		uznn0sub 12889	. . . . . . 7 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
12	10, 11	syl 17	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
13		f1ocnvdm 7277	. . . . . 6 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0 ∧ ((𝑁 + 1) − 𝑀) ∈ ℕ0) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
14	9, 12, 13	sylancr 587	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
15	7, 14	sselid 3956	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin)
16	8	fzen2 13985	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)))
17		enfii 9198	. . . 4 ⊢ (((◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin ∧ (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀))) → (𝑀...𝑁) ∈ Fin)
18	15, 16, 17	syl2anc 584	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ∈ Fin)
19	4, 18	sylbi 217	. 2 ⊢ ((𝑀...𝑁) ≠ ∅ → (𝑀...𝑁) ∈ Fin)
20	3, 19	pm2.61ine 3015	1 ⊢ (𝑀...𝑁) ∈ Fin

Syntax hints:   = wceq 1540   ∈ wcel 2108   ≠ wne 2932  Vcvv 3459   ∩ cin 3925  ∅c0 4308   class class class wbr 5119   ↦ cmpt 5201  ^◡ccnv 5653   ↾ cres 5656  Oncon0 6352  –1-1-onto→wf1o 6529  ‘cfv 6530  (class class class)co 7403  ωcom 7859  reccrdg 8421   ≈ cen 8954  Fincfn 8957  0cc0 11127  1c1 11128   + caddc 11130   − cmin 11464  ℕ₀cn0 12499  ℤ_≥cuz 12850  ...cfz 13522

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

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-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-om 7860  df-1st 7986  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-1o 8478  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11466  df-neg 11467  df-nn 12239  df-n0 12500  df-z 12587  df-uz 12851  df-fz 13523

This theorem is referenced by:  fzfid  13989  fzofi  13990  fsequb  13991  fsequb2  13992  fseqsupcl  13993  ssnn0fi  14001  seqf1o  14059  isfinite4  14378  hashdom  14395  fzsdom2  14444  fnfz0hashnn0  14464  seqcoll2  14481  caubnd  15375  limsupgre  15495  summolem3  15728  summolem2  15730  zsum  15732  prodmolem3  15947  prodmolem2  15949  zprod  15951  risefallfac  16038  bpolylem  16062  phicl2  16785  phibnd  16788  hashdvds  16792  phiprmpw  16793  eulerth  16800  pcfac  16917  prmreclem2  16935  prmreclem3  16936  prmreclem4  16937  prmreclem5  16938  prmrec  16940  1arith  16945  vdwlem6  17004  vdwlem10  17008  vdwlem12  17010  prmdvdsprmo  17060  prmgaplcmlem1  17069  prmgaplcm  17078  isstruct2  17166  gsumval3lem1  19884  gsumval3lem2  19885  gsumval3  19886  coe1mul2  22204  ehleudis  25368  ehleudisval  25369  ovoliunlem2  25454  uniioombllem6  25539  itg0  25731  itgz  25732  coemullem  26205  aannenlem1  26286  aannenlem2  26287  birthdaylem1  26911  birthdaylem2  26912  wilthlem2  27029  wilthlem3  27030  ftalem5  27037  ppifi  27066  prmdvdsfi  27067  chtdif  27118  ppidif  27123  chp1  27127  ppiltx  27137  prmorcht  27138  mumul  27141  sqff1o  27142  ppiub  27165  pclogsum  27176  logexprlim  27186  gausslemma2dlem1  27327  gausslemma2dlem5  27332  gausslemma2dlem6  27333  lgseisenlem2  27337  axlowdimlem16  28882  konigsberglem5  30183  pmtrto1cl  33056  psgnfzto1stlem  33057  fzto1st  33060  psgnfzto1st  33062  smatcl  33779  1smat1  33781  esumpcvgval  34055  esumcvg  34063  carsggect  34296  carsgclctunlem2  34297  oddpwdc  34332  eulerpartlemb  34346  ballotlem1  34465  ballotlem2  34467  ballotlemfelz  34469  ballotlemfp1  34470  ballotlemfc0  34471  ballotlemfcc  34472  ballotlemfmpn  34473  ballotlemiex  34480  ballotlemsup  34483  ballotlemfg  34504  ballotlemfrc  34505  ballotlemfrceq  34507  ballotth  34516  plymulx0  34525  fsum2dsub  34585  reprfi2  34601  breprexpnat  34612  hgt750lemb  34634  hgt750leme  34636  pthhashvtx  35096  subfacf  35143  subfacp1lem1  35147  subfacp1lem3  35150  subfacp1lem5  35152  subfacp1lem6  35153  erdszelem2  35160  erdszelem10  35168  cvmliftlem15  35266  bcprod  35701  ptrecube  37590  poimirlem25  37615  poimirlem26  37616  poimirlem27  37617  poimirlem28  37618  poimirlem29  37619  poimirlem30  37620  poimirlem31  37621  poimirlem32  37622  mblfinlem2  37628  volsupnfl  37635  itg2addnclem2  37642  nnubfi  37720  nninfnub  37721  cntotbnd  37766  lcmfunnnd  41971  lcmineqlem4  41991  lcmineqlem6  41993  lcmineqlem15  42002  lcmineqlem16  42003  lcmineqlem19  42006  lcmineqlem20  42007  lcmineqlem21  42008  lcmineqlem22  42009  sticksstones17  42122  fisdomnn  42242  fz1sumconst  42305  eldioph2lem1  42730  eldioph2lem2  42731  eldioph2  42732  pellexlem5  42803  pellex  42805  jm2.22  42966  jm2.23  42967  hbt  43101  rp-isfinite6  43489  fzisoeu  45277  sumnnodd  45607  stoweidlem37  46014  stoweidlem44  46021  stoweidlem59  46036  fourierdlem37  46121  fourierdlem103  46186  fourierdlem104  46187  etransclem16  46227  etransclem24  46235  etransclem25  46236  etransclem33  46244  etransclem35  46246  etransclem44  46255  etransclem45  46256  sge0reuz  46424  hoidmvlelem2  46573  aacllem  49613