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

Metamath Proof Explorer

Theorem ffz0hash

Description: The size of a function on a finite set of sequential nonnegative integers equals the upper bound of the sequence increased by 1. (Contributed by Alexander van der Vekens, 15-Mar-2018) (Proof shortened by AV, 11-Apr-2021)

Ref Expression
Assertion ffz0hash ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ 𝐵 ) → ( ♯ ‘ 𝐹 ) = ( 𝑁 + 1 ) )

Proof

Step Hyp Ref Expression
1 ffn ⊢ ( 𝐹 : ( 0 ... 𝑁 ) ⟶ 𝐵 → 𝐹 Fn ( 0 ... 𝑁 ) )
2 fnfz0hash ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 Fn ( 0 ... 𝑁 ) ) → ( ♯ ‘ 𝐹 ) = ( 𝑁 + 1 ) )
3 1 2 sylan2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 : ( 0 ... 𝑁 ) ⟶ 𝐵 ) → ( ♯ ‘ 𝐹 ) = ( 𝑁 + 1 ) )