fsuppmapnn0fz

Description: If a function over the nonnegative integers is finitely supported, then there is an upper bound for a finite set of sequential integers containing the support of the function. (Contributed by AV, 30-Sep-2019) (Proof shortened by AV, 6-Oct-2019)

		Ref	Expression
	Assertion	fsuppmapnn0fz	$⊢ (F \in (R^{ℕ_{0}}) \land Z \in V) \to ({finSupp}_{Z} (F) \to \exists m \in ℕ_{0} F supp Z \subseteq (0 \dots m))$

Proof

Step	Hyp	Ref	Expression
1		fsuppmapnn0ub	$⊢ (F \in (R^{ℕ_{0}}) \land Z \in V) \to ({finSupp}_{Z} (F) \to \exists m \in ℕ_{0} \forall x \in ℕ_{0} (m < x \to F (x) = Z))$
2		simpllr	$⊢ (((F \in (R^{ℕ_{0}}) \land Z \in V) \land m \in ℕ_{0}) \land \forall x \in ℕ_{0} (m < x \to F (x) = Z)) \to Z \in V$
3		simplll	$⊢ (((F \in (R^{ℕ_{0}}) \land Z \in V) \land m \in ℕ_{0}) \land \forall x \in ℕ_{0} (m < x \to F (x) = Z)) \to F \in (R^{ℕ_{0}})$
4		simplr	$⊢ (((F \in (R^{ℕ_{0}}) \land Z \in V) \land m \in ℕ_{0}) \land \forall x \in ℕ_{0} (m < x \to F (x) = Z)) \to m \in ℕ_{0}$
5		simpr	$⊢ (((F \in (R^{ℕ_{0}}) \land Z \in V) \land m \in ℕ_{0}) \land \forall x \in ℕ_{0} (m < x \to F (x) = Z)) \to \forall x \in ℕ_{0} (m < x \to F (x) = Z)$
6	2 3 4 5	suppssfz	$⊢ (((F \in (R^{ℕ_{0}}) \land Z \in V) \land m \in ℕ_{0}) \land \forall x \in ℕ_{0} (m < x \to F (x) = Z)) \to F supp Z \subseteq (0 \dots m)$
7	6	ex	$⊢ ((F \in (R^{ℕ_{0}}) \land Z \in V) \land m \in ℕ_{0}) \to (\forall x \in ℕ_{0} (m < x \to F (x) = Z) \to F supp Z \subseteq (0 \dots m))$
8	7	reximdva	$⊢ (F \in (R^{ℕ_{0}}) \land Z \in V) \to (\exists m \in ℕ_{0} \forall x \in ℕ_{0} (m < x \to F (x) = Z) \to \exists m \in ℕ_{0} F supp Z \subseteq (0 \dots m))$
9	1 8	syld	$⊢ (F \in (R^{ℕ_{0}}) \land Z \in V) \to ({finSupp}_{Z} (F) \to \exists m \in ℕ_{0} F supp Z \subseteq (0 \dots m))$

Metamath Proof Explorer

Theorem fsuppmapnn0fz

Proof