Theorem fzfi 13620

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 8916	. . 3 ⊢ ∅ ∈ Fin
2		eleq1 2826	. . 3 ⊢ ((𝑀...𝑁) = ∅ → ((𝑀...𝑁) ∈ Fin ↔ ∅ ∈ Fin))
3	1, 2	mpbiri 257	. 2 ⊢ ((𝑀...𝑁) = ∅ → (𝑀...𝑁) ∈ Fin)
4		fzn0 13199	. . 3 ⊢ ((𝑀...𝑁) ≠ ∅ ↔ 𝑁 ∈ (ℤ≥‘𝑀))
5		onfin2 8945	. . . . . 6 ⊢ ω = (On ∩ Fin)
6		inss2 4160	. . . . . 6 ⊢ (On ∩ Fin) ⊆ Fin
7	5, 6	eqsstri 3951	. . . . 5 ⊢ ω ⊆ Fin
8		eqid 2738	. . . . . . 7 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
9	8	hashgf1o 13619	. . . . . 6 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
10		peano2uz 12570	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
11		uznn0sub 12546	. . . . . . 7 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
12	10, 11	syl 17	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
13		f1ocnvdm 7137	. . . . . 6 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0 ∧ ((𝑁 + 1) − 𝑀) ∈ ℕ0) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
14	9, 12, 13	sylancr 586	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
15	7, 14	sselid 3915	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin)
16	8	fzen2 13617	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)))
17		enfii 8932	. . . 4 ⊢ (((◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin ∧ (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀))) → (𝑀...𝑁) ∈ Fin)
18	15, 16, 17	syl2anc 583	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ∈ Fin)
19	4, 18	sylbi 216	. 2 ⊢ ((𝑀...𝑁) ≠ ∅ → (𝑀...𝑁) ∈ Fin)
20	3, 19	pm2.61ine 3027	1 ⊢ (𝑀...𝑁) ∈ Fin

Syntax hints:   = wceq 1539   ∈ wcel 2108   ≠ wne 2942  Vcvv 3422   ∩ cin 3882  ∅c0 4253   class class class wbr 5070   ↦ cmpt 5153  ^◡ccnv 5579   ↾ cres 5582  Oncon0 6251  –1-1-onto→wf1o 6417  ‘cfv 6418  (class class class)co 7255  ωcom 7687  reccrdg 8211   ≈ cen 8688  Fincfn 8691  0cc0 10802  1c1 10803   + caddc 10805   − cmin 11135  ℕ₀cn0 12163  ℤ_≥cuz 12511  ...cfz 13168

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-1st 7804  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-1o 8267  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-fin 8695  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-nn 11904  df-n0 12164  df-z 12250  df-uz 12512  df-fz 13169

This theorem is referenced by:  fzfid  13621  fzofi  13622  fsequb  13623  fsequb2  13624  fseqsupcl  13625  ssnn0fi  13633  seqf1o  13692  isfinite4  14005  hashdom  14022  fzsdom2  14071  fnfz0hashnn0  14088  seqcoll2  14107  caubnd  14998  limsupgre  15118  summolem3  15354  summolem2  15356  zsum  15358  prodmolem3  15571  prodmolem2  15573  zprod  15575  risefallfac  15662  bpolylem  15686  phicl2  16397  phibnd  16400  hashdvds  16404  phiprmpw  16405  eulerth  16412  phisum  16419  pcfac  16528  prmreclem2  16546  prmreclem3  16547  prmreclem4  16548  prmreclem5  16549  prmrec  16551  1arith  16556  vdwlem6  16615  vdwlem10  16619  vdwlem12  16621  prmdvdsprmo  16671  prmgaplcmlem1  16680  prmgaplcm  16689  isstruct2  16778  gsumval3lem1  19421  gsumval3lem2  19422  gsumval3  19423  coe1mul2  21350  ehleudis  24487  ehleudisval  24488  ovoliunlem2  24572  uniioombllem6  24657  itg0  24849  itgz  24850  coemullem  25316  aannenlem1  25393  aannenlem2  25394  birthdaylem1  26006  birthdaylem2  26007  wilthlem2  26123  wilthlem3  26124  ftalem5  26131  ppifi  26160  prmdvdsfi  26161  chtdif  26212  ppidif  26217  chp1  26221  ppiltx  26231  prmorcht  26232  mumul  26235  sqff1o  26236  ppiub  26257  pclogsum  26268  logexprlim  26278  gausslemma2dlem1  26419  gausslemma2dlem5  26424  gausslemma2dlem6  26425  lgseisenlem2  26429  axlowdimlem16  27228  konigsberglem5  28521  pmtrto1cl  31268  psgnfzto1stlem  31269  fzto1st  31272  psgnfzto1st  31274  smatcl  31654  1smat1  31656  esumpcvgval  31946  esumcvg  31954  carsggect  32185  carsgclctunlem2  32186  oddpwdc  32221  eulerpartlemb  32235  ballotlem1  32353  ballotlem2  32355  ballotlemfelz  32357  ballotlemfp1  32358  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemfmpn  32361  ballotlemiex  32368  ballotlemsup  32371  ballotlemfg  32392  ballotlemfrc  32393  ballotlemfrceq  32395  ballotth  32404  plymulx0  32426  fsum2dsub  32487  reprfi2  32503  breprexpnat  32514  hgt750lemb  32536  hgt750leme  32538  pthhashvtx  32989  subfacf  33037  subfacp1lem1  33041  subfacp1lem3  33044  subfacp1lem5  33046  subfacp1lem6  33047  erdszelem2  33054  erdszelem10  33062  cvmliftlem15  33160  bcprod  33610  ptrecube  35704  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  poimirlem28  35732  poimirlem29  35733  poimirlem30  35734  poimirlem31  35735  poimirlem32  35736  mblfinlem2  35742  volsupnfl  35749  itg2addnclem2  35756  nnubfi  35835  nninfnub  35836  cntotbnd  35881  lcmfunnnd  39948  lcmineqlem4  39968  lcmineqlem6  39970  lcmineqlem15  39979  lcmineqlem16  39980  lcmineqlem19  39983  lcmineqlem20  39984  lcmineqlem21  39985  lcmineqlem22  39986  sticksstones17  40047  eldioph2lem1  40498  eldioph2lem2  40499  eldioph2  40500  pellexlem5  40571  pellex  40573  jm2.22  40733  jm2.23  40734  hbt  40871  rp-isfinite6  41023  fzisoeu  42729  sumnnodd  43061  stoweidlem37  43468  stoweidlem44  43475  stoweidlem59  43490  fourierdlem37  43575  fourierdlem103  43640  fourierdlem104  43641  etransclem16  43681  etransclem24  43689  etransclem25  43690  etransclem33  43698  etransclem35  43700  etransclem44  43709  etransclem45  43710  sge0reuz  43875  hoidmvlelem2  44024  aacllem  46391