This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 1 ... 𝑀 ) = ( 1 ... 𝑁 ) ↔ 𝑀 = 𝑁 ) )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( ( 1 ... 𝑀 ) = ( 1 ... 𝑁 ) → ( ♯ ‘ ( 1 ... 𝑀 ) ) = ( ♯ ‘ ( 1 ... 𝑁 ) ) )
2 hashfz1 ⊢ ( 𝑀 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 )
3 hashfz1 ⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
4 2 3 eqeqan12d ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ ( 1 ... 𝑀 ) ) = ( ♯ ‘ ( 1 ... 𝑁 ) ) ↔ 𝑀 = 𝑁 ) )
5 1 4 imbitrid ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 1 ... 𝑀 ) = ( 1 ... 𝑁 ) → 𝑀 = 𝑁 ) )
6 oveq2 ⊢ ( 𝑀 = 𝑁 → ( 1 ... 𝑀 ) = ( 1 ... 𝑁 ) )
7 5 6 impbid1 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 1 ... 𝑀 ) = ( 1 ... 𝑁 ) ↔ 𝑀 = 𝑁 ) )