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