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 sselid 
 |-  ( 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