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 ... 𝑁 ) ↔ 𝑀 = 𝑁 ) )