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	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 Fn ( 1 ... 𝑁 ) ) → ( ♯ ‘ 𝐹 ) = 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		hashfn	⊢ ( 𝐹 Fn ( 1 ... 𝑁 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ( 1 ... 𝑁 ) ) )
2		hashfz1	⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
3	1 2	sylan9eqr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 Fn ( 1 ... 𝑁 ) ) → ( ♯ ‘ 𝐹 ) = 𝑁 )