# Metamath Proof Explorer

## Theorem fzfi

Description: A finite interval of integers is finite. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 12-Mar-2015)

Ref Expression
Assertion fzfi ${⊢}\left({M}\dots {N}\right)\in \mathrm{Fin}$

### Proof

Step Hyp Ref Expression
1 0fin ${⊢}\varnothing \in \mathrm{Fin}$
2 eleq1 ${⊢}\left({M}\dots {N}\right)=\varnothing \to \left(\left({M}\dots {N}\right)\in \mathrm{Fin}↔\varnothing \in \mathrm{Fin}\right)$
3 1 2 mpbiri ${⊢}\left({M}\dots {N}\right)=\varnothing \to \left({M}\dots {N}\right)\in \mathrm{Fin}$
4 fzn0 ${⊢}\left({M}\dots {N}\right)\ne \varnothing ↔{N}\in {ℤ}_{\ge {M}}$
5 onfin2 ${⊢}\mathrm{\omega }=\mathrm{On}\cap \mathrm{Fin}$
6 inss2 ${⊢}\mathrm{On}\cap \mathrm{Fin}\subseteq \mathrm{Fin}$
7 5 6 eqsstri ${⊢}\mathrm{\omega }\subseteq \mathrm{Fin}$
8 eqid ${⊢}{\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}={\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}$
9 8 hashgf1o ${⊢}\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right):\mathrm{\omega }\underset{1-1 onto}{⟶}{ℕ}_{0}$
10 peano2uz ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}+1\in {ℤ}_{\ge {M}}$
11 uznn0sub ${⊢}{N}+1\in {ℤ}_{\ge {M}}\to {N}+1-{M}\in {ℕ}_{0}$
12 10 11 syl ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}+1-{M}\in {ℕ}_{0}$
13 f1ocnvdm ${⊢}\left(\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right):\mathrm{\omega }\underset{1-1 onto}{⟶}{ℕ}_{0}\wedge {N}+1-{M}\in {ℕ}_{0}\right)\to {\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right)}^{-1}\left({N}+1-{M}\right)\in \mathrm{\omega }$
14 9 12 13 sylancr ${⊢}{N}\in {ℤ}_{\ge {M}}\to {\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right)}^{-1}\left({N}+1-{M}\right)\in \mathrm{\omega }$
15 7 14 sseldi ${⊢}{N}\in {ℤ}_{\ge {M}}\to {\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right)}^{-1}\left({N}+1-{M}\right)\in \mathrm{Fin}$
16 8 fzen2 ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({M}\dots {N}\right)\approx {\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right)}^{-1}\left({N}+1-{M}\right)$
17 enfii ${⊢}\left({\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right)}^{-1}\left({N}+1-{M}\right)\in \mathrm{Fin}\wedge \left({M}\dots {N}\right)\approx {\left({\mathrm{rec}\left(\left({x}\in \mathrm{V}⟼{x}+1\right),0\right)↾}_{\mathrm{\omega }}\right)}^{-1}\left({N}+1-{M}\right)\right)\to \left({M}\dots {N}\right)\in \mathrm{Fin}$
18 15 16 17 syl2anc ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({M}\dots {N}\right)\in \mathrm{Fin}$
19 4 18 sylbi ${⊢}\left({M}\dots {N}\right)\ne \varnothing \to \left({M}\dots {N}\right)\in \mathrm{Fin}$
20 3 19 pm2.61ine ${⊢}\left({M}\dots {N}\right)\in \mathrm{Fin}$