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	11 12	syl	$⊢ f Fn ℕ_{0} \to dom f \subseteq ℕ_{0}$
14	9 10 13	3syl	$⊢ (M \subseteq R^{ℕ_{0}} \land f \in M) \to dom f \subseteq ℕ_{0}$
15	14	3ad2antl1	$⊢ ((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land f \in M) \to dom f \subseteq ℕ_{0}$
16	8 15	sstrid	$⊢ ((M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \land f \in M) \to f supp Z \subseteq ℕ_{0}$
17	16	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})$
18	17	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})$
19	18	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}$
20	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})$
21	20	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}$
22	21	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}$
23	9 10 11	3syl	$⊢ (M \subseteq R^{ℕ_{0}} \land f \in M) \to dom f = ℕ_{0}$
24	23	ex	$⊢ M \subseteq R^{ℕ_{0}} \to (f \in M \to dom f = ℕ_{0})$
25	24	3ad2ant1	$⊢ (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \to (f \in M \to dom f = ℕ_{0})$
26	25	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})$
27	26	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}$
28		nn0ssre	$⊢ ℕ_{0} \subseteq ℝ$
29	27 28	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 ℝ$
30	8 29	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 ℝ$
31	30	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 ℝ)$
32	7 31	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 ℝ$
33	32	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 ℝ$
34		iunss	$⊢ ⋃_{f \in M} {supp}_{Z} (f) \subseteq ℝ \leftrightarrow \forall f \in M f supp Z \subseteq ℝ$
35	33 34	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 ℝ$
36	1 35	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 ℝ$
37		simp2	$⊢ (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \to M \in Fin$
38		id	$⊢ {finSupp}_{Z} (f) \to {finSupp}_{Z} (f)$
39	38	fsuppimpd	$⊢ {finSupp}_{Z} (f) \to f supp Z \in Fin$
40	39	ralimi	$⊢ \forall f \in M {finSupp}_{Z} (f) \to \forall f \in M f supp Z \in Fin$
41	40	adantr	$⊢ (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset) \to \forall f \in M f supp Z \in Fin$
42	37 41	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)$
43	42	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)$
44		iunfi	$⊢ (M \in Fin \land \forall f \in M f supp Z \in Fin) \to ⋃_{f \in M} {supp}_{Z} (f) \in Fin$
45	43 44	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$
46	1 45	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$
47		rspe	$⊢ (f \in M \land x \in {supp}_{Z} (f)) \to \exists f \in M x \in {supp}_{Z} (f)$
48		eliun	$⊢ x \in ⋃_{f \in M} {supp}_{Z} (f) \leftrightarrow \exists f \in M x \in {supp}_{Z} (f)$
49	47 48	sylibr	$⊢ (f \in M \land x \in {supp}_{Z} (f)) \to x \in ⋃_{f \in M} {supp}_{Z} (f)$
50	49 1	eleqtrrdi	$⊢ (f \in M \land x \in {supp}_{Z} (f)) \to x \in U$
51	50	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$
52	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 ℝ <)$
53	36 46 51 52	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$
54		elfz2nn0	$⊢ x \in (0 \dots S) \leftrightarrow (x \in ℕ_{0} \land S \in ℕ_{0} \land x \leq S)$
55	19 22 53 54	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)$
56	55	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))$
57	56	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)$
58	57	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))$
59	7 58	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)$
60	59	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