Theorem fzfi 13937

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 9013	. . 3 ⊢ ∅ ∈ Fin
2		eleq1 2816	. . 3 ⊢ ((𝑀...𝑁) = ∅ → ((𝑀...𝑁) ∈ Fin ↔ ∅ ∈ Fin))
3	1, 2	mpbiri 258	. 2 ⊢ ((𝑀...𝑁) = ∅ → (𝑀...𝑁) ∈ Fin)
4		fzn0 13499	. . 3 ⊢ ((𝑀...𝑁) ≠ ∅ ↔ 𝑁 ∈ (ℤ≥‘𝑀))
5		onfin2 9180	. . . . . 6 ⊢ ω = (On ∩ Fin)
6		inss2 4201	. . . . . 6 ⊢ (On ∩ Fin) ⊆ Fin
7	5, 6	eqsstri 3993	. . . . 5 ⊢ ω ⊆ Fin
8		eqid 2729	. . . . . . 7 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
9	8	hashgf1o 13936	. . . . . 6 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
10		peano2uz 12860	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
11		uznn0sub 12832	. . . . . . 7 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
12	10, 11	syl 17	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
13		f1ocnvdm 7260	. . . . . 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 3944	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin)
16	8	fzen2 13934	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)))
17		enfii 9150	. . . 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 3008	1 ⊢ (𝑀...𝑁) ∈ Fin

Syntax hints:   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  Vcvv 3447   ∩ cin 3913  ∅c0 4296   class class class wbr 5107   ↦ cmpt 5188  ^◡ccnv 5637   ↾ cres 5640  Oncon0 6332  –1-1-onto→wf1o 6510  ‘cfv 6511  (class class class)co 7387  ωcom 7842  reccrdg 8377   ≈ cen 8915  Fincfn 8918  0cc0 11068  1c1 11069   + caddc 11071   − cmin 11405  ℕ₀cn0 12442  ℤ_≥cuz 12793  ...cfz 13468

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 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-1st 7968  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-1o 8434  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-fin 8922  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-nn 12187  df-n0 12443  df-z 12530  df-uz 12794  df-fz 13469

This theorem is referenced by:  fzfid  13938  fzofi  13939  fsequb  13940  fsequb2  13941  fseqsupcl  13942  ssnn0fi  13950  seqf1o  14008  isfinite4  14327  hashdom  14344  fzsdom2  14393  fnfz0hashnn0  14413  seqcoll2  14430  caubnd  15325  limsupgre  15447  summolem3  15680  summolem2  15682  zsum  15684  prodmolem3  15899  prodmolem2  15901  zprod  15903  risefallfac  15990  bpolylem  16014  phicl2  16738  phibnd  16741  hashdvds  16745  phiprmpw  16746  eulerth  16753  pcfac  16870  prmreclem2  16888  prmreclem3  16889  prmreclem4  16890  prmreclem5  16891  prmrec  16893  1arith  16898  vdwlem6  16957  vdwlem10  16961  vdwlem12  16963  prmdvdsprmo  17013  prmgaplcmlem1  17022  prmgaplcm  17031  isstruct2  17119  gsumval3lem1  19835  gsumval3lem2  19836  gsumval3  19837  coe1mul2  22155  ehleudis  25318  ehleudisval  25319  ovoliunlem2  25404  uniioombllem6  25489  itg0  25681  itgz  25682  coemullem  26155  aannenlem1  26236  aannenlem2  26237  birthdaylem1  26861  birthdaylem2  26862  wilthlem2  26979  wilthlem3  26980  ftalem5  26987  ppifi  27016  prmdvdsfi  27017  chtdif  27068  ppidif  27073  chp1  27077  ppiltx  27087  prmorcht  27088  mumul  27091  sqff1o  27092  ppiub  27115  pclogsum  27126  logexprlim  27136  gausslemma2dlem1  27277  gausslemma2dlem5  27282  gausslemma2dlem6  27283  lgseisenlem2  27287  axlowdimlem16  28884  konigsberglem5  30185  pmtrto1cl  33056  psgnfzto1stlem  33057  fzto1st  33060  psgnfzto1st  33062  smatcl  33792  1smat1  33794  esumpcvgval  34068  esumcvg  34076  carsggect  34309  carsgclctunlem2  34310  oddpwdc  34345  eulerpartlemb  34359  ballotlem1  34478  ballotlem2  34480  ballotlemfelz  34482  ballotlemfp1  34483  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemfmpn  34486  ballotlemiex  34493  ballotlemsup  34496  ballotlemfg  34517  ballotlemfrc  34518  ballotlemfrceq  34520  ballotth  34529  plymulx0  34538  fsum2dsub  34598  reprfi2  34614  breprexpnat  34625  hgt750lemb  34647  hgt750leme  34649  pthhashvtx  35115  subfacf  35162  subfacp1lem1  35166  subfacp1lem3  35169  subfacp1lem5  35171  subfacp1lem6  35172  erdszelem2  35179  erdszelem10  35187  cvmliftlem15  35285  bcprod  35725  ptrecube  37614  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  poimirlem28  37642  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  mblfinlem2  37652  volsupnfl  37659  itg2addnclem2  37666  nnubfi  37744  nninfnub  37745  cntotbnd  37790  lcmfunnnd  42000  lcmineqlem4  42020  lcmineqlem6  42022  lcmineqlem15  42031  lcmineqlem16  42032  lcmineqlem19  42035  lcmineqlem20  42036  lcmineqlem21  42037  lcmineqlem22  42038  sticksstones17  42151  fisdomnn  42232  fz1sumconst  42297  eldioph2lem1  42748  eldioph2lem2  42749  eldioph2  42750  pellexlem5  42821  pellex  42823  jm2.22  42984  jm2.23  42985  hbt  43119  rp-isfinite6  43507  fzisoeu  45298  sumnnodd  45628  stoweidlem37  46035  stoweidlem44  46042  stoweidlem59  46057  fourierdlem37  46142  fourierdlem103  46207  fourierdlem104  46208  etransclem16  46248  etransclem24  46256  etransclem25  46257  etransclem33  46265  etransclem35  46267  etransclem44  46276  etransclem45  46277  sge0reuz  46445  hoidmvlelem2  46594  aacllem  49790