Theorem fzfi 13943

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 9015	. . 3 ⊢ ∅ ∈ Fin
2		eleq1 2817	. . 3 ⊢ ((𝑀...𝑁) = ∅ → ((𝑀...𝑁) ∈ Fin ↔ ∅ ∈ Fin))
3	1, 2	mpbiri 258	. 2 ⊢ ((𝑀...𝑁) = ∅ → (𝑀...𝑁) ∈ Fin)
4		fzn0 13505	. . 3 ⊢ ((𝑀...𝑁) ≠ ∅ ↔ 𝑁 ∈ (ℤ≥‘𝑀))
5		onfin2 9185	. . . . . 6 ⊢ ω = (On ∩ Fin)
6		inss2 4203	. . . . . 6 ⊢ (On ∩ Fin) ⊆ Fin
7	5, 6	eqsstri 3995	. . . . 5 ⊢ ω ⊆ Fin
8		eqid 2730	. . . . . . 7 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
9	8	hashgf1o 13942	. . . . . 6 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
10		peano2uz 12866	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
11		uznn0sub 12838	. . . . . . 7 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
12	10, 11	syl 17	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
13		f1ocnvdm 7262	. . . . . 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 3946	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin)
16	8	fzen2 13940	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)))
17		enfii 9155	. . . 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 3915  ∅c0 4298   class class class wbr 5109   ↦ cmpt 5190  ^◡ccnv 5639   ↾ cres 5642  Oncon0 6334  –1-1-onto→wf1o 6512  ‘cfv 6513  (class class class)co 7389  ωcom 7844  reccrdg 8379   ≈ cen 8917  Fincfn 8920  0cc0 11074  1c1 11075   + caddc 11077   − cmin 11411  ℕ₀cn0 12448  ℤ_≥cuz 12799  ...cfz 13474

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 5253  ax-nul 5263  ax-pow 5322  ax-pr 5389  ax-un 7713  ax-cnex 11130  ax-resscn 11131  ax-1cn 11132  ax-icn 11133  ax-addcl 11134  ax-addrcl 11135  ax-mulcl 11136  ax-mulrcl 11137  ax-mulcom 11138  ax-addass 11139  ax-mulass 11140  ax-distr 11141  ax-i2m1 11142  ax-1ne0 11143  ax-1rid 11144  ax-rnegex 11145  ax-rrecex 11146  ax-cnre 11147  ax-pre-lttri 11148  ax-pre-lttrn 11149  ax-pre-ltadd 11150  ax-pre-mulgt0 11151

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 3756  df-csb 3865  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-pss 3936  df-nul 4299  df-if 4491  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5110  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5535  df-eprel 5540  df-po 5548  df-so 5549  df-fr 5593  df-we 5595  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-pred 6276  df-ord 6337  df-on 6338  df-lim 6339  df-suc 6340  df-iota 6466  df-fun 6515  df-fn 6516  df-f 6517  df-f1 6518  df-fo 6519  df-f1o 6520  df-fv 6521  df-riota 7346  df-ov 7392  df-oprab 7393  df-mpo 7394  df-om 7845  df-1st 7970  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8380  df-1o 8436  df-er 8673  df-en 8921  df-dom 8922  df-sdom 8923  df-fin 8924  df-pnf 11216  df-mnf 11217  df-xr 11218  df-ltxr 11219  df-le 11220  df-sub 11413  df-neg 11414  df-nn 12188  df-n0 12449  df-z 12536  df-uz 12800  df-fz 13475

This theorem is referenced by:  fzfid  13944  fzofi  13945  fsequb  13946  fsequb2  13947  fseqsupcl  13948  ssnn0fi  13956  seqf1o  14014  isfinite4  14333  hashdom  14350  fzsdom2  14399  fnfz0hashnn0  14419  seqcoll2  14436  caubnd  15331  limsupgre  15453  summolem3  15686  summolem2  15688  zsum  15690  prodmolem3  15905  prodmolem2  15907  zprod  15909  risefallfac  15996  bpolylem  16020  phicl2  16744  phibnd  16747  hashdvds  16751  phiprmpw  16752  eulerth  16759  pcfac  16876  prmreclem2  16894  prmreclem3  16895  prmreclem4  16896  prmreclem5  16897  prmrec  16899  1arith  16904  vdwlem6  16963  vdwlem10  16967  vdwlem12  16969  prmdvdsprmo  17019  prmgaplcmlem1  17028  prmgaplcm  17037  isstruct2  17125  gsumval3lem1  19841  gsumval3lem2  19842  gsumval3  19843  coe1mul2  22161  ehleudis  25324  ehleudisval  25325  ovoliunlem2  25410  uniioombllem6  25495  itg0  25687  itgz  25688  coemullem  26161  aannenlem1  26242  aannenlem2  26243  birthdaylem1  26867  birthdaylem2  26868  wilthlem2  26985  wilthlem3  26986  ftalem5  26993  ppifi  27022  prmdvdsfi  27023  chtdif  27074  ppidif  27079  chp1  27083  ppiltx  27093  prmorcht  27094  mumul  27097  sqff1o  27098  ppiub  27121  pclogsum  27132  logexprlim  27142  gausslemma2dlem1  27283  gausslemma2dlem5  27288  gausslemma2dlem6  27289  lgseisenlem2  27293  axlowdimlem16  28890  konigsberglem5  30191  pmtrto1cl  33062  psgnfzto1stlem  33063  fzto1st  33066  psgnfzto1st  33068  smatcl  33798  1smat1  33800  esumpcvgval  34074  esumcvg  34082  carsggect  34315  carsgclctunlem2  34316  oddpwdc  34351  eulerpartlemb  34365  ballotlem1  34484  ballotlem2  34486  ballotlemfelz  34488  ballotlemfp1  34489  ballotlemfc0  34490  ballotlemfcc  34491  ballotlemfmpn  34492  ballotlemiex  34499  ballotlemsup  34502  ballotlemfg  34523  ballotlemfrc  34524  ballotlemfrceq  34526  ballotth  34535  plymulx0  34544  fsum2dsub  34604  reprfi2  34620  breprexpnat  34631  hgt750lemb  34653  hgt750leme  34655  pthhashvtx  35115  subfacf  35162  subfacp1lem1  35166  subfacp1lem3  35169  subfacp1lem5  35171  subfacp1lem6  35172  erdszelem2  35179  erdszelem10  35187  cvmliftlem15  35285  bcprod  35720  ptrecube  37609  poimirlem25  37634  poimirlem26  37635  poimirlem27  37636  poimirlem28  37637  poimirlem29  37638  poimirlem30  37639  poimirlem31  37640  poimirlem32  37641  mblfinlem2  37647  volsupnfl  37654  itg2addnclem2  37661  nnubfi  37739  nninfnub  37740  cntotbnd  37785  lcmfunnnd  41995  lcmineqlem4  42015  lcmineqlem6  42017  lcmineqlem15  42026  lcmineqlem16  42027  lcmineqlem19  42030  lcmineqlem20  42031  lcmineqlem21  42032  lcmineqlem22  42033  sticksstones17  42146  fisdomnn  42227  fz1sumconst  42292  eldioph2lem1  42741  eldioph2lem2  42742  eldioph2  42743  pellexlem5  42814  pellex  42816  jm2.22  42977  jm2.23  42978  hbt  43112  rp-isfinite6  43500  fzisoeu  45291  sumnnodd  45621  stoweidlem37  46028  stoweidlem44  46035  stoweidlem59  46050  fourierdlem37  46135  fourierdlem103  46200  fourierdlem104  46201  etransclem16  46241  etransclem24  46249  etransclem25  46250  etransclem33  46258  etransclem35  46260  etransclem44  46269  etransclem45  46270  sge0reuz  46438  hoidmvlelem2  46587  aacllem  49767