Theorem fzfi 13929

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 8983	. . 3 ⊢ ∅ ∈ Fin
2		eleq1 2829	. . 3 ⊢ ((𝑀...𝑁) = ∅ → ((𝑀...𝑁) ∈ Fin ↔ ∅ ∈ Fin))
3	1, 2	mpbiri 260	. 2 ⊢ ((𝑀...𝑁) = ∅ → (𝑀...𝑁) ∈ Fin)
4		fzn0 13487	. . 3 ⊢ ((𝑀...𝑁) ≠ ∅ ↔ 𝑁 ∈ (ℤ≥‘𝑀))
5		onfin2 9145	. . . . . 6 ⊢ ω = (On ∩ Fin)
6		inss2 4169	. . . . . 6 ⊢ (On ∩ Fin) ⊆ Fin
7	5, 6	eqsstri 3963	. . . . 5 ⊢ ω ⊆ Fin
8		eqid 2741	. . . . . . 7 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
9	8	hashgf1o 13928	. . . . . 6 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
10		peano2uz 12846	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
11		uznn0sub 12818	. . . . . . 7 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
12	10, 11	syl 17	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
13		f1ocnvdm 7233	. . . . . 6 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0 ∧ ((𝑁 + 1) − 𝑀) ∈ ℕ0) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
14	9, 12, 13	sylancr 594	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
15	7, 14	sselid 3915	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin)
16	8	fzen2 13926	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)))
17		enfii 9114	. . . 4 ⊢ (((◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin ∧ (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀))) → (𝑀...𝑁) ∈ Fin)
18	15, 16, 17	syl2anc 591	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ∈ Fin)
19	4, 18	sylbi 219	. 2 ⊢ ((𝑀...𝑁) ≠ ∅ → (𝑀...𝑁) ∈ Fin)
20	3, 19	pm2.61ine 3019	1 ⊢ (𝑀...𝑁) ∈ Fin

Syntax hints:   = wceq 1548   ∈ wcel 2121   ≠ wne 2936  Vcvv 3433   ∩ cin 3884  ∅c0 4264   class class class wbr 5075   ↦ cmpt 5156  ^◡ccnv 5620   ↾ cres 5623  Oncon0 6314  –1-1-onto→wf1o 6488  ‘cfv 6489  (class class class)co 7360  ωcom 7810  reccrdg 8342   ≈ cen 8884  Fincfn 8887  0cc0 11033  1c1 11034   + caddc 11036   − cmin 11372  ℕ₀cn0 12432  ℤ_≥cuz 12783  ...cfz 13456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682  ax-cnex 11089  ax-resscn 11090  ax-1cn 11091  ax-icn 11092  ax-addcl 11093  ax-addrcl 11094  ax-mulcl 11095  ax-mulrcl 11096  ax-mulcom 11097  ax-addass 11098  ax-mulass 11099  ax-distr 11100  ax-i2m1 11101  ax-1ne0 11102  ax-1rid 11103  ax-rnegex 11104  ax-rrecex 11105  ax-cnre 11106  ax-pre-lttri 11107  ax-pre-lttrn 11108  ax-pre-ltadd 11109  ax-pre-mulgt0 11110

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-iun 4926  df-br 5076  df-opab 5138  df-mpt 5157  df-tr 5183  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-1st 7935  df-2nd 7936  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-pnf 11176  df-mnf 11177  df-xr 11178  df-ltxr 11179  df-le 11180  df-sub 11374  df-neg 11375  df-nn 12170  df-n0 12433  df-z 12520  df-uz 12784  df-fz 13457

This theorem is referenced by:  fzfid  13930  fzofi  13931  fsequb  13932  fsequb2  13933  fseqsupcl  13934  ssnn0fi  13942  seqf1o  14000  isfinite4  14319  hashdom  14336  fzsdom2  14385  fnfz0hashnn0  14405  seqcoll2  14422  caubnd  15316  limsupgre  15438  summolem3  15671  summolem2  15673  zsum  15675  prodmolem3  15893  prodmolem2  15895  zprod  15897  risefallfac  15984  bpolylem  16008  phicl2  16733  phibnd  16736  hashdvds  16740  phiprmpw  16741  eulerth  16748  pcfac  16865  prmreclem2  16883  prmreclem3  16884  prmreclem4  16885  prmreclem5  16886  prmrec  16888  1arith  16893  vdwlem6  16952  vdwlem10  16956  vdwlem12  16958  prmdvdsprmo  17008  prmgaplcmlem1  17017  prmgaplcm  17026  isstruct2  17114  gsumval3lem1  19875  gsumval3lem2  19876  gsumval3  19877  coe1mul2  22259  ehleudis  25407  ehleudisval  25408  ovoliunlem2  25492  uniioombllem6  25577  itg0  25769  itgz  25770  coemullem  26237  aannenlem1  26316  aannenlem2  26317  birthdaylem1  26937  birthdaylem2  26938  wilthlem2  27054  wilthlem3  27055  ftalem5  27062  ppifi  27091  prmdvdsfi  27092  chtdif  27143  ppidif  27148  chp1  27152  ppiltx  27162  prmorcht  27163  mumul  27166  sqff1o  27167  ppiub  27189  pclogsum  27200  logexprlim  27210  gausslemma2dlem1  27351  gausslemma2dlem5  27356  gausslemma2dlem6  27357  lgseisenlem2  27361  axlowdimlem16  29048  konigsberglem5  30348  pmtrto1cl  33184  psgnfzto1stlem  33185  fzto1st  33188  psgnfzto1st  33190  smatcl  33998  1smat1  34000  esumpcvgval  34274  esumcvg  34282  carsggect  34514  carsgclctunlem2  34515  oddpwdc  34550  eulerpartlemb  34564  ballotlem1  34683  ballotlem2  34685  ballotlemfelz  34687  ballotlemfp1  34688  ballotlemfc0  34689  ballotlemfcc  34690  ballotlemfmpn  34691  ballotlemiex  34698  ballotlemsup  34701  ballotlemfg  34722  ballotlemfrc  34723  ballotlemfrceq  34725  ballotth  34734  plymulx0  34743  fsum2dsub  34803  reprfi2  34819  breprexpnat  34830  hgt750lemb  34852  hgt750leme  34854  pthhashvtx  35371  subfacf  35418  subfacp1lem1  35422  subfacp1lem3  35425  subfacp1lem5  35427  subfacp1lem6  35428  erdszelem2  35435  erdszelem10  35443  cvmliftlem15  35541  bcprod  35981  ptrecube  38002  poimirlem25  38027  poimirlem26  38028  poimirlem27  38029  poimirlem28  38030  poimirlem29  38031  poimirlem30  38032  poimirlem31  38033  poimirlem32  38034  mblfinlem2  38040  volsupnfl  38047  itg2addnclem2  38054  nnubfi  38132  nninfnub  38133  cntotbnd  38178  lcmfunnnd  42512  lcmineqlem4  42532  lcmineqlem6  42534  lcmineqlem15  42543  lcmineqlem16  42544  lcmineqlem19  42547  lcmineqlem20  42548  lcmineqlem21  42549  lcmineqlem22  42550  sticksstones17  42663  fisdomnn  42743  fz1sumconst  42801  eldioph2lem1  43224  eldioph2lem2  43225  eldioph2  43226  pellexlem5  43293  pellex  43295  jm2.22  43455  jm2.23  43456  hbt  43590  rp-isfinite6  43977  fzisoeu  45762  sumnnodd  46089  stoweidlem37  46494  stoweidlem44  46501  stoweidlem59  46516  fourierdlem37  46601  fourierdlem103  46666  fourierdlem104  46667  etransclem16  46707  etransclem24  46715  etransclem25  46716  etransclem33  46724  etransclem35  46726  etransclem44  46735  etransclem45  46736  sge0reuz  46904  hoidmvlelem2  47053  aacllem  50305