Theorem fzfi 13545

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 8849	. . 3 ⊢ ∅ ∈ Fin
2		eleq1 2825	. . 3 ⊢ ((𝑀...𝑁) = ∅ → ((𝑀...𝑁) ∈ Fin ↔ ∅ ∈ Fin))
3	1, 2	mpbiri 261	. 2 ⊢ ((𝑀...𝑁) = ∅ → (𝑀...𝑁) ∈ Fin)
4		fzn0 13126	. . 3 ⊢ ((𝑀...𝑁) ≠ ∅ ↔ 𝑁 ∈ (ℤ≥‘𝑀))
5		onfin2 8871	. . . . . 6 ⊢ ω = (On ∩ Fin)
6		inss2 4144	. . . . . 6 ⊢ (On ∩ Fin) ⊆ Fin
7	5, 6	eqsstri 3935	. . . . 5 ⊢ ω ⊆ Fin
8		eqid 2737	. . . . . . 7 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
9	8	hashgf1o 13544	. . . . . 6 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
10		peano2uz 12497	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
11		uznn0sub 12473	. . . . . . 7 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
12	10, 11	syl 17	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
13		f1ocnvdm 7095	. . . . . 6 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0 ∧ ((𝑁 + 1) − 𝑀) ∈ ℕ0) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
14	9, 12, 13	sylancr 590	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
15	7, 14	sselid 3898	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin)
16	8	fzen2 13542	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)))
17		enfii 8864	. . . 4 ⊢ (((◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin ∧ (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀))) → (𝑀...𝑁) ∈ Fin)
18	15, 16, 17	syl2anc 587	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ∈ Fin)
19	4, 18	sylbi 220	. 2 ⊢ ((𝑀...𝑁) ≠ ∅ → (𝑀...𝑁) ∈ Fin)
20	3, 19	pm2.61ine 3025	1 ⊢ (𝑀...𝑁) ∈ Fin

Syntax hints:   = wceq 1543   ∈ wcel 2110   ≠ wne 2940  Vcvv 3408   ∩ cin 3865  ∅c0 4237   class class class wbr 5053   ↦ cmpt 5135  ^◡ccnv 5550   ↾ cres 5553  Oncon0 6213  –1-1-onto→wf1o 6379  ‘cfv 6380  (class class class)co 7213  ωcom 7644  reccrdg 8145   ≈ cen 8623  Fincfn 8626  0cc0 10729  1c1 10730   + caddc 10732   − cmin 11062  ℕ₀cn0 12090  ℤ_≥cuz 12438  ...cfz 13095

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 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-1st 7761  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-1o 8202  df-er 8391  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-nn 11831  df-n0 12091  df-z 12177  df-uz 12439  df-fz 13096

This theorem is referenced by:  fzfid  13546  fzofi  13547  fsequb  13548  fsequb2  13549  fseqsupcl  13550  ssnn0fi  13558  seqf1o  13617  isfinite4  13929  hashdom  13946  fzsdom2  13995  fnfz0hashnn0  14012  seqcoll2  14031  caubnd  14922  limsupgre  15042  summolem3  15278  summolem2  15280  zsum  15282  prodmolem3  15495  prodmolem2  15497  zprod  15499  risefallfac  15586  bpolylem  15610  phicl2  16321  phibnd  16324  hashdvds  16328  phiprmpw  16329  eulerth  16336  phisum  16343  pcfac  16452  prmreclem2  16470  prmreclem3  16471  prmreclem4  16472  prmreclem5  16473  prmrec  16475  1arith  16480  vdwlem6  16539  vdwlem10  16543  vdwlem12  16545  prmdvdsprmo  16595  prmgaplcmlem1  16604  prmgaplcm  16613  isstruct2  16702  gsumval3lem1  19290  gsumval3lem2  19291  gsumval3  19292  coe1mul2  21190  ehleudis  24315  ehleudisval  24316  ovoliunlem2  24400  uniioombllem6  24485  itg0  24677  itgz  24678  coemullem  25144  aannenlem1  25221  aannenlem2  25222  birthdaylem1  25834  birthdaylem2  25835  wilthlem2  25951  wilthlem3  25952  ftalem5  25959  ppifi  25988  prmdvdsfi  25989  chtdif  26040  ppidif  26045  chp1  26049  ppiltx  26059  prmorcht  26060  mumul  26063  sqff1o  26064  ppiub  26085  pclogsum  26096  logexprlim  26106  gausslemma2dlem1  26247  gausslemma2dlem5  26252  gausslemma2dlem6  26253  lgseisenlem2  26257  axlowdimlem16  27048  konigsberglem5  28339  pmtrto1cl  31085  psgnfzto1stlem  31086  fzto1st  31089  psgnfzto1st  31091  smatcl  31466  1smat1  31468  esumpcvgval  31758  esumcvg  31766  carsggect  31997  carsgclctunlem2  31998  oddpwdc  32033  eulerpartlemb  32047  ballotlem1  32165  ballotlem2  32167  ballotlemfelz  32169  ballotlemfp1  32170  ballotlemfc0  32171  ballotlemfcc  32172  ballotlemfmpn  32173  ballotlemiex  32180  ballotlemsup  32183  ballotlemfg  32204  ballotlemfrc  32205  ballotlemfrceq  32207  ballotth  32216  plymulx0  32238  fsum2dsub  32299  reprfi2  32315  breprexpnat  32326  hgt750lemb  32348  hgt750leme  32350  pthhashvtx  32802  subfacf  32850  subfacp1lem1  32854  subfacp1lem3  32857  subfacp1lem5  32859  subfacp1lem6  32860  erdszelem2  32867  erdszelem10  32875  cvmliftlem15  32973  bcprod  33422  ptrecube  35514  poimirlem25  35539  poimirlem26  35540  poimirlem27  35541  poimirlem28  35542  poimirlem29  35543  poimirlem30  35544  poimirlem31  35545  poimirlem32  35546  mblfinlem2  35552  volsupnfl  35559  itg2addnclem2  35566  nnubfi  35645  nninfnub  35646  cntotbnd  35691  lcmfunnnd  39754  lcmineqlem4  39774  lcmineqlem6  39776  lcmineqlem15  39785  lcmineqlem16  39786  lcmineqlem19  39789  lcmineqlem20  39790  lcmineqlem21  39791  lcmineqlem22  39792  sticksstones17  39841  eldioph2lem1  40285  eldioph2lem2  40286  eldioph2  40287  pellexlem5  40358  pellex  40360  jm2.22  40520  jm2.23  40521  hbt  40658  rp-isfinite6  40810  fzisoeu  42512  sumnnodd  42846  stoweidlem37  43253  stoweidlem44  43260  stoweidlem59  43275  fourierdlem37  43360  fourierdlem103  43425  fourierdlem104  43426  etransclem16  43466  etransclem24  43474  etransclem25  43475  etransclem33  43483  etransclem35  43485  etransclem44  43494  etransclem45  43495  sge0reuz  43660  hoidmvlelem2  43809  aacllem  46176