Metamath Proof Explorer

Theorem fz1eqb

Description: Two possibly-empty 1-based finite sets of sequential integers are equal iff their endpoints are equal. (Contributed by Paul Chapman, 22-Jun-2011) (Proof shortened by Mario Carneiro, 29-Mar-2014)

Ref Expression
Assertion fz1eqb 
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( 1 ... M ) = ( 1 ... N ) <-> M = N ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( ( 1 ... M ) = ( 1 ... N ) -> ( # ` ( 1 ... M ) ) = ( # ` ( 1 ... N ) ) )
2 hashfz1 
 |-  ( M e. NN0 -> ( # ` ( 1 ... M ) ) = M )
3 hashfz1 
 |-  ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
4 2 3 eqeqan12d 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( # ` ( 1 ... M ) ) = ( # ` ( 1 ... N ) ) <-> M = N ) )
5 1 4 syl5ib 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( 1 ... M ) = ( 1 ... N ) -> M = N ) )
6 oveq2 
 |-  ( M = N -> ( 1 ... M ) = ( 1 ... N ) )
7 5 6 impbid1 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( 1 ... M ) = ( 1 ... N ) <-> M = N ) )