Theorem fzfi 13692

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 8954	. . 3 ⊢ ∅ ∈ Fin
2		eleq1 2826	. . 3 ⊢ ((𝑀...𝑁) = ∅ → ((𝑀...𝑁) ∈ Fin ↔ ∅ ∈ Fin))
3	1, 2	mpbiri 257	. 2 ⊢ ((𝑀...𝑁) = ∅ → (𝑀...𝑁) ∈ Fin)
4		fzn0 13270	. . 3 ⊢ ((𝑀...𝑁) ≠ ∅ ↔ 𝑁 ∈ (ℤ≥‘𝑀))
5		onfin2 9014	. . . . . 6 ⊢ ω = (On ∩ Fin)
6		inss2 4163	. . . . . 6 ⊢ (On ∩ Fin) ⊆ Fin
7	5, 6	eqsstri 3955	. . . . 5 ⊢ ω ⊆ Fin
8		eqid 2738	. . . . . . 7 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
9	8	hashgf1o 13691	. . . . . 6 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
10		peano2uz 12641	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
11		uznn0sub 12617	. . . . . . 7 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
12	10, 11	syl 17	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
13		f1ocnvdm 7157	. . . . . 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 3919	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin)
16	8	fzen2 13689	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)))
17		enfii 8972	. . . 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 216	. 2 ⊢ ((𝑀...𝑁) ≠ ∅ → (𝑀...𝑁) ∈ Fin)
20	3, 19	pm2.61ine 3028	1 ⊢ (𝑀...𝑁) ∈ Fin

Syntax hints:   = wceq 1539   ∈ wcel 2106   ≠ wne 2943  Vcvv 3432   ∩ cin 3886  ∅c0 4256   class class class wbr 5074   ↦ cmpt 5157  ^◡ccnv 5588   ↾ cres 5591  Oncon0 6266  –1-1-onto→wf1o 6432  ‘cfv 6433  (class class class)co 7275  ωcom 7712  reccrdg 8240   ≈ cen 8730  Fincfn 8733  0cc0 10871  1c1 10872   + caddc 10874   − cmin 11205  ℕ₀cn0 12233  ℤ_≥cuz 12582  ...cfz 13239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-nn 11974  df-n0 12234  df-z 12320  df-uz 12583  df-fz 13240

This theorem is referenced by:  fzfid  13693  fzofi  13694  fsequb  13695  fsequb2  13696  fseqsupcl  13697  ssnn0fi  13705  seqf1o  13764  isfinite4  14077  hashdom  14094  fzsdom2  14143  fnfz0hashnn0  14160  seqcoll2  14179  caubnd  15070  limsupgre  15190  summolem3  15426  summolem2  15428  zsum  15430  prodmolem3  15643  prodmolem2  15645  zprod  15647  risefallfac  15734  bpolylem  15758  phicl2  16469  phibnd  16472  hashdvds  16476  phiprmpw  16477  eulerth  16484  phisum  16491  pcfac  16600  prmreclem2  16618  prmreclem3  16619  prmreclem4  16620  prmreclem5  16621  prmrec  16623  1arith  16628  vdwlem6  16687  vdwlem10  16691  vdwlem12  16693  prmdvdsprmo  16743  prmgaplcmlem1  16752  prmgaplcm  16761  isstruct2  16850  gsumval3lem1  19506  gsumval3lem2  19507  gsumval3  19508  coe1mul2  21440  ehleudis  24582  ehleudisval  24583  ovoliunlem2  24667  uniioombllem6  24752  itg0  24944  itgz  24945  coemullem  25411  aannenlem1  25488  aannenlem2  25489  birthdaylem1  26101  birthdaylem2  26102  wilthlem2  26218  wilthlem3  26219  ftalem5  26226  ppifi  26255  prmdvdsfi  26256  chtdif  26307  ppidif  26312  chp1  26316  ppiltx  26326  prmorcht  26327  mumul  26330  sqff1o  26331  ppiub  26352  pclogsum  26363  logexprlim  26373  gausslemma2dlem1  26514  gausslemma2dlem5  26519  gausslemma2dlem6  26520  lgseisenlem2  26524  axlowdimlem16  27325  konigsberglem5  28620  pmtrto1cl  31366  psgnfzto1stlem  31367  fzto1st  31370  psgnfzto1st  31372  smatcl  31752  1smat1  31754  esumpcvgval  32046  esumcvg  32054  carsggect  32285  carsgclctunlem2  32286  oddpwdc  32321  eulerpartlemb  32335  ballotlem1  32453  ballotlem2  32455  ballotlemfelz  32457  ballotlemfp1  32458  ballotlemfc0  32459  ballotlemfcc  32460  ballotlemfmpn  32461  ballotlemiex  32468  ballotlemsup  32471  ballotlemfg  32492  ballotlemfrc  32493  ballotlemfrceq  32495  ballotth  32504  plymulx0  32526  fsum2dsub  32587  reprfi2  32603  breprexpnat  32614  hgt750lemb  32636  hgt750leme  32638  pthhashvtx  33089  subfacf  33137  subfacp1lem1  33141  subfacp1lem3  33144  subfacp1lem5  33146  subfacp1lem6  33147  erdszelem2  33154  erdszelem10  33162  cvmliftlem15  33260  bcprod  33704  ptrecube  35777  poimirlem25  35802  poimirlem26  35803  poimirlem27  35804  poimirlem28  35805  poimirlem29  35806  poimirlem30  35807  poimirlem31  35808  poimirlem32  35809  mblfinlem2  35815  volsupnfl  35822  itg2addnclem2  35829  nnubfi  35908  nninfnub  35909  cntotbnd  35954  lcmfunnnd  40020  lcmineqlem4  40040  lcmineqlem6  40042  lcmineqlem15  40051  lcmineqlem16  40052  lcmineqlem19  40055  lcmineqlem20  40056  lcmineqlem21  40057  lcmineqlem22  40058  sticksstones17  40119  eldioph2lem1  40582  eldioph2lem2  40583  eldioph2  40584  pellexlem5  40655  pellex  40657  jm2.22  40817  jm2.23  40818  hbt  40955  rp-isfinite6  41125  fzisoeu  42839  sumnnodd  43171  stoweidlem37  43578  stoweidlem44  43585  stoweidlem59  43600  fourierdlem37  43685  fourierdlem103  43750  fourierdlem104  43751  etransclem16  43791  etransclem24  43799  etransclem25  43800  etransclem33  43808  etransclem35  43810  etransclem44  43819  etransclem45  43820  sge0reuz  43985  hoidmvlelem2  44134  aacllem  46505