Theorem fzfi 13929

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 8984	. . 3 ⊢ ∅ ∈ Fin
2		eleq1 2825	. . 3 ⊢ ((𝑀...𝑁) = ∅ → ((𝑀...𝑁) ∈ Fin ↔ ∅ ∈ Fin))
3	1, 2	mpbiri 258	. 2 ⊢ ((𝑀...𝑁) = ∅ → (𝑀...𝑁) ∈ Fin)
4		fzn0 13487	. . 3 ⊢ ((𝑀...𝑁) ≠ ∅ ↔ 𝑁 ∈ (ℤ≥‘𝑀))
5		onfin2 9146	. . . . . 6 ⊢ ω = (On ∩ Fin)
6		inss2 4179	. . . . . 6 ⊢ (On ∩ Fin) ⊆ Fin
7	5, 6	eqsstri 3969	. . . . 5 ⊢ ω ⊆ Fin
8		eqid 2737	. . . . . . 7 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)
9	8	hashgf1o 13928	. . . . . 6 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0
10		peano2uz 12846	. . . . . . 7 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
11		uznn0sub 12818	. . . . . . 7 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
12	10, 11	syl 17	. . . . . 6 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑁 + 1) − 𝑀) ∈ ℕ0)
13		f1ocnvdm 7235	. . . . . 6 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω):ω–1-1-onto→ℕ0 ∧ ((𝑁 + 1) − 𝑀) ∈ ℕ0) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
14	9, 12, 13	sylancr 588	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ ω)
15	7, 14	sselid 3920	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin)
16	8	fzen2 13926	. . . 4 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)))
17		enfii 9115	. . . 4 ⊢ (((◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀)) ∈ Fin ∧ (𝑀...𝑁) ≈ (◡(rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω)‘((𝑁 + 1) − 𝑀))) → (𝑀...𝑁) ∈ Fin)
18	15, 16, 17	syl2anc 585	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) ∈ Fin)
19	4, 18	sylbi 217	. 2 ⊢ ((𝑀...𝑁) ≠ ∅ → (𝑀...𝑁) ∈ Fin)
20	3, 19	pm2.61ine 3016	1 ⊢ (𝑀...𝑁) ∈ Fin

Syntax hints:   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  Vcvv 3430   ∩ cin 3889  ∅c0 4274   class class class wbr 5086   ↦ cmpt 5167  ^◡ccnv 5625   ↾ cres 5628  Oncon0 6319  –1-1-onto→wf1o 6493  ‘cfv 6494  (class class class)co 7362  ωcom 7812  reccrdg 8343   ≈ cen 8885  Fincfn 8888  0cc0 11033  1c1 11034   + caddc 11036   − cmin 11372  ℕ₀cn0 12432  ℤ_≥cuz 12783  ...cfz 13456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5304  ax-pr 5372  ax-un 7684  ax-cnex 11089  ax-resscn 11090  ax-1cn 11091  ax-icn 11092  ax-addcl 11093  ax-addrcl 11094  ax-mulcl 11095  ax-mulrcl 11096  ax-mulcom 11097  ax-addass 11098  ax-mulass 11099  ax-distr 11100  ax-i2m1 11101  ax-1ne0 11102  ax-1rid 11103  ax-rnegex 11104  ax-rrecex 11105  ax-cnre 11106  ax-pre-lttri 11107  ax-pre-lttrn 11108  ax-pre-ltadd 11109  ax-pre-mulgt0 11110

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5521  df-eprel 5526  df-po 5534  df-so 5535  df-fr 5579  df-we 5581  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-pred 6261  df-ord 6322  df-on 6323  df-lim 6324  df-suc 6325  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-riota 7319  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7813  df-1st 7937  df-2nd 7938  df-frecs 8226  df-wrecs 8257  df-recs 8306  df-rdg 8344  df-1o 8400  df-er 8638  df-en 8889  df-dom 8890  df-sdom 8891  df-fin 8892  df-pnf 11176  df-mnf 11177  df-xr 11178  df-ltxr 11179  df-le 11180  df-sub 11374  df-neg 11375  df-nn 12170  df-n0 12433  df-z 12520  df-uz 12784  df-fz 13457

This theorem is referenced by:  fzfid  13930  fzofi  13931  fsequb  13932  fsequb2  13933  fseqsupcl  13934  ssnn0fi  13942  seqf1o  14000  isfinite4  14319  hashdom  14336  fzsdom2  14385  fnfz0hashnn0  14405  seqcoll2  14422  caubnd  15316  limsupgre  15438  summolem3  15671  summolem2  15673  zsum  15675  prodmolem3  15893  prodmolem2  15895  zprod  15897  risefallfac  15984  bpolylem  16008  phicl2  16733  phibnd  16736  hashdvds  16740  phiprmpw  16741  eulerth  16748  pcfac  16865  prmreclem2  16883  prmreclem3  16884  prmreclem4  16885  prmreclem5  16886  prmrec  16888  1arith  16893  vdwlem6  16952  vdwlem10  16956  vdwlem12  16958  prmdvdsprmo  17008  prmgaplcmlem1  17017  prmgaplcm  17026  isstruct2  17114  gsumval3lem1  19875  gsumval3lem2  19876  gsumval3  19877  coe1mul2  22248  ehleudis  25399  ehleudisval  25400  ovoliunlem2  25484  uniioombllem6  25569  itg0  25761  itgz  25762  coemullem  26229  aannenlem1  26309  aannenlem2  26310  birthdaylem1  26932  birthdaylem2  26933  wilthlem2  27050  wilthlem3  27051  ftalem5  27058  ppifi  27087  prmdvdsfi  27088  chtdif  27139  ppidif  27144  chp1  27148  ppiltx  27158  prmorcht  27159  mumul  27162  sqff1o  27163  ppiub  27185  pclogsum  27196  logexprlim  27206  gausslemma2dlem1  27347  gausslemma2dlem5  27352  gausslemma2dlem6  27353  lgseisenlem2  27357  axlowdimlem16  29044  konigsberglem5  30345  pmtrto1cl  33179  psgnfzto1stlem  33180  fzto1st  33183  psgnfzto1st  33185  smatcl  33966  1smat1  33968  esumpcvgval  34242  esumcvg  34250  carsggect  34482  carsgclctunlem2  34483  oddpwdc  34518  eulerpartlemb  34532  ballotlem1  34651  ballotlem2  34653  ballotlemfelz  34655  ballotlemfp1  34656  ballotlemfc0  34657  ballotlemfcc  34658  ballotlemfmpn  34659  ballotlemiex  34666  ballotlemsup  34669  ballotlemfg  34690  ballotlemfrc  34691  ballotlemfrceq  34693  ballotth  34702  plymulx0  34711  fsum2dsub  34771  reprfi2  34787  breprexpnat  34798  hgt750lemb  34820  hgt750leme  34822  pthhashvtx  35330  subfacf  35377  subfacp1lem1  35381  subfacp1lem3  35384  subfacp1lem5  35386  subfacp1lem6  35387  erdszelem2  35394  erdszelem10  35402  cvmliftlem15  35500  bcprod  35940  ptrecube  37961  poimirlem25  37986  poimirlem26  37987  poimirlem27  37988  poimirlem28  37989  poimirlem29  37990  poimirlem30  37991  poimirlem31  37992  poimirlem32  37993  mblfinlem2  37999  volsupnfl  38006  itg2addnclem2  38013  nnubfi  38091  nninfnub  38092  cntotbnd  38137  lcmfunnnd  42471  lcmineqlem4  42491  lcmineqlem6  42493  lcmineqlem15  42502  lcmineqlem16  42503  lcmineqlem19  42506  lcmineqlem20  42507  lcmineqlem21  42508  lcmineqlem22  42509  sticksstones17  42622  fisdomnn  42703  fz1sumconst  42761  eldioph2lem1  43212  eldioph2lem2  43213  eldioph2  43214  pellexlem5  43285  pellex  43287  jm2.22  43447  jm2.23  43448  hbt  43582  rp-isfinite6  43969  fzisoeu  45757  sumnnodd  46084  stoweidlem37  46489  stoweidlem44  46496  stoweidlem59  46511  fourierdlem37  46596  fourierdlem103  46661  fourierdlem104  46662  etransclem16  46702  etransclem24  46710  etransclem25  46711  etransclem33  46719  etransclem35  46721  etransclem44  46730  etransclem45  46731  sge0reuz  46899  hoidmvlelem2  47048  aacllem  50294