fsuppmapnn0fiubex

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. (Contributed by AV, 2-Oct-2019)

		Ref	Expression
	Assertion	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))$

Proof

Step	Hyp	Ref	Expression
1		0nn0	$⊢ 0 \in ℕ_{0}$
2	1	a1i	$⊢ (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \to 0 \in ℕ_{0}$
3		oveq2	$⊢ m = 0 \to (0 \dots m) = (0 \dots 0)$
4	3	sseq2d	$⊢ m = 0 \to (f supp Z \subseteq (0 \dots m) \leftrightarrow f supp Z \subseteq (0 \dots 0))$
5	4	ralbidv	$⊢ m = 0 \to (\forall f \in M f supp Z \subseteq (0 \dots m) \leftrightarrow \forall f \in M f supp Z \subseteq (0 \dots 0))$
6	5	adantl	$⊢ ((\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \land m = 0) \to (\forall f \in M f supp Z \subseteq (0 \dots m) \leftrightarrow \forall f \in M f supp Z \subseteq (0 \dots 0))$
7		ral0	$⊢ \forall f \in \emptyset f supp Z \subseteq (0 \dots 0)$
8		raleq	$⊢ \emptyset = M \to (\forall f \in \emptyset f supp Z \subseteq (0 \dots 0) \leftrightarrow \forall f \in M f supp Z \subseteq (0 \dots 0))$
9	7 8	mpbii	$⊢ \emptyset = M \to \forall f \in M f supp Z \subseteq (0 \dots 0)$
10		0ss	$⊢ \emptyset \subseteq (0 \dots 0)$
11		sseq1	$⊢ f supp Z = \emptyset \to (f supp Z \subseteq (0 \dots 0) \leftrightarrow \emptyset \subseteq (0 \dots 0))$
12	10 11	mpbiri	$⊢ f supp Z = \emptyset \to f supp Z \subseteq (0 \dots 0)$
13	12	ralimi	$⊢ \forall f \in M f supp Z = \emptyset \to \forall f \in M f supp Z \subseteq (0 \dots 0)$
14	9 13	jaoi	$⊢ (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \to \forall f \in M f supp Z \subseteq (0 \dots 0)$
15	2 6 14	rspcedvd	$⊢ (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \to \exists m \in ℕ_{0} \forall f \in M f supp Z \subseteq (0 \dots m)$
16	15	2a1d	$⊢ (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \to ((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)))$
17		simplr	$⊢ ((\neg (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \land (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V)) \land \forall f \in M {finSupp}_{Z} (f)) \to (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V)$
18		simpr	$⊢ ((\neg (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \land (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V)) \land \forall f \in M {finSupp}_{Z} (f)) \to \forall f \in M {finSupp}_{Z} (f)$
19		ioran	$⊢ \neg (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \leftrightarrow (\neg \emptyset = M \land \neg \forall f \in M f supp Z = \emptyset)$
20		oveq1	$⊢ f = g \to f supp Z = g supp Z$
21	20	eqeq1d	$⊢ f = g \to (f supp Z = \emptyset \leftrightarrow g supp Z = \emptyset)$
22	21	cbvralvw	$⊢ \forall f \in M f supp Z = \emptyset \leftrightarrow \forall g \in M g supp Z = \emptyset$
23	22	notbii	$⊢ \neg \forall f \in M f supp Z = \emptyset \leftrightarrow \neg \forall g \in M g supp Z = \emptyset$
24	23	anbi2i	$⊢ (\neg \emptyset = M \land \neg \forall f \in M f supp Z = \emptyset) \leftrightarrow (\neg \emptyset = M \land \neg \forall g \in M g supp Z = \emptyset)$
25	19 24	bitri	$⊢ \neg (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \leftrightarrow (\neg \emptyset = M \land \neg \forall g \in M g supp Z = \emptyset)$
26		rexnal	$⊢ \exists g \in M \neg g supp Z = \emptyset \leftrightarrow \neg \forall g \in M g supp Z = \emptyset$
27		df-ne	$⊢ g supp Z \neq \emptyset \leftrightarrow \neg g supp Z = \emptyset$
28	27	bicomi	$⊢ \neg g supp Z = \emptyset \leftrightarrow g supp Z \neq \emptyset$
29	28	rexbii	$⊢ \exists g \in M \neg g supp Z = \emptyset \leftrightarrow \exists g \in M g supp Z \neq \emptyset$
30	26 29	sylbb1	$⊢ \neg \forall g \in M g supp Z = \emptyset \to \exists g \in M g supp Z \neq \emptyset$
31	25 30	simplbiim	$⊢ \neg (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \to \exists g \in M g supp Z \neq \emptyset$
32	31	ad2antrr	$⊢ ((\neg (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \land (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V)) \land \forall f \in M {finSupp}_{Z} (f)) \to \exists g \in M g supp Z \neq \emptyset$
33		iunn0	$⊢ \exists g \in M g supp Z \neq \emptyset \leftrightarrow ⋃_{g \in M} {supp}_{Z} (g) \neq \emptyset$
34	32 33	sylib	$⊢ ((\neg (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \land (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V)) \land \forall f \in M {finSupp}_{Z} (f)) \to ⋃_{g \in M} {supp}_{Z} (g) \neq \emptyset$
35	18 34	jca	$⊢ ((\neg (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \land (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V)) \land \forall f \in M {finSupp}_{Z} (f)) \to (\forall f \in M {finSupp}_{Z} (f) \land ⋃_{g \in M} {supp}_{Z} (g) \neq \emptyset)$
36		oveq1	$⊢ g = f \to g supp Z = f supp Z$
37	36	cbviunv	$⊢ ⋃_{g \in M} {supp}_{Z} (g) = ⋃_{f \in M} {supp}_{Z} (f)$
38		eqid	$⊢ sup (⋃_{g \in M} {supp}_{Z} (g) ℝ <) = sup (⋃_{g \in M} {supp}_{Z} (g) ℝ <)$
39	37 38	fsuppmapnn0fiublem	$⊢ (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \to ((\forall f \in M {finSupp}_{Z} (f) \land ⋃_{g \in M} {supp}_{Z} (g) \neq \emptyset) \to sup (⋃_{g \in M} {supp}_{Z} (g) ℝ <) \in ℕ_{0})$
40	17 35 39	sylc	$⊢ ((\neg (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \land (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V)) \land \forall f \in M {finSupp}_{Z} (f)) \to sup (⋃_{g \in M} {supp}_{Z} (g) ℝ <) \in ℕ_{0}$
41		nfv	$⊢ Ⅎ f \emptyset = M$
42		nfra1	$⊢ Ⅎ f \forall f \in M f supp Z = \emptyset$
43	41 42	nfor	$⊢ Ⅎ f (\emptyset = M \lor \forall f \in M f supp Z = \emptyset)$
44	43	nfn	$⊢ Ⅎ f \neg (\emptyset = M \lor \forall f \in M f supp Z = \emptyset)$
45		nfv	$⊢ Ⅎ f (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V)$
46	44 45	nfan	$⊢ Ⅎ f (\neg (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \land (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V))$
47		nfra1	$⊢ Ⅎ f \forall f \in M {finSupp}_{Z} (f)$
48	46 47	nfan	$⊢ Ⅎ f ((\neg (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \land (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V)) \land \forall f \in M {finSupp}_{Z} (f))$
49		nfv	$⊢ Ⅎ f m = sup (⋃_{g \in M} {supp}_{Z} (g) ℝ <)$
50	48 49	nfan	$⊢ Ⅎ f (((\neg (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \land (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V)) \land \forall f \in M {finSupp}_{Z} (f)) \land m = sup (⋃_{g \in M} {supp}_{Z} (g) ℝ <))$
51		oveq2	$⊢ m = sup (⋃_{g \in M} {supp}_{Z} (g) ℝ <) \to (0 \dots m) = (0 \dots sup (⋃_{g \in M} {supp}_{Z} (g) ℝ <))$
52	51	sseq2d	$⊢ m = sup (⋃_{g \in M} {supp}_{Z} (g) ℝ <) \to (f supp Z \subseteq (0 \dots m) \leftrightarrow f supp Z \subseteq (0 \dots sup (⋃_{g \in M} {supp}_{Z} (g) ℝ <)))$
53	52	adantl	$⊢ (((\neg (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \land (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V)) \land \forall f \in M {finSupp}_{Z} (f)) \land m = sup (⋃_{g \in M} {supp}_{Z} (g) ℝ <)) \to (f supp Z \subseteq (0 \dots m) \leftrightarrow f supp Z \subseteq (0 \dots sup (⋃_{g \in M} {supp}_{Z} (g) ℝ <)))$
54	50 53	ralbid	$⊢ (((\neg (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \land (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V)) \land \forall f \in M {finSupp}_{Z} (f)) \land m = sup (⋃_{g \in M} {supp}_{Z} (g) ℝ <)) \to (\forall f \in M f supp Z \subseteq (0 \dots m) \leftrightarrow \forall f \in M f supp Z \subseteq (0 \dots sup (⋃_{g \in M} {supp}_{Z} (g) ℝ <)))$
55		rexnal	$⊢ \exists f \in M \neg f supp Z = \emptyset \leftrightarrow \neg \forall f \in M f supp Z = \emptyset$
56		df-ne	$⊢ f supp Z \neq \emptyset \leftrightarrow \neg f supp Z = \emptyset$
57	56	bicomi	$⊢ \neg f supp Z = \emptyset \leftrightarrow f supp Z \neq \emptyset$
58	57	rexbii	$⊢ \exists f \in M \neg f supp Z = \emptyset \leftrightarrow \exists f \in M f supp Z \neq \emptyset$
59	55 58	sylbb1	$⊢ \neg \forall f \in M f supp Z = \emptyset \to \exists f \in M f supp Z \neq \emptyset$
60	19 59	simplbiim	$⊢ \neg (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \to \exists f \in M f supp Z \neq \emptyset$
61	60	ad2antrr	$⊢ ((\neg (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \land (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V)) \land \forall f \in M {finSupp}_{Z} (f)) \to \exists f \in M f supp Z \neq \emptyset$
62		iunn0	$⊢ \exists f \in M f supp Z \neq \emptyset \leftrightarrow ⋃_{f \in M} {supp}_{Z} (f) \neq \emptyset$
63	20	cbviunv	$⊢ ⋃_{f \in M} {supp}_{Z} (f) = ⋃_{g \in M} {supp}_{Z} (g)$
64	63	neeq1i	$⊢ ⋃_{f \in M} {supp}_{Z} (f) \neq \emptyset \leftrightarrow ⋃_{g \in M} {supp}_{Z} (g) \neq \emptyset$
65	62 64	bitri	$⊢ \exists f \in M f supp Z \neq \emptyset \leftrightarrow ⋃_{g \in M} {supp}_{Z} (g) \neq \emptyset$
66	61 65	sylib	$⊢ ((\neg (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \land (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V)) \land \forall f \in M {finSupp}_{Z} (f)) \to ⋃_{g \in M} {supp}_{Z} (g) \neq \emptyset$
67	18 66	jca	$⊢ ((\neg (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \land (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V)) \land \forall f \in M {finSupp}_{Z} (f)) \to (\forall f \in M {finSupp}_{Z} (f) \land ⋃_{g \in M} {supp}_{Z} (g) \neq \emptyset)$
68	37 38	fsuppmapnn0fiub	$⊢ (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \to ((\forall f \in M {finSupp}_{Z} (f) \land ⋃_{g \in M} {supp}_{Z} (g) \neq \emptyset) \to \forall f \in M f supp Z \subseteq (0 \dots sup (⋃_{g \in M} {supp}_{Z} (g) ℝ <)))$
69	17 67 68	sylc	$⊢ ((\neg (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \land (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V)) \land \forall f \in M {finSupp}_{Z} (f)) \to \forall f \in M f supp Z \subseteq (0 \dots sup (⋃_{g \in M} {supp}_{Z} (g) ℝ <))$
70	40 54 69	rspcedvd	$⊢ ((\neg (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \land (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V)) \land \forall f \in M {finSupp}_{Z} (f)) \to \exists m \in ℕ_{0} \forall f \in M f supp Z \subseteq (0 \dots m)$
71	70	exp31	$⊢ \neg (\emptyset = M \lor \forall f \in M f supp Z = \emptyset) \to ((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)))$
72	16 71	pm2.61i	$⊢ (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))$

Metamath Proof Explorer

Theorem fsuppmapnn0fiubex

Proof