Theorem fzfi 14013

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 9082	. . 3 ⊢ ∅ ∈ Fin
2		eleq1 2829	. . 3 ⊢ ((𝑀...𝑁) = ∅ → ((𝑀...𝑁) ∈ Fin ↔ ∅ ∈ Fin))
3	1, 2	mpbiri 258	. 2 ⊢ ((𝑀...𝑁) = ∅ → (𝑀...𝑁) ∈ Fin)
4		fzn0 13578	. . 3 ⊢ ((𝑀...𝑁) ≠ ∅ ↔ 𝑁 ∈ (ℤ≥‘𝑀))
5		onfin2 9268	. . . . . 6 ⊢ ω = (On ∩ Fin)
6		inss2 4238	. . . . . 6 ⊢ (On ∩ Fin) ⊆ Fin
7	5, 6	eqsstri 4030	. . . . 5 ⊢ ω ⊆ Fin
8		eqid 2737	. . . . . . 7 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
9	8	hashgf1o 14012	. . . . . 6 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
10		peano2uz 12943	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
11		uznn0sub 12917	. . . . . . 7 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
12	10, 11	syl 17	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
13		f1ocnvdm 7305	. . . . . 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 3981	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin)
16	8	fzen2 14010	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)))
17		enfii 9226	. . . 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 3025	1 ⊢ (𝑀...𝑁) ∈ Fin

Syntax hints:   = wceq 1540   ∈ wcel 2108   ≠ wne 2940  Vcvv 3480   ∩ cin 3950  ∅c0 4333   class class class wbr 5143   ↦ cmpt 5225  ^◡ccnv 5684   ↾ cres 5687  Oncon0 6384  –1-1-onto→wf1o 6560  ‘cfv 6561  (class class class)co 7431  ωcom 7887  reccrdg 8449   ≈ cen 8982  Fincfn 8985  0cc0 11155  1c1 11156   + caddc 11158   − cmin 11492  ℕ₀cn0 12526  ℤ_≥cuz 12878  ...cfz 13547

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 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-n0 12527  df-z 12614  df-uz 12879  df-fz 13548

This theorem is referenced by:  fzfid  14014  fzofi  14015  fsequb  14016  fsequb2  14017  fseqsupcl  14018  ssnn0fi  14026  seqf1o  14084  isfinite4  14401  hashdom  14418  fzsdom2  14467  fnfz0hashnn0  14487  seqcoll2  14504  caubnd  15397  limsupgre  15517  summolem3  15750  summolem2  15752  zsum  15754  prodmolem3  15969  prodmolem2  15971  zprod  15973  risefallfac  16060  bpolylem  16084  phicl2  16805  phibnd  16808  hashdvds  16812  phiprmpw  16813  eulerth  16820  pcfac  16937  prmreclem2  16955  prmreclem3  16956  prmreclem4  16957  prmreclem5  16958  prmrec  16960  1arith  16965  vdwlem6  17024  vdwlem10  17028  vdwlem12  17030  prmdvdsprmo  17080  prmgaplcmlem1  17089  prmgaplcm  17098  isstruct2  17186  gsumval3lem1  19923  gsumval3lem2  19924  gsumval3  19925  coe1mul2  22272  ehleudis  25452  ehleudisval  25453  ovoliunlem2  25538  uniioombllem6  25623  itg0  25815  itgz  25816  coemullem  26289  aannenlem1  26370  aannenlem2  26371  birthdaylem1  26994  birthdaylem2  26995  wilthlem2  27112  wilthlem3  27113  ftalem5  27120  ppifi  27149  prmdvdsfi  27150  chtdif  27201  ppidif  27206  chp1  27210  ppiltx  27220  prmorcht  27221  mumul  27224  sqff1o  27225  ppiub  27248  pclogsum  27259  logexprlim  27269  gausslemma2dlem1  27410  gausslemma2dlem5  27415  gausslemma2dlem6  27416  lgseisenlem2  27420  axlowdimlem16  28972  konigsberglem5  30275  pmtrto1cl  33119  psgnfzto1stlem  33120  fzto1st  33123  psgnfzto1st  33125  smatcl  33801  1smat1  33803  esumpcvgval  34079  esumcvg  34087  carsggect  34320  carsgclctunlem2  34321  oddpwdc  34356  eulerpartlemb  34370  ballotlem1  34489  ballotlem2  34491  ballotlemfelz  34493  ballotlemfp1  34494  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemfmpn  34497  ballotlemiex  34504  ballotlemsup  34507  ballotlemfg  34528  ballotlemfrc  34529  ballotlemfrceq  34531  ballotth  34540  plymulx0  34562  fsum2dsub  34622  reprfi2  34638  breprexpnat  34649  hgt750lemb  34671  hgt750leme  34673  pthhashvtx  35133  subfacf  35180  subfacp1lem1  35184  subfacp1lem3  35187  subfacp1lem5  35189  subfacp1lem6  35190  erdszelem2  35197  erdszelem10  35205  cvmliftlem15  35303  bcprod  35738  ptrecube  37627  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  poimirlem28  37655  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  poimirlem32  37659  mblfinlem2  37665  volsupnfl  37672  itg2addnclem2  37679  nnubfi  37757  nninfnub  37758  cntotbnd  37803  lcmfunnnd  42013  lcmineqlem4  42033  lcmineqlem6  42035  lcmineqlem15  42044  lcmineqlem16  42045  lcmineqlem19  42048  lcmineqlem20  42049  lcmineqlem21  42050  lcmineqlem22  42051  sticksstones17  42164  fisdomnn  42285  fz1sumconst  42343  eldioph2lem1  42771  eldioph2lem2  42772  eldioph2  42773  pellexlem5  42844  pellex  42846  jm2.22  43007  jm2.23  43008  hbt  43142  rp-isfinite6  43531  fzisoeu  45312  sumnnodd  45645  stoweidlem37  46052  stoweidlem44  46059  stoweidlem59  46074  fourierdlem37  46159  fourierdlem103  46224  fourierdlem104  46225  etransclem16  46265  etransclem24  46273  etransclem25  46274  etransclem33  46282  etransclem35  46284  etransclem44  46293  etransclem45  46294  sge0reuz  46462  hoidmvlelem2  46611  aacllem  49320