# 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
`|- ( M ... N ) e. Fin`

### Proof

Step Hyp Ref Expression
1 0fin
` |-  (/) e. Fin`
2 eleq1
` |-  ( ( M ... N ) = (/) -> ( ( M ... N ) e. Fin <-> (/) e. Fin ) )`
3 1 2 mpbiri
` |-  ( ( M ... N ) = (/) -> ( M ... N ) e. Fin )`
4 fzn0
` |-  ( ( M ... N ) =/= (/) <-> N e. ( ZZ>= ` M ) )`
5 onfin2
` |-  _om = ( On i^i Fin )`
6 inss2
` |-  ( On i^i Fin ) C_ Fin`
7 5 6 eqsstri
` |-  _om C_ Fin`
8 eqid
` |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )`
9 8 hashgf1o
` |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) : _om -1-1-onto-> NN0`
10 peano2uz
` |-  ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )`
11 uznn0sub
` |-  ( ( N + 1 ) e. ( ZZ>= ` M ) -> ( ( N + 1 ) - M ) e. NN0 )`
12 10 11 syl
` |-  ( N e. ( ZZ>= ` M ) -> ( ( N + 1 ) - M ) e. NN0 )`
13 f1ocnvdm
` |-  ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) : _om -1-1-onto-> NN0 /\ ( ( N + 1 ) - M ) e. NN0 ) -> ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( N + 1 ) - M ) ) e. _om )`
14 9 12 13 sylancr
` |-  ( N e. ( ZZ>= ` M ) -> ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( N + 1 ) - M ) ) e. _om )`
15 7 14 sseldi
` |-  ( N e. ( ZZ>= ` M ) -> ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( N + 1 ) - M ) ) e. Fin )`
16 8 fzen2
` |-  ( N e. ( ZZ>= ` M ) -> ( M ... N ) ~~ ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( N + 1 ) - M ) ) )`
17 enfii
` |-  ( ( ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( N + 1 ) - M ) ) e. Fin /\ ( M ... N ) ~~ ( `' ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) ` ( ( N + 1 ) - M ) ) ) -> ( M ... N ) e. Fin )`
18 15 16 17 syl2anc
` |-  ( N e. ( ZZ>= ` M ) -> ( M ... N ) e. Fin )`
19 4 18 sylbi
` |-  ( ( M ... N ) =/= (/) -> ( M ... N ) e. Fin )`
20 3 19 pm2.61ine
` |-  ( M ... N ) e. Fin`