fsuppmapnn0fiublem

	Ref	Expression
Hypotheses	fsuppmapnn0fiub.u	$⊢ U = ⋃_{f \in M} {supp}_{Z} (f)$
	fsuppmapnn0fiub.s	$⊢ S = sup (U ℝ <)$
Assertion	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})$

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	ex	$⊢ M \subseteq R^{ℕ_{0}} \to (f \in M \to dom f \subseteq ℕ_{0})$
16	15	3ad2ant1	$⊢ (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \to (f \in M \to dom f \subseteq ℕ_{0})$
17	16	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 \subseteq ℕ_{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) \to dom f \subseteq ℕ_{0}$
19	8 18	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 ℕ_{0}$
20	19	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})$
21	7 20	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}$
22		iunss	$⊢ ⋃_{f \in M} {supp}_{Z} (f) \subseteq ℕ_{0} \leftrightarrow \forall f \in M f supp Z \subseteq ℕ_{0}$
23	21 22	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)) \to ⋃_{f \in M} {supp}_{Z} (f) \subseteq ℕ_{0}$
24	1 23	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)) \to U \subseteq ℕ_{0}$
25		ltso	$⊢ < Or ℝ$
26	25	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)) \to < Or ℝ$
27		simp2	$⊢ (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \to M \in Fin$
28		id	$⊢ {finSupp}_{Z} (f) \to {finSupp}_{Z} (f)$
29	28	fsuppimpd	$⊢ {finSupp}_{Z} (f) \to f supp Z \in Fin$
30	29	ralimi	$⊢ \forall f \in M {finSupp}_{Z} (f) \to \forall f \in M f supp Z \in Fin$
31	30	adantr	$⊢ (\forall f \in M {finSupp}_{Z} (f) \land U \neq \emptyset) \to \forall f \in M f supp Z \in Fin$
32		iunfi	$⊢ (M \in Fin \land \forall f \in M f supp Z \in Fin) \to ⋃_{f \in M} {supp}_{Z} (f) \in Fin$
33	27 31 32	syl2an	$⊢ ((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} {supp}_{Z} (f) \in Fin$
34	1 33	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)) \to U \in Fin$
35		simprr	$⊢ ((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 U \neq \emptyset$
36	9 10 11	3syl	$⊢ (M \subseteq R^{ℕ_{0}} \land f \in M) \to dom f = ℕ_{0}$
37	36	ex	$⊢ M \subseteq R^{ℕ_{0}} \to (f \in M \to dom f = ℕ_{0})$
38	37	3ad2ant1	$⊢ (M \subseteq R^{ℕ_{0}} \land M \in Fin \land Z \in V) \to (f \in M \to dom f = ℕ_{0})$
39	38	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})$
40	39	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}$
41		nn0ssre	$⊢ ℕ_{0} \subseteq ℝ$
42	40 41	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 ℝ$
43	8 42	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 ℝ$
44	43	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 ℝ)$
45	7 44	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 ℝ$
46	1	sseq1i	$⊢ U \subseteq ℝ \leftrightarrow ⋃_{f \in M} {supp}_{Z} (f) \subseteq ℝ$
47		iunss	$⊢ ⋃_{f \in M} {supp}_{Z} (f) \subseteq ℝ \leftrightarrow \forall f \in M f supp Z \subseteq ℝ$
48	46 47	bitri	$⊢ U \subseteq ℝ \leftrightarrow \forall f \in M f supp Z \subseteq ℝ$
49	45 48	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)) \to U \subseteq ℝ$
50		fisupcl	$⊢ (< Or ℝ \land (U \in Fin \land U \neq \emptyset \land U \subseteq ℝ)) \to sup (U ℝ <) \in U$
51	2 50	eqeltrid	$⊢ (< Or ℝ \land (U \in Fin \land U \neq \emptyset \land U \subseteq ℝ)) \to S \in U$
52	26 34 35 49 51	syl13anc	$⊢ ((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 U$
53	24 52	sseldd	$⊢ ((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}$
54	53	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 S \in ℕ_{0})$

Metamath Proof Explorer

Theorem fsuppmapnn0fiublem

Proof