fsuppmapnn0fiub0

Description: If all functions of a finite set of functions over the nonnegative integers are finitely supported, then all these functions are zero for all integers greater than a fixed integer. (Contributed by AV, 3-Oct-2019)

		Ref	Expression
	Assertion	fsuppmapnn0fiub0	$⊢ (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \to (\forall f \in M {finSupp}_{Z} (f) \to \exists m \in ℕ_{0} \forall f \in M \forall x \in ℕ_{0} (m < x \to f (x) = Z))$

Proof

Step	Hyp	Ref	Expression
1		fsuppmapnn0fiubex	$⊢ (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \to (\forall f \in M {finSupp}_{Z} (f) \to \exists m \in ℕ_{0} \forall f \in M f supp Z \subseteq (0 \dots m))$
2		ssel2	$⊢ (M \subseteq R^{ℕ_{0}} \land f \in M) \to f \in (R^{ℕ_{0}})$
3	2	ancoms	$⊢ (f \in M \land M \subseteq R^{ℕ_{0}}) \to f \in (R^{ℕ_{0}})$
4		elmapfn	$⊢ f \in (R^{ℕ_{0}}) \to f Fn ℕ_{0}$
5	3 4	syl	$⊢ (f \in M \land M \subseteq R^{ℕ_{0}}) \to f Fn ℕ_{0}$
6	5	expcom	$⊢ M \subseteq R^{ℕ_{0}} \to (f \in M \to f Fn ℕ_{0})$
7	6	3ad2ant1	$⊢ (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \to (f \in M \to f Fn ℕ_{0})$
8	7	adantr	$⊢ ((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land m \in ℕ_{0}) \to (f \in M \to f Fn ℕ_{0})$
9	8	imp	$⊢ (((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land m \in ℕ_{0}) \land f \in M) \to f Fn ℕ_{0}$
10		nn0ex	$⊢ ℕ_{0} \in V$
11	10	a1i	$⊢ (((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land m \in ℕ_{0}) \land f \in M) \to ℕ_{0} \in V$
12		simpll3	$⊢ (((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land m \in ℕ_{0}) \land f \in M) \to Z \in V$
13		suppvalfn	$⊢ (f Fn ℕ_{0} \land ℕ_{0} \in V \land Z \in V) \to f supp Z = \{x \in ℕ_{0} \| f (x) \neq Z\}$
14	9 11 12 13	syl3anc	$⊢ (((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land m \in ℕ_{0}) \land f \in M) \to f supp Z = \{x \in ℕ_{0} \| f (x) \neq Z\}$
15	14	sseq1d	$⊢ (((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land m \in ℕ_{0}) \land f \in M) \to (f supp Z \subseteq (0 \dots m) \leftrightarrow \{x \in ℕ_{0} \| f (x) \neq Z\} \subseteq (0 \dots m))$
16		rabss	$⊢ \{x \in ℕ_{0} \| f (x) \neq Z\} \subseteq (0 \dots m) \leftrightarrow \forall x \in ℕ_{0} (f (x) \neq Z \to x \in (0 \dots m))$
17	15 16	bitrdi	$⊢ (((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land m \in ℕ_{0}) \land f \in M) \to (f supp Z \subseteq (0 \dots m) \leftrightarrow \forall x \in ℕ_{0} (f (x) \neq Z \to x \in (0 \dots m)))$
18		nne	$⊢ \neg f (x) \neq Z \leftrightarrow f (x) = Z$
19	18	biimpi	$⊢ \neg f (x) \neq Z \to f (x) = Z$
20	19	2a1d	$⊢ \neg f (x) \neq Z \to (((((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land m \in ℕ_{0}) \land f \in M) \land x \in ℕ_{0}) \to (m < x \to f (x) = Z))$
21		elfz2nn0	$⊢ x \in (0 \dots m) \leftrightarrow (x \in ℕ_{0} \land m \in ℕ_{0} \land x \leq m)$
22		nn0re	$⊢ x \in ℕ_{0} \to x \in ℝ$
23		nn0re	$⊢ m \in ℕ_{0} \to m \in ℝ$
24		lenlt	$⊢ (x \in ℝ \land m \in ℝ) \to (x \leq m \leftrightarrow \neg m < x)$
25	22 23 24	syl2an	$⊢ (x \in ℕ_{0} \land m \in ℕ_{0}) \to (x \leq m \leftrightarrow \neg m < x)$
26		pm2.21	$⊢ \neg m < x \to (m < x \to f (x) = Z)$
27	25 26	syl6bi	$⊢ (x \in ℕ_{0} \land m \in ℕ_{0}) \to (x \leq m \to (m < x \to f (x) = Z))$
28	27	3impia	$⊢ (x \in ℕ_{0} \land m \in ℕ_{0} \land x \leq m) \to (m < x \to f (x) = Z)$
29	28	a1d	$⊢ (x \in ℕ_{0} \land m \in ℕ_{0} \land x \leq m) \to (((((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land m \in ℕ_{0}) \land f \in M) \land x \in ℕ_{0}) \to (m < x \to f (x) = Z))$
30	21 29	sylbi	$⊢ x \in (0 \dots m) \to (((((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land m \in ℕ_{0}) \land f \in M) \land x \in ℕ_{0}) \to (m < x \to f (x) = Z))$
31	20 30	ja	$⊢ (f (x) \neq Z \to x \in (0 \dots m)) \to (((((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land m \in ℕ_{0}) \land f \in M) \land x \in ℕ_{0}) \to (m < x \to f (x) = Z))$
32	31	com12	$⊢ ((((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land m \in ℕ_{0}) \land f \in M) \land x \in ℕ_{0}) \to ((f (x) \neq Z \to x \in (0 \dots m)) \to (m < x \to f (x) = Z))$
33	32	ralimdva	$⊢ (((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land m \in ℕ_{0}) \land f \in M) \to (\forall x \in ℕ_{0} (f (x) \neq Z \to x \in (0 \dots m)) \to \forall x \in ℕ_{0} (m < x \to f (x) = Z))$
34	17 33	sylbid	$⊢ (((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land m \in ℕ_{0}) \land f \in M) \to (f supp Z \subseteq (0 \dots m) \to \forall x \in ℕ_{0} (m < x \to f (x) = Z))$
35	34	ralimdva	$⊢ ((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land m \in ℕ_{0}) \to (\forall f \in M f supp Z \subseteq (0 \dots m) \to \forall f \in M \forall x \in ℕ_{0} (m < x \to f (x) = Z))$
36	35	reximdva	$⊢ (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \to (\exists m \in ℕ_{0} \forall f \in M f supp Z \subseteq (0 \dots m) \to \exists m \in ℕ_{0} \forall f \in M \forall x \in ℕ_{0} (m < x \to f (x) = Z))$
37	1 36	syld	$⊢ (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \to (\forall f \in M {finSupp}_{Z} (f) \to \exists m \in ℕ_{0} \forall f \in M \forall x \in ℕ_{0} (m < x \to f (x) = Z))$

Metamath Proof Explorer

Theorem fsuppmapnn0fiub0

Proof