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