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	$⊢ (N \in ℕ_{0} \land F : (0 \dots N) ⟶ B) \to \|F\| = N + 1$

Proof

Step	Hyp	Ref	Expression
1		ffn	$⊢ F : (0 \dots N) ⟶ B \to F Fn (0 \dots N)$
2		fnfz0hash	$⊢ (N \in ℕ_{0} \land F Fn (0 \dots N)) \to \|F\| = N + 1$
3	1 2	sylan2	$⊢ (N \in ℕ_{0} \land F : (0 \dots N) ⟶ B) \to \|F\| = N + 1$