fsuppmapnn0fiub

Description: If all functions of a finite set of functions over the nonnegative integers are finitely supported, then the support of all these functions is contained in a finite set of sequential integers starting at 0 and ending with the supremum of the union of the support of these functions. (Contributed by AV, 2-Oct-2019) (Proof shortened by JJ, 2-Aug-2021)

	Ref	Expression
Hypotheses	fsuppmapnn0fiub.u	$⊢ U = ⋃_{f \in M} {supp}_{Z} (f)$
	fsuppmapnn0fiub.s	$⊢ S = sup (U ℝ <)$
Assertion	fsuppmapnn0fiub	$⊢ (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \to ((\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset) \to \forall f \in M f supp Z \subseteq (0 \dots S))$

Proof

Step	Hyp	Ref	Expression
1		fsuppmapnn0fiub.u	$⊢ U = ⋃_{f \in M} {supp}_{Z} (f)$
2		fsuppmapnn0fiub.s	$⊢ S = sup (U ℝ <)$
3		nfv	$⊢ Ⅎ f (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V)$
4		nfra1	$⊢ Ⅎ f \forall f \in M {finSupp}_{Z} (f)$
5		nfv	$⊢ Ⅎ f U \neq \emptyset$
6	4 5	nfan	$⊢ Ⅎ f (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)$
7	3 6	nfan	$⊢ Ⅎ f ((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset))$
8		suppssdm	$⊢ f supp Z \subseteq dom f$
9		ssel2	$⊢ (M \subseteq R^{ℕ_{0}} \land f \in M) \to f \in (R^{ℕ_{0}})$
10		elmapfn	$⊢ f \in (R^{ℕ_{0}}) \to f Fn ℕ_{0}$
11		fndm	$⊢ f Fn ℕ_{0} \to dom f = ℕ_{0}$
12		eqimss	$⊢ dom f = ℕ_{0} \to dom f \subseteq ℕ_{0}$
13	9 10 11 12	4syl	$⊢ (M \subseteq R^{ℕ_{0}} \land f \in M) \to dom f \subseteq ℕ_{0}$
14	13	3ad2antl1	$⊢ ((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land f \in M) \to dom f \subseteq ℕ_{0}$
15	8 14	sstrid	$⊢ ((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land f \in M) \to f supp Z \subseteq ℕ_{0}$
16	15	sseld	$⊢ ((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land f \in M) \to (x \in {supp}_{Z} (f) \to x \in ℕ_{0})$
17	16	adantlr	$⊢ (((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \land f \in M) \to (x \in {supp}_{Z} (f) \to x \in ℕ_{0})$
18	17	imp	$⊢ ((((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \land f \in M) \land x \in {supp}_{Z} (f)) \to x \in ℕ_{0}$
19	1 2	fsuppmapnn0fiublem	$⊢ (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \to ((\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset) \to S \in ℕ_{0})$
20	19	imp	$⊢ ((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \to S \in ℕ_{0}$
21	20	ad2antrr	$⊢ ((((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \land f \in M) \land x \in {supp}_{Z} (f)) \to S \in ℕ_{0}$
22	9 10 11	3syl	$⊢ (M \subseteq R^{ℕ_{0}} \land f \in M) \to dom f = ℕ_{0}$
23	22	ex	$⊢ M \subseteq R^{ℕ_{0}} \to (f \in M \to dom f = ℕ_{0})$
24	23	3ad2ant1	$⊢ (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \to (f \in M \to dom f = ℕ_{0})$
25	24	adantr	$⊢ ((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \to (f \in M \to dom f = ℕ_{0})$
26	25	imp	$⊢ (((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \land f \in M) \to dom f = ℕ_{0}$
27		nn0ssre	$⊢ ℕ_{0} \subseteq ℝ$
28	26 27	eqsstrdi	$⊢ (((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \land f \in M) \to dom f \subseteq ℝ$
29	8 28	sstrid	$⊢ (((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \land f \in M) \to f supp Z \subseteq ℝ$
30	29	ex	$⊢ ((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \to (f \in M \to f supp Z \subseteq ℝ)$
31	7 30	ralrimi	$⊢ ((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \to \forall f \in M f supp Z \subseteq ℝ$
32	31	ad2antrr	$⊢ ((((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \land f \in M) \land x \in {supp}_{Z} (f)) \to \forall f \in M f supp Z \subseteq ℝ$
33		iunss	$⊢ ⋃_{f \in M} {supp}_{Z} (f) \subseteq ℝ \leftrightarrow \forall f \in M f supp Z \subseteq ℝ$
34	32 33	sylibr	$⊢ ((((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \land f \in M) \land x \in {supp}_{Z} (f)) \to ⋃_{f \in M} {supp}_{Z} (f) \subseteq ℝ$
35	1 34	eqsstrid	$⊢ ((((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \land f \in M) \land x \in {supp}_{Z} (f)) \to U \subseteq ℝ$
36		simp2	$⊢ (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \to M \in Fin$
37		id	$⊢ {finSupp}_{Z} (f) \to {finSupp}_{Z} (f)$
38	37	fsuppimpd	$⊢ {finSupp}_{Z} (f) \to f supp Z \in Fin$
39	38	ralimi	$⊢ \forall f \in M {finSupp}_{Z} (f) \to \forall f \in M f supp Z \in Fin$
40	39	adantr	$⊢ (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset) \to \forall f \in M f supp Z \in Fin$
41	36 40	anim12i	$⊢ ((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \to (M \in Fin \land \forall f \in M f supp Z \in Fin)$
42	41	ad2antrr	$⊢ ((((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \land f \in M) \land x \in {supp}_{Z} (f)) \to (M \in Fin \land \forall f \in M f supp Z \in Fin)$
43		iunfi	$⊢ (M \in Fin \land \forall f \in M f supp Z \in Fin) \to ⋃_{f \in M} {supp}_{Z} (f) \in Fin$
44	42 43	syl	$⊢ ((((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \land f \in M) \land x \in {supp}_{Z} (f)) \to ⋃_{f \in M} {supp}_{Z} (f) \in Fin$
45	1 44	eqeltrid	$⊢ ((((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \land f \in M) \land x \in {supp}_{Z} (f)) \to U \in Fin$
46		rspe	$⊢ (f \in M \land x \in {supp}_{Z} (f)) \to \exists f \in M x \in {supp}_{Z} (f)$
47		eliun	$⊢ x \in ⋃_{f \in M} {supp}_{Z} (f) \leftrightarrow \exists f \in M x \in {supp}_{Z} (f)$
48	46 47	sylibr	$⊢ (f \in M \land x \in {supp}_{Z} (f)) \to x \in ⋃_{f \in M} {supp}_{Z} (f)$
49	48 1	eleqtrrdi	$⊢ (f \in M \land x \in {supp}_{Z} (f)) \to x \in U$
50	49	adantll	$⊢ ((((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \land f \in M) \land x \in {supp}_{Z} (f)) \to x \in U$
51	2	a1i	$⊢ ((((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \land f \in M) \land x \in {supp}_{Z} (f)) \to S = sup (U ℝ <)$
52	35 45 50 51	supfirege	$⊢ ((((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \land f \in M) \land x \in {supp}_{Z} (f)) \to x \leq S$
53		elfz2nn0	$⊢ x \in (0 \dots S) \leftrightarrow (x \in ℕ_{0} \land S \in ℕ_{0} \land x \leq S)$
54	18 21 52 53	syl3anbrc	$⊢ ((((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \land f \in M) \land x \in {supp}_{Z} (f)) \to x \in (0 \dots S)$
55	54	ex	$⊢ (((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \land f \in M) \to (x \in {supp}_{Z} (f) \to x \in (0 \dots S))$
56	55	ssrdv	$⊢ (((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \land f \in M) \to f supp Z \subseteq (0 \dots S)$
57	56	ex	$⊢ ((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \to (f \in M \to f supp Z \subseteq (0 \dots S))$
58	7 57	ralrimi	$⊢ ((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset)) \to \forall f \in M f supp Z \subseteq (0 \dots S)$
59	58	ex	$⊢ (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \to ((\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset) \to \forall f \in M f supp Z \subseteq (0 \dots S))$

Metamath Proof Explorer

Theorem fsuppmapnn0fiub

Proof