Theorem fseq1hash

Description: The value of the size function on a finite 1-based sequence. (Contributed by Paul Chapman, 26-Oct-2012) (Proof shortened by Mario Carneiro, 12-Mar-2015)

	Ref	Expression
Assertion	fseq1hash	$$⊢\left(N\in {\mathbb{N}}_0\wedge FFn\left(1\dots N\right)\right)\to \left|F\right|=N$$

Proof

Step	Hyp	Ref	Expression
1		hashfn	$$⊢FFn\left(1\dots N\right)\to \left|F\right|=\left|\left(1\dots N\right)\right|$$
2		hashfz1	$$⊢N\in {\mathbb{N}}_0\to \left|\left(1\dots N\right)\right|=N$$
3	1 2	sylan9eqr	$$⊢\left(N\in {\mathbb{N}}_0\wedge FFn\left(1\dots N\right)\right)\to \left|F\right|=N$$