Theorem fzfi 14008

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 9039	. . 3 ⊢ ∅ ∈ Fin
2		eleq1 2857	. . 3 ⊢ ((𝑀...𝑁) = ∅ → ((𝑀...𝑁) ∈ Fin ↔ ∅ ∈ Fin))
3	1, 2	mpbiri 261	. 2 ⊢ ((𝑀...𝑁) = ∅ → (𝑀...𝑁) ∈ Fin)
4		fzn0 13566	. . 3 ⊢ ((𝑀...𝑁) ≠ ∅ ↔ 𝑁 ∈ (ℤ≥‘𝑀))
5		onfin2 9201	. . . . . 6 ⊢ ω = (On ∩ Fin)
6		inss2 4196	. . . . . 6 ⊢ (On ∩ Fin) ⊆ Fin
7	5, 6	eqsstri 3989	. . . . 5 ⊢ ω ⊆ Fin
8		eqid 2769	. . . . . . 7 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
9	8	hashgf1o 14007	. . . . . 6 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
10		peano2uz 12925	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
11		uznn0sub 12897	. . . . . . 7 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
12	10, 11	syl 18	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
13		f1ocnvdm 7284	. . . . . 6 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0 ∧ ((𝑁 + 1) − 𝑀) ∈ ℕ0) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
14	9, 12, 13	sylancr 598	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
15	7, 14	sselid 3941	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin)
16	8	fzen2 14005	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)))
17		enfii 9170	. . . 4 ⊢ (((◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin ∧ (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀))) → (𝑀...𝑁) ∈ Fin)
18	15, 16, 17	syl2anc 595	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ∈ Fin)
19	4, 18	sylbi 220	. 2 ⊢ ((𝑀...𝑁) ≠ ∅ → (𝑀...𝑁) ∈ Fin)
20	3, 19	pm2.61ine 3047	1 ⊢ (𝑀...𝑁) ∈ Fin

Syntax hints:   = wceq 1567   ∈ wcel 2149   ≠ wne 2964  Vcvv 3461   ∩ cin 3910  ∅c0 4292   class class class wbr 5111   ↦ cmpt 5194  ^◡ccnv 5661   ↾ cres 5664  Oncon0 6361  –1-1-onto→wf1o 6536  ‘cfv 6537  (class class class)co 7411  ωcom 7862  reccrdg 8396   ≈ cen 8940  Fincfn 8943  0cc0 11100  1c1 11101   + caddc 11103   − cmin 11441  ℕ₀cn0 12504  ℤ_≥cuz 12862  ...cfz 13535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5259  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-cnex 11156  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-addrcl 11161  ax-mulcl 11162  ax-mulrcl 11163  ax-mulcom 11164  ax-addass 11165  ax-mulass 11166  ax-distr 11167  ax-i2m1 11168  ax-1ne0 11169  ax-1rid 11170  ax-rnegex 11171  ax-rrecex 11172  ax-cnre 11173  ax-pre-lttri 11174  ax-pre-lttrn 11175  ax-pre-ltadd 11176  ax-pre-mulgt0 11177

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3376  df-rab 3423  df-v 3463  df-sbc 3752  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7863  df-1st 7986  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-rdg 8397  df-1o 8453  df-er 8694  df-en 8944  df-dom 8945  df-sdom 8946  df-fin 8947  df-pnf 11245  df-mnf 11246  df-xr 11247  df-ltxr 11248  df-le 11249  df-sub 11443  df-neg 11444  df-nn 12234  df-n0 12505  df-z 12592  df-uz 12863  df-fz 13536

This theorem is referenced by:  fzfid  14009  fzofi  14010  fsequb  14011  fsequb2  14012  fseqsupcl  14013  ssnn0fi  14021  seqf1o  14079  isfinite4  14398  hashdom  14415  fzsdom2  14465  fnfz0hashnn0  14485  seqcoll2  14502  caubnd  15410  limsupgre  15532  summolem3  15765  summolem2  15767  zsum  15769  prodmolem3  15987  prodmolem2  15989  zprod  15991  risefallfac  16078  bpolylem  16102  phicl2  16827  phibnd  16830  hashdvds  16834  phiprmpw  16835  eulerth  16842  pcfac  16959  prmreclem2  16977  prmreclem3  16978  prmreclem4  16979  prmreclem5  16980  prmrec  16982  1arith  16987  vdwlem6  17046  vdwlem10  17050  vdwlem12  17052  prmdvdsprmo  17102  prmgaplcmlem1  17111  prmgaplcm  17120  isstruct2  17209  gsumval3lem1  19975  gsumval3lem2  19976  gsumval3  19977  coe1mul2  22399  ehleudis  25546  ehleudisval  25547  ovoliunlem2  25631  uniioombllem6  25716  itg0  25908  itgz  25909  coemullem  26376  plyn0mulidp  26411  aannenlem1  26458  aannenlem2  26459  birthdaylem1  27082  birthdaylem2  27083  wilthlem2  27199  wilthlem3  27200  ftalem5  27207  ppifi  27236  prmdvdsfi  27237  chtdif  27288  ppidif  27293  chp1  27297  ppiltx  27307  prmorcht  27308  mumul  27311  sqff1o  27312  ppiub  27334  pclogsum  27345  logexprlim  27355  gausslemma2dlem1  27496  gausslemma2dlem5  27501  gausslemma2dlem6  27502  lgseisenlem2  27506  axlowdimlem16  29248  konigsberglem5  30548  pmtrto1cl  33360  psgnfzto1stlem  33361  fzto1st  33364  psgnfzto1st  33366  smatcl  34137  1smat1  34139  esumpcvgval  34413  esumcvg  34421  carsggect  34653  carsgclctunlem2  34654  oddpwdc  34689  eulerpartlemb  34703  ballotlem1  34822  ballotlem2  34824  ballotlemfelz  34826  ballotlemfp1  34827  ballotlemfc0  34828  ballotlemfcc  34829  ballotlemfmpn  34830  ballotlemiex  34837  ballotlemsup  34840  ballotlemfg  34861  ballotlemfrc  34862  ballotlemfrceq  34864  ballotth  34873  fsum2dsub  34939  reprfi2  34955  breprexpnat  34966  hgt750lemb  34988  hgt750leme  34990  pthhashvtx  35553  subfacf  35600  subfacp1lem1  35604  subfacp1lem3  35607  subfacp1lem5  35609  subfacp1lem6  35610  erdszelem2  35617  erdszelem10  35625  cvmliftlem15  35723  bcprod  36163  ptrecube  38194  poimirlem25  38219  poimirlem26  38220  poimirlem27  38221  poimirlem28  38222  poimirlem29  38223  poimirlem30  38224  poimirlem31  38225  poimirlem32  38226  mblfinlem2  38232  volsupnfl  38239  itg2addnclem2  38246  nnubfi  38324  nninfnub  38325  cntotbnd  38370  lcmfunnnd  42704  lcmineqlem4  42724  lcmineqlem6  42726  lcmineqlem15  42735  lcmineqlem16  42736  lcmineqlem19  42739  lcmineqlem20  42740  lcmineqlem21  42741  lcmineqlem22  42742  sticksstones17  42855  fisdomnn  42937  fz1sumconst  42995  eldioph2lem1  43418  eldioph2lem2  43419  eldioph2  43420  pellexlem5  43487  pellex  43489  jm2.22  43649  jm2.23  43650  hbt  43784  rp-isfinite6  44171  fzisoeu  45946  sumnnodd  46273  stoweidlem37  46678  stoweidlem44  46685  stoweidlem59  46700  fourierdlem37  46785  fourierdlem103  46850  fourierdlem104  46851  etransclem16  46891  etransclem24  46899  etransclem25  46900  etransclem33  46908  etransclem35  46910  etransclem44  46919  etransclem45  46920  sge0reuz  47088  hoidmvlelem2  47237  aacllem  50510