Theorem fzfi 13944

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 9016	. . 3 ⊢ ∅ ∈ Fin
2		eleq1 2817	. . 3 ⊢ ((𝑀...𝑁) = ∅ → ((𝑀...𝑁) ∈ Fin ↔ ∅ ∈ Fin))
3	1, 2	mpbiri 258	. 2 ⊢ ((𝑀...𝑁) = ∅ → (𝑀...𝑁) ∈ Fin)
4		fzn0 13506	. . 3 ⊢ ((𝑀...𝑁) ≠ ∅ ↔ 𝑁 ∈ (ℤ≥‘𝑀))
5		onfin2 9186	. . . . . 6 ⊢ ω = (On ∩ Fin)
6		inss2 4204	. . . . . 6 ⊢ (On ∩ Fin) ⊆ Fin
7	5, 6	eqsstri 3996	. . . . 5 ⊢ ω ⊆ Fin
8		eqid 2730	. . . . . . 7 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
9	8	hashgf1o 13943	. . . . . 6 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
10		peano2uz 12867	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
11		uznn0sub 12839	. . . . . . 7 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
12	10, 11	syl 17	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
13		f1ocnvdm 7263	. . . . . 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 3947	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin)
16	8	fzen2 13941	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)))
17		enfii 9156	. . . 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 3009	1 ⊢ (𝑀...𝑁) ∈ Fin

Syntax hints:   = wceq 1540   ∈ wcel 2109   ≠ wne 2926  Vcvv 3450   ∩ cin 3916  ∅c0 4299   class class class wbr 5110   ↦ cmpt 5191  ^◡ccnv 5640   ↾ cres 5643  Oncon0 6335  –1-1-onto→wf1o 6513  ‘cfv 6514  (class class class)co 7390  ωcom 7845  reccrdg 8380   ≈ cen 8918  Fincfn 8921  0cc0 11075  1c1 11076   + caddc 11078   − cmin 11412  ℕ₀cn0 12449  ℤ_≥cuz 12800  ...cfz 13475

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-om 7846  df-1st 7971  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-1o 8437  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-nn 12194  df-n0 12450  df-z 12537  df-uz 12801  df-fz 13476

This theorem is referenced by:  fzfid  13945  fzofi  13946  fsequb  13947  fsequb2  13948  fseqsupcl  13949  ssnn0fi  13957  seqf1o  14015  isfinite4  14334  hashdom  14351  fzsdom2  14400  fnfz0hashnn0  14420  seqcoll2  14437  caubnd  15332  limsupgre  15454  summolem3  15687  summolem2  15689  zsum  15691  prodmolem3  15906  prodmolem2  15908  zprod  15910  risefallfac  15997  bpolylem  16021  phicl2  16745  phibnd  16748  hashdvds  16752  phiprmpw  16753  eulerth  16760  pcfac  16877  prmreclem2  16895  prmreclem3  16896  prmreclem4  16897  prmreclem5  16898  prmrec  16900  1arith  16905  vdwlem6  16964  vdwlem10  16968  vdwlem12  16970  prmdvdsprmo  17020  prmgaplcmlem1  17029  prmgaplcm  17038  isstruct2  17126  gsumval3lem1  19842  gsumval3lem2  19843  gsumval3  19844  coe1mul2  22162  ehleudis  25325  ehleudisval  25326  ovoliunlem2  25411  uniioombllem6  25496  itg0  25688  itgz  25689  coemullem  26162  aannenlem1  26243  aannenlem2  26244  birthdaylem1  26868  birthdaylem2  26869  wilthlem2  26986  wilthlem3  26987  ftalem5  26994  ppifi  27023  prmdvdsfi  27024  chtdif  27075  ppidif  27080  chp1  27084  ppiltx  27094  prmorcht  27095  mumul  27098  sqff1o  27099  ppiub  27122  pclogsum  27133  logexprlim  27143  gausslemma2dlem1  27284  gausslemma2dlem5  27289  gausslemma2dlem6  27290  lgseisenlem2  27294  axlowdimlem16  28891  konigsberglem5  30192  pmtrto1cl  33063  psgnfzto1stlem  33064  fzto1st  33067  psgnfzto1st  33069  smatcl  33799  1smat1  33801  esumpcvgval  34075  esumcvg  34083  carsggect  34316  carsgclctunlem2  34317  oddpwdc  34352  eulerpartlemb  34366  ballotlem1  34485  ballotlem2  34487  ballotlemfelz  34489  ballotlemfp1  34490  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemfmpn  34493  ballotlemiex  34500  ballotlemsup  34503  ballotlemfg  34524  ballotlemfrc  34525  ballotlemfrceq  34527  ballotth  34536  plymulx0  34545  fsum2dsub  34605  reprfi2  34621  breprexpnat  34632  hgt750lemb  34654  hgt750leme  34656  pthhashvtx  35122  subfacf  35169  subfacp1lem1  35173  subfacp1lem3  35176  subfacp1lem5  35178  subfacp1lem6  35179  erdszelem2  35186  erdszelem10  35194  cvmliftlem15  35292  bcprod  35732  ptrecube  37621  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  poimirlem28  37649  poimirlem29  37650  poimirlem30  37651  poimirlem31  37652  poimirlem32  37653  mblfinlem2  37659  volsupnfl  37666  itg2addnclem2  37673  nnubfi  37751  nninfnub  37752  cntotbnd  37797  lcmfunnnd  42007  lcmineqlem4  42027  lcmineqlem6  42029  lcmineqlem15  42038  lcmineqlem16  42039  lcmineqlem19  42042  lcmineqlem20  42043  lcmineqlem21  42044  lcmineqlem22  42045  sticksstones17  42158  fisdomnn  42239  fz1sumconst  42304  eldioph2lem1  42755  eldioph2lem2  42756  eldioph2  42757  pellexlem5  42828  pellex  42830  jm2.22  42991  jm2.23  42992  hbt  43126  rp-isfinite6  43514  fzisoeu  45305  sumnnodd  45635  stoweidlem37  46042  stoweidlem44  46049  stoweidlem59  46064  fourierdlem37  46149  fourierdlem103  46214  fourierdlem104  46215  etransclem16  46255  etransclem24  46263  etransclem25  46264  etransclem33  46272  etransclem35  46274  etransclem44  46283  etransclem45  46284  sge0reuz  46452  hoidmvlelem2  46601  aacllem  49794