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	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \left(\left(1\dots M\right)=\left(1\dots N\right)\leftrightarrow M=N\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢\left(1\dots M\right)=\left(1\dots N\right)\to \left|\left(1\dots M\right)\right|=\left|\left(1\dots N\right)\right|$$
2		hashfz1	$$⊢M\in {\mathbb{N}}_0\to \left|\left(1\dots M\right)\right|=M$$
3		hashfz1	$$⊢N\in {\mathbb{N}}_0\to \left|\left(1\dots N\right)\right|=N$$
4	2 3	eqeqan12d	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \left(\left|\left(1\dots M\right)\right|=\left|\left(1\dots N\right)\right|\leftrightarrow M=N\right)$$
5	1 4	imbitrid	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \left(\left(1\dots M\right)=\left(1\dots N\right)\to M=N\right)$$
6		oveq2	$$⊢M=N\to \left(1\dots M\right)=\left(1\dots N\right)$$
7	5 6	impbid1	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \left(\left(1\dots M\right)=\left(1\dots N\right)\leftrightarrow M=N\right)$$