Theorem fzfi 13925

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 8979	. . 3 ⊢ ∅ ∈ Fin
2		eleq1 2827	. . 3 ⊢ ((𝑀...𝑁) = ∅ → ((𝑀...𝑁) ∈ Fin ↔ ∅ ∈ Fin))
3	1, 2	mpbiri 259	. 2 ⊢ ((𝑀...𝑁) = ∅ → (𝑀...𝑁) ∈ Fin)
4		fzn0 13483	. . 3 ⊢ ((𝑀...𝑁) ≠ ∅ ↔ 𝑁 ∈ (ℤ≥‘𝑀))
5		onfin2 9141	. . . . . 6 ⊢ ω = (On ∩ Fin)
6		inss2 4166	. . . . . 6 ⊢ (On ∩ Fin) ⊆ Fin
7	5, 6	eqsstri 3961	. . . . 5 ⊢ ω ⊆ Fin
8		eqid 2739	. . . . . . 7 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
9	8	hashgf1o 13924	. . . . . 6 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
10		peano2uz 12842	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
11		uznn0sub 12814	. . . . . . 7 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
12	10, 11	syl 17	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
13		f1ocnvdm 7229	. . . . . 6 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0 ∧ ((𝑁 + 1) − 𝑀) ∈ ℕ0) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
14	9, 12, 13	sylancr 593	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
15	7, 14	sselid 3913	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin)
16	8	fzen2 13922	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)))
17		enfii 9110	. . . 4 ⊢ (((◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin ∧ (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀))) → (𝑀...𝑁) ∈ Fin)
18	15, 16, 17	syl2anc 590	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ∈ Fin)
19	4, 18	sylbi 218	. 2 ⊢ ((𝑀...𝑁) ≠ ∅ → (𝑀...𝑁) ∈ Fin)
20	3, 19	pm2.61ine 3017	1 ⊢ (𝑀...𝑁) ∈ Fin

Syntax hints:   = wceq 1547   ∈ wcel 2119   ≠ wne 2934  Vcvv 3431   ∩ cin 3882  ∅c0 4261   class class class wbr 5072   ↦ cmpt 5153  ^◡ccnv 5617   ↾ cres 5620  Oncon0 6310  –1-1-onto→wf1o 6484  ‘cfv 6485  (class class class)co 7356  ωcom 7806  reccrdg 8338   ≈ cen 8880  Fincfn 8883  0cc0 11029  1c1 11030   + caddc 11032   − cmin 11368  ℕ₀cn0 12428  ℤ_≥cuz 12779  ...cfz 13452

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-1st 7931  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-n0 12429  df-z 12516  df-uz 12780  df-fz 13453

This theorem is referenced by:  fzfid  13926  fzofi  13927  fsequb  13928  fsequb2  13929  fseqsupcl  13930  ssnn0fi  13938  seqf1o  13996  isfinite4  14315  hashdom  14332  fzsdom2  14381  fnfz0hashnn0  14401  seqcoll2  14418  caubnd  15312  limsupgre  15434  summolem3  15667  summolem2  15669  zsum  15671  prodmolem3  15889  prodmolem2  15891  zprod  15893  risefallfac  15980  bpolylem  16004  phicl2  16729  phibnd  16732  hashdvds  16736  phiprmpw  16737  eulerth  16744  pcfac  16861  prmreclem2  16879  prmreclem3  16880  prmreclem4  16881  prmreclem5  16882  prmrec  16884  1arith  16889  vdwlem6  16948  vdwlem10  16952  vdwlem12  16954  prmdvdsprmo  17004  prmgaplcmlem1  17013  prmgaplcm  17022  isstruct2  17110  gsumval3lem1  19871  gsumval3lem2  19872  gsumval3  19873  coe1mul2  22255  ehleudis  25403  ehleudisval  25404  ovoliunlem2  25488  uniioombllem6  25573  itg0  25765  itgz  25766  coemullem  26233  aannenlem1  26312  aannenlem2  26313  birthdaylem1  26933  birthdaylem2  26934  wilthlem2  27050  wilthlem3  27051  ftalem5  27058  ppifi  27087  prmdvdsfi  27088  chtdif  27139  ppidif  27144  chp1  27148  ppiltx  27158  prmorcht  27159  mumul  27162  sqff1o  27163  ppiub  27185  pclogsum  27196  logexprlim  27206  gausslemma2dlem1  27347  gausslemma2dlem5  27352  gausslemma2dlem6  27353  lgseisenlem2  27357  axlowdimlem16  29044  konigsberglem5  30344  pmtrto1cl  33180  psgnfzto1stlem  33181  fzto1st  33184  psgnfzto1st  33186  smatcl  33986  1smat1  33988  esumpcvgval  34262  esumcvg  34270  carsggect  34502  carsgclctunlem2  34503  oddpwdc  34538  eulerpartlemb  34552  ballotlem1  34671  ballotlem2  34673  ballotlemfelz  34675  ballotlemfp1  34676  ballotlemfc0  34677  ballotlemfcc  34678  ballotlemfmpn  34679  ballotlemiex  34686  ballotlemsup  34689  ballotlemfg  34710  ballotlemfrc  34711  ballotlemfrceq  34713  ballotth  34722  plymulx0  34731  fsum2dsub  34791  reprfi2  34807  breprexpnat  34818  hgt750lemb  34840  hgt750leme  34842  pthhashvtx  35356  subfacf  35403  subfacp1lem1  35407  subfacp1lem3  35410  subfacp1lem5  35412  subfacp1lem6  35413  erdszelem2  35420  erdszelem10  35428  cvmliftlem15  35526  bcprod  35966  ptrecube  37987  poimirlem25  38012  poimirlem26  38013  poimirlem27  38014  poimirlem28  38015  poimirlem29  38016  poimirlem30  38017  poimirlem31  38018  poimirlem32  38019  mblfinlem2  38025  volsupnfl  38032  itg2addnclem2  38039  nnubfi  38117  nninfnub  38118  cntotbnd  38163  lcmfunnnd  42497  lcmineqlem4  42517  lcmineqlem6  42519  lcmineqlem15  42528  lcmineqlem16  42529  lcmineqlem19  42532  lcmineqlem20  42533  lcmineqlem21  42534  lcmineqlem22  42535  sticksstones17  42648  fisdomnn  42728  fz1sumconst  42786  eldioph2lem1  43209  eldioph2lem2  43210  eldioph2  43211  pellexlem5  43278  pellex  43280  jm2.22  43440  jm2.23  43441  hbt  43575  rp-isfinite6  43962  fzisoeu  45748  sumnnodd  46075  stoweidlem37  46480  stoweidlem44  46487  stoweidlem59  46502  fourierdlem37  46587  fourierdlem103  46652  fourierdlem104  46653  etransclem16  46693  etransclem24  46701  etransclem25  46702  etransclem33  46710  etransclem35  46712  etransclem44  46721  etransclem45  46722  sge0reuz  46890  hoidmvlelem2  47039  aacllem  50291