sge0iunmptlemre

Description: Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0iunmptlemre.a	$⊢ φ \to A \in V$
	sge0iunmptlemre.b	$⊢ (φ \land x \in A) \to B \in W$
	sge0iunmptlemre.dj	$⊢ φ \to \underset{x \in A}{Disj} B$
	sge0iunmptlemre.c	$⊢ (φ \land x \in A \land k \in B) \to C \in [0, +∞]$
	sge0iunmptlemre.re	$⊢ (φ \land x \in A) \to sum^((k \in B ⟼ C)) \in ℝ$
	sge0iunmptlemre.sxr	$⊢ φ \to sum^((k \in ⋃_{x \in A} B ⟼ C)) \in ℝ^{*}$
	sge0iunmptlemre.ssxr	$⊢ φ \to sum^((x \in A ⟼ sum^((k \in B ⟼ C)))) \in ℝ^{*}$
	sge0iunmptlemre.f	$⊢ φ \to (k \in ⋃_{x \in A} B ⟼ C) : ⋃_{x \in A} B ⟶ [0, +∞]$
	sge0iunmptlemre.iue	$⊢ φ \to ⋃_{x \in A} B \in V$
Assertion	sge0iunmptlemre	$⊢ φ \to sum^((k \in ⋃_{x \in A} B ⟼ C)) = sum^((x \in A ⟼ sum^((k \in B ⟼ C))))$

Proof

Step	Hyp	Ref	Expression
1		sge0iunmptlemre.a	$⊢ φ \to A \in V$
2		sge0iunmptlemre.b	$⊢ (φ \land x \in A) \to B \in W$
3		sge0iunmptlemre.dj	$⊢ φ \to \underset{x \in A}{Disj} B$
4		sge0iunmptlemre.c	$⊢ (φ \land x \in A \land k \in B) \to C \in [0, +∞]$
5		sge0iunmptlemre.re	$⊢ (φ \land x \in A) \to sum^((k \in B ⟼ C)) \in ℝ$
6		sge0iunmptlemre.sxr	$⊢ φ \to sum^((k \in ⋃_{x \in A} B ⟼ C)) \in ℝ^{*}$
7		sge0iunmptlemre.ssxr	$⊢ φ \to sum^((x \in A ⟼ sum^((k \in B ⟼ C)))) \in ℝ^{*}$
8		sge0iunmptlemre.f	$⊢ φ \to (k \in ⋃_{x \in A} B ⟼ C) : ⋃_{x \in A} B ⟶ [0, +∞]$
9		sge0iunmptlemre.iue	$⊢ φ \to ⋃_{x \in A} B \in V$
10		elpwinss	$⊢ y \in (𝒫 ⋃_{x \in A} B \cap Fin) \to y \subseteq ⋃_{x \in A} B$
11	10	resmptd	$⊢ y \in (𝒫 ⋃_{x \in A} B \cap Fin) \to {(k \in ⋃_{x \in A} B ⟼ C) ↾}_{y} = (k \in y ⟼ C)$
12	11	fveq2d	$⊢ y \in (𝒫 ⋃_{x \in A} B \cap Fin) \to sum^({(k \in ⋃_{x \in A} B ⟼ C) ↾}_{y}) = sum^((k \in y ⟼ C))$
13	12	adantl	$⊢ (φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin)) \to sum^({(k \in ⋃_{x \in A} B ⟼ C) ↾}_{y}) = sum^((k \in y ⟼ C))$
14		elinel2	$⊢ y \in (𝒫 ⋃_{x \in A} B \cap Fin) \to y \in Fin$
15	14	adantl	$⊢ (φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin)) \to y \in Fin$
16	10	sselda	$⊢ (y \in (𝒫 ⋃_{x \in A} B \cap Fin) \land k \in y) \to k \in ⋃_{x \in A} B$
17		eliun	$⊢ k \in ⋃_{x \in A} B \leftrightarrow \exists x \in A k \in B$
18	16 17	sylib	$⊢ (y \in (𝒫 ⋃_{x \in A} B \cap Fin) \land k \in y) \to \exists x \in A k \in B$
19	18	adantll	$⊢ ((φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin)) \land k \in y) \to \exists x \in A k \in B$
20		nfv	$⊢ Ⅎ x φ$
21		nfcv	$⊢ \underline{Ⅎ} x y$
22		nfiu1	$⊢ \underline{Ⅎ} x ⋃_{x \in A} B$
23	22	nfpw	$⊢ \underline{Ⅎ} x 𝒫 ⋃_{x \in A} B$
24		nfcv	$⊢ \underline{Ⅎ} x Fin$
25	23 24	nfin	$⊢ \underline{Ⅎ} x (𝒫 ⋃_{x \in A} B \cap Fin)$
26	21 25	nfel	$⊢ Ⅎ x y \in (𝒫 ⋃_{x \in A} B \cap Fin)$
27	20 26	nfan	$⊢ Ⅎ x (φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin))$
28		nfv	$⊢ Ⅎ x k \in y$
29	27 28	nfan	$⊢ Ⅎ x ((φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin)) \land k \in y)$
30		nfv	$⊢ Ⅎ x C \in [0, +∞)$
31		simp3	$⊢ (φ \land x \in A \land k \in B) \to k \in B$
32		eqid	$⊢ (k \in B ⟼ C) = (k \in B ⟼ C)$
33	32	fvmpt2	$⊢ (k \in B \land C \in [0, +∞]) \to (k \in B ⟼ C) (k) = C$
34	31 4 33	syl2anc	$⊢ (φ \land x \in A \land k \in B) \to (k \in B ⟼ C) (k) = C$
35	34	eqcomd	$⊢ (φ \land x \in A \land k \in B) \to C = (k \in B ⟼ C) (k)$
36	4	3expa	$⊢ ((φ \land x \in A) \land k \in B) \to C \in [0, +∞]$
37	36 32	fmptd	$⊢ (φ \land x \in A) \to (k \in B ⟼ C) : B ⟶ [0, +∞]$
38	37	3adant3	$⊢ (φ \land x \in A \land k \in B) \to (k \in B ⟼ C) : B ⟶ [0, +∞]$
39	2	3adant3	$⊢ (φ \land x \in A \land k \in B) \to B \in W$
40	5	3adant3	$⊢ (φ \land x \in A \land k \in B) \to sum^((k \in B ⟼ C)) \in ℝ$
41	39 38 40	sge0rern	$⊢ (φ \land x \in A \land k \in B) \to \neg +∞ \in ran (k \in B ⟼ C)$
42	38 41	fge0iccico	$⊢ (φ \land x \in A \land k \in B) \to (k \in B ⟼ C) : B ⟶ [0, +∞)$
43	42 31	ffvelcdmd	$⊢ (φ \land x \in A \land k \in B) \to (k \in B ⟼ C) (k) \in [0, +∞)$
44	35 43	eqeltrd	$⊢ (φ \land x \in A \land k \in B) \to C \in [0, +∞)$
45	44	3exp	$⊢ φ \to (x \in A \to (k \in B \to C \in [0, +∞)))$
46	45	ad2antrr	$⊢ ((φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin)) \land k \in y) \to (x \in A \to (k \in B \to C \in [0, +∞)))$
47	29 30 46	rexlimd	$⊢ ((φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin)) \land k \in y) \to (\exists x \in A k \in B \to C \in [0, +∞))$
48	19 47	mpd	$⊢ ((φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin)) \land k \in y) \to C \in [0, +∞)$
49	15 48	sge0fsummpt	$⊢ (φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin)) \to sum^((k \in y ⟼ C)) = \sum_{k \in y} C$
50		sseqin2	$⊢ y \subseteq ⋃_{x \in A} B \leftrightarrow ⋃_{x \in A} B \cap y = y$
51	50	biimpi	$⊢ y \subseteq ⋃_{x \in A} B \to ⋃_{x \in A} B \cap y = y$
52	51	eqcomd	$⊢ y \subseteq ⋃_{x \in A} B \to y = ⋃_{x \in A} B \cap y$
53		iunin1	$⊢ ⋃_{x \in A} (B \cap y) = ⋃_{x \in A} B \cap y$
54	53	a1i	$⊢ y \subseteq ⋃_{x \in A} B \to ⋃_{x \in A} (B \cap y) = ⋃_{x \in A} B \cap y$
55	52 54	eqtr4d	$⊢ y \subseteq ⋃_{x \in A} B \to y = ⋃_{x \in A} (B \cap y)$
56	10 55	syl	$⊢ y \in (𝒫 ⋃_{x \in A} B \cap Fin) \to y = ⋃_{x \in A} (B \cap y)$
57	56	sumeq1d	$⊢ y \in (𝒫 ⋃_{x \in A} B \cap Fin) \to \sum_{k \in y} C = \sum_{k \in ⋃_{x \in A} (B \cap y)} C$
58	57	adantl	$⊢ (φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin)) \to \sum_{k \in y} C = \sum_{k \in ⋃_{x \in A} (B \cap y)} C$
59		simpl	$⊢ (φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin)) \to φ$
60	2	adantlr	$⊢ ((φ \land y \in Fin) \land x \in A) \to B \in W$
61	3	adantr	$⊢ (φ \land y \in Fin) \to \underset{x \in A}{Disj} B$
62		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
63		ax-resscn	$⊢ ℝ \subseteq ℂ$
64	62 63	sstri	$⊢ [0, +∞) \subseteq ℂ$
65	64 44	sselid	$⊢ (φ \land x \in A \land k \in B) \to C \in ℂ$
66	65	3adant1r	$⊢ ((φ \land y \in Fin) \land x \in A \land k \in B) \to C \in ℂ$
67		simpr	$⊢ (φ \land y \in Fin) \to y \in Fin$
68	60 61 66 67	fsumiunss	$⊢ (φ \land y \in Fin) \to \sum_{k \in ⋃_{x \in A} (B \cap y)} C = \sum_{x \in \{x \in A \| B \cap y \neq \emptyset\}} \sum_{k \in B \cap y} C$
69	59 15 68	syl2anc	$⊢ (φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin)) \to \sum_{k \in ⋃_{x \in A} (B \cap y)} C = \sum_{x \in \{x \in A \| B \cap y \neq \emptyset\}} \sum_{k \in B \cap y} C$
70	58 69	eqtrd	$⊢ (φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin)) \to \sum_{k \in y} C = \sum_{x \in \{x \in A \| B \cap y \neq \emptyset\}} \sum_{k \in B \cap y} C$
71	13 49 70	3eqtrd	$⊢ (φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin)) \to sum^({(k \in ⋃_{x \in A} B ⟼ C) ↾}_{y}) = \sum_{x \in \{x \in A \| B \cap y \neq \emptyset\}} \sum_{k \in B \cap y} C$
72	60 61 67	disjinfi	$⊢ (φ \land y \in Fin) \to \{x \in A \| B \cap y \neq \emptyset\} \in Fin$
73		id	$⊢ y \in Fin \to y \in Fin$
74		inss2	$⊢ ⦋ w / x ⦌ B \cap y \subseteq y$
75	74	a1i	$⊢ y \in Fin \to ⦋ w / x ⦌ B \cap y \subseteq y$
76		ssfi	$⊢ (y \in Fin \land ⦋ w / x ⦌ B \cap y \subseteq y) \to ⦋ w / x ⦌ B \cap y \in Fin$
77	73 75 76	syl2anc	$⊢ y \in Fin \to ⦋ w / x ⦌ B \cap y \in Fin$
78	77	ad2antlr	$⊢ ((φ \land y \in Fin) \land w \in \{x \in A \| B \cap y \neq \emptyset\}) \to ⦋ w / x ⦌ B \cap y \in Fin$
79		simpll	$⊢ ((φ \land w \in \{x \in A \| B \cap y \neq \emptyset\}) \land k \in (⦋ w / x ⦌ B \cap y)) \to φ$
80		elrabi	$⊢ w \in \{x \in A \| B \cap y \neq \emptyset\} \to w \in A$
81	80	ad2antlr	$⊢ ((φ \land w \in \{x \in A \| B \cap y \neq \emptyset\}) \land k \in (⦋ w / x ⦌ B \cap y)) \to w \in A$
82		elinel1	$⊢ k \in (⦋ w / x ⦌ B \cap y) \to k \in ⦋ w / x ⦌ B$
83	82	adantl	$⊢ ((φ \land w \in \{x \in A \| B \cap y \neq \emptyset\}) \land k \in (⦋ w / x ⦌ B \cap y)) \to k \in ⦋ w / x ⦌ B$
84		nfv	$⊢ Ⅎ x w \in A$
85		nfcv	$⊢ \underline{Ⅎ} x k$
86		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ w / x ⦌ B$
87	85 86	nfel	$⊢ Ⅎ x k \in ⦋ w / x ⦌ B$
88	20 84 87	nf3an	$⊢ Ⅎ x (φ \land w \in A \land k \in ⦋ w / x ⦌ B)$
89	88 30	nfim	$⊢ Ⅎ x ((φ \land w \in A \land k \in ⦋ w / x ⦌ B) \to C \in [0, +∞))$
90		eleq1w	$⊢ x = w \to (x \in A \leftrightarrow w \in A)$
91		csbeq1a	$⊢ x = w \to B = ⦋ w / x ⦌ B$
92	91	eleq2d	$⊢ x = w \to (k \in B \leftrightarrow k \in ⦋ w / x ⦌ B)$
93	90 92	3anbi23d	$⊢ x = w \to ((φ \land x \in A \land k \in B) \leftrightarrow (φ \land w \in A \land k \in ⦋ w / x ⦌ B))$
94	93	imbi1d	$⊢ x = w \to (((φ \land x \in A \land k \in B) \to C \in [0, +∞)) \leftrightarrow ((φ \land w \in A \land k \in ⦋ w / x ⦌ B) \to C \in [0, +∞)))$
95	89 94 44	chvarfv	$⊢ (φ \land w \in A \land k \in ⦋ w / x ⦌ B) \to C \in [0, +∞)$
96	79 81 83 95	syl3anc	$⊢ ((φ \land w \in \{x \in A \| B \cap y \neq \emptyset\}) \land k \in (⦋ w / x ⦌ B \cap y)) \to C \in [0, +∞)$
97	96	adantllr	$⊢ (((φ \land y \in Fin) \land w \in \{x \in A \| B \cap y \neq \emptyset\}) \land k \in (⦋ w / x ⦌ B \cap y)) \to C \in [0, +∞)$
98	78 97	fsumge0cl	$⊢ ((φ \land y \in Fin) \land w \in \{x \in A \| B \cap y \neq \emptyset\}) \to \sum_{k \in ⦋ w / x ⦌ B \cap y} C \in [0, +∞)$
99	72 98	sge0fsummpt	$⊢ (φ \land y \in Fin) \to sum^((w \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ \sum_{k \in ⦋ w / x ⦌ B \cap y} C)) = \sum_{w \in \{x \in A \| B \cap y \neq \emptyset\}} \sum_{k \in ⦋ w / x ⦌ B \cap y} C$
100		inss2	$⊢ B \cap y \subseteq y$
101	100	a1i	$⊢ y \in Fin \to B \cap y \subseteq y$
102		ssfi	$⊢ (y \in Fin \land B \cap y \subseteq y) \to B \cap y \in Fin$
103	73 101 102	syl2anc	$⊢ y \in Fin \to B \cap y \in Fin$
104	103	ad2antlr	$⊢ ((φ \land y \in Fin) \land x \in \{x \in A \| B \cap y \neq \emptyset\}) \to B \cap y \in Fin$
105		simpll	$⊢ ((φ \land x \in \{x \in A \| B \cap y \neq \emptyset\}) \land k \in (B \cap y)) \to φ$
106		rabid	$⊢ x \in \{x \in A \| B \cap y \neq \emptyset\} \leftrightarrow (x \in A \land B \cap y \neq \emptyset)$
107	106	biimpi	$⊢ x \in \{x \in A \| B \cap y \neq \emptyset\} \to (x \in A \land B \cap y \neq \emptyset)$
108	107	simpld	$⊢ x \in \{x \in A \| B \cap y \neq \emptyset\} \to x \in A$
109	108	ad2antlr	$⊢ ((φ \land x \in \{x \in A \| B \cap y \neq \emptyset\}) \land k \in (B \cap y)) \to x \in A$
110		elinel1	$⊢ k \in (B \cap y) \to k \in B$
111	110	adantl	$⊢ ((φ \land x \in \{x \in A \| B \cap y \neq \emptyset\}) \land k \in (B \cap y)) \to k \in B$
112	105 109 111 44	syl3anc	$⊢ ((φ \land x \in \{x \in A \| B \cap y \neq \emptyset\}) \land k \in (B \cap y)) \to C \in [0, +∞)$
113	112	adantllr	$⊢ (((φ \land y \in Fin) \land x \in \{x \in A \| B \cap y \neq \emptyset\}) \land k \in (B \cap y)) \to C \in [0, +∞)$
114	104 113	sge0fsummpt	$⊢ ((φ \land y \in Fin) \land x \in \{x \in A \| B \cap y \neq \emptyset\}) \to sum^((k \in (B \cap y) ⟼ C)) = \sum_{k \in B \cap y} C$
115	114	mpteq2dva	$⊢ (φ \land y \in Fin) \to (x \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ sum^((k \in (B \cap y) ⟼ C))) = (x \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ \sum_{k \in B \cap y} C)$
116		nfrab1	$⊢ \underline{Ⅎ} x \{x \in A \| B \cap y \neq \emptyset\}$
117		nfcv	$⊢ \underline{Ⅎ} w \{x \in A \| B \cap y \neq \emptyset\}$
118		nfcv	$⊢ \underline{Ⅎ} w \sum_{k \in B \cap y} C$
119	86 21	nfin	$⊢ \underline{Ⅎ} x (⦋ w / x ⦌ B \cap y)$
120		nfcv	$⊢ \underline{Ⅎ} x C$
121	119 120	nfsum	$⊢ \underline{Ⅎ} x \sum_{k \in ⦋ w / x ⦌ B \cap y} C$
122	91	ineq1d	$⊢ x = w \to B \cap y = ⦋ w / x ⦌ B \cap y$
123	122	sumeq1d	$⊢ x = w \to \sum_{k \in B \cap y} C = \sum_{k \in ⦋ w / x ⦌ B \cap y} C$
124	116 117 118 121 123	cbvmptf	$⊢ (x \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ \sum_{k \in B \cap y} C) = (w \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ \sum_{k \in ⦋ w / x ⦌ B \cap y} C)$
125	124	a1i	$⊢ (φ \land y \in Fin) \to (x \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ \sum_{k \in B \cap y} C) = (w \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ \sum_{k \in ⦋ w / x ⦌ B \cap y} C)$
126	115 125	eqtr2d	$⊢ (φ \land y \in Fin) \to (w \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ \sum_{k \in ⦋ w / x ⦌ B \cap y} C) = (x \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ sum^((k \in (B \cap y) ⟼ C)))$
127	126	fveq2d	$⊢ (φ \land y \in Fin) \to sum^((w \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ \sum_{k \in ⦋ w / x ⦌ B \cap y} C)) = sum^((x \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ sum^((k \in (B \cap y) ⟼ C))))$
128	127	eqcomd	$⊢ (φ \land y \in Fin) \to sum^((x \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ sum^((k \in (B \cap y) ⟼ C)))) = sum^((w \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ \sum_{k \in ⦋ w / x ⦌ B \cap y} C))$
129	123 117 116 118 121	cbvsum	$⊢ \sum_{x \in \{x \in A \| B \cap y \neq \emptyset\}} \sum_{k \in B \cap y} C = \sum_{w \in \{x \in A \| B \cap y \neq \emptyset\}} \sum_{k \in ⦋ w / x ⦌ B \cap y} C$
130	129	a1i	$⊢ (φ \land y \in Fin) \to \sum_{x \in \{x \in A \| B \cap y \neq \emptyset\}} \sum_{k \in B \cap y} C = \sum_{w \in \{x \in A \| B \cap y \neq \emptyset\}} \sum_{k \in ⦋ w / x ⦌ B \cap y} C$
131	99 128 130	3eqtr4d	$⊢ (φ \land y \in Fin) \to sum^((x \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ sum^((k \in (B \cap y) ⟼ C)))) = \sum_{x \in \{x \in A \| B \cap y \neq \emptyset\}} \sum_{k \in B \cap y} C$
132	59 15 131	syl2anc	$⊢ (φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin)) \to sum^((x \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ sum^((k \in (B \cap y) ⟼ C)))) = \sum_{x \in \{x \in A \| B \cap y \neq \emptyset\}} \sum_{k \in B \cap y} C$
133	132	eqcomd	$⊢ (φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin)) \to \sum_{x \in \{x \in A \| B \cap y \neq \emptyset\}} \sum_{k \in B \cap y} C = sum^((x \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ sum^((k \in (B \cap y) ⟼ C))))$
134	71 133	eqtrd	$⊢ (φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin)) \to sum^({(k \in ⋃_{x \in A} B ⟼ C) ↾}_{y}) = sum^((x \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ sum^((k \in (B \cap y) ⟼ C))))$
135	80	ssriv	$⊢ \{x \in A \| B \cap y \neq \emptyset\} \subseteq A$
136	135	a1i	$⊢ φ \to \{x \in A \| B \cap y \neq \emptyset\} \subseteq A$
137	1 136	ssexd	$⊢ φ \to \{x \in A \| B \cap y \neq \emptyset\} \in V$
138		vex	$⊢ y \in V$
139	138	inex2	$⊢ ⦋ w / x ⦌ B \cap y \in V$
140	139	a1i	$⊢ (φ \land w \in A) \to ⦋ w / x ⦌ B \cap y \in V$
141		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
142		simpll	$⊢ ((φ \land w \in A) \land k \in (⦋ w / x ⦌ B \cap y)) \to φ$
143		simplr	$⊢ ((φ \land w \in A) \land k \in (⦋ w / x ⦌ B \cap y)) \to w \in A$
144	82	adantl	$⊢ ((φ \land w \in A) \land k \in (⦋ w / x ⦌ B \cap y)) \to k \in ⦋ w / x ⦌ B$
145	142 143 144 95	syl3anc	$⊢ ((φ \land w \in A) \land k \in (⦋ w / x ⦌ B \cap y)) \to C \in [0, +∞)$
146	141 145	sselid	$⊢ ((φ \land w \in A) \land k \in (⦋ w / x ⦌ B \cap y)) \to C \in [0, +∞]$
147		eqid	$⊢ (k \in (⦋ w / x ⦌ B \cap y) ⟼ C) = (k \in (⦋ w / x ⦌ B \cap y) ⟼ C)$
148	146 147	fmptd	$⊢ (φ \land w \in A) \to (k \in (⦋ w / x ⦌ B \cap y) ⟼ C) : ⦋ w / x ⦌ B \cap y ⟶ [0, +∞]$
149	140 148	sge0cl	$⊢ (φ \land w \in A) \to sum^((k \in (⦋ w / x ⦌ B \cap y) ⟼ C)) \in [0, +∞]$
150	80 149	sylan2	$⊢ (φ \land w \in \{x \in A \| B \cap y \neq \emptyset\}) \to sum^((k \in (⦋ w / x ⦌ B \cap y) ⟼ C)) \in [0, +∞]$
151		nfcv	$⊢ \underline{Ⅎ} w sum^((k \in (B \cap y) ⟼ C))$
152		nfcv	$⊢ \underline{Ⅎ} x sum^$
153	119 120	nfmpt	$⊢ \underline{Ⅎ} x (k \in (⦋ w / x ⦌ B \cap y) ⟼ C)$
154	152 153	nffv	$⊢ \underline{Ⅎ} x sum^((k \in (⦋ w / x ⦌ B \cap y) ⟼ C))$
155	122	mpteq1d	$⊢ x = w \to (k \in (B \cap y) ⟼ C) = (k \in (⦋ w / x ⦌ B \cap y) ⟼ C)$
156	155	fveq2d	$⊢ x = w \to sum^((k \in (B \cap y) ⟼ C)) = sum^((k \in (⦋ w / x ⦌ B \cap y) ⟼ C))$
157	116 117 151 154 156	cbvmptf	$⊢ (x \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ sum^((k \in (B \cap y) ⟼ C))) = (w \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ sum^((k \in (⦋ w / x ⦌ B \cap y) ⟼ C)))$
158	150 157	fmptd	$⊢ φ \to (x \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ sum^((k \in (B \cap y) ⟼ C))) : \{x \in A \| B \cap y \neq \emptyset\} ⟶ [0, +∞]$
159	137 158	sge0xrcl	$⊢ φ \to sum^((x \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ sum^((k \in (B \cap y) ⟼ C)))) \in ℝ^{*}$
160	159	adantr	$⊢ (φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin)) \to sum^((x \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ sum^((k \in (B \cap y) ⟼ C)))) \in ℝ^{*}$
161		eqid	$⊢ (w \in A ⟼ sum^((k \in (⦋ w / x ⦌ B \cap y) ⟼ C))) = (w \in A ⟼ sum^((k \in (⦋ w / x ⦌ B \cap y) ⟼ C)))$
162	149 161	fmptd	$⊢ φ \to (w \in A ⟼ sum^((k \in (⦋ w / x ⦌ B \cap y) ⟼ C))) : A ⟶ [0, +∞]$
163	1 162	sge0xrcl	$⊢ φ \to sum^((w \in A ⟼ sum^((k \in (⦋ w / x ⦌ B \cap y) ⟼ C)))) \in ℝ^{*}$
164	163	adantr	$⊢ (φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin)) \to sum^((w \in A ⟼ sum^((k \in (⦋ w / x ⦌ B \cap y) ⟼ C)))) \in ℝ^{*}$
165	59 7	syl	$⊢ (φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin)) \to sum^((x \in A ⟼ sum^((k \in B ⟼ C)))) \in ℝ^{*}$
166	157	fveq2i	$⊢ sum^((x \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ sum^((k \in (B \cap y) ⟼ C)))) = sum^((w \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ sum^((k \in (⦋ w / x ⦌ B \cap y) ⟼ C))))$
167	166	a1i	$⊢ φ \to sum^((x \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ sum^((k \in (B \cap y) ⟼ C)))) = sum^((w \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ sum^((k \in (⦋ w / x ⦌ B \cap y) ⟼ C))))$
168	1 149 136	sge0lessmpt	$⊢ φ \to sum^((w \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ sum^((k \in (⦋ w / x ⦌ B \cap y) ⟼ C)))) \leq sum^((w \in A ⟼ sum^((k \in (⦋ w / x ⦌ B \cap y) ⟼ C))))$
169	167 168	eqbrtrd	$⊢ φ \to sum^((x \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ sum^((k \in (B \cap y) ⟼ C)))) \leq sum^((w \in A ⟼ sum^((k \in (⦋ w / x ⦌ B \cap y) ⟼ C))))$
170	169	adantr	$⊢ (φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin)) \to sum^((x \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ sum^((k \in (B \cap y) ⟼ C)))) \leq sum^((w \in A ⟼ sum^((k \in (⦋ w / x ⦌ B \cap y) ⟼ C))))$
171	151 154 156	cbvmpt	$⊢ (x \in A ⟼ sum^((k \in (B \cap y) ⟼ C))) = (w \in A ⟼ sum^((k \in (⦋ w / x ⦌ B \cap y) ⟼ C)))$
172	171	eqcomi	$⊢ (w \in A ⟼ sum^((k \in (⦋ w / x ⦌ B \cap y) ⟼ C))) = (x \in A ⟼ sum^((k \in (B \cap y) ⟼ C)))$
173	172	fveq2i	$⊢ sum^((w \in A ⟼ sum^((k \in (⦋ w / x ⦌ B \cap y) ⟼ C)))) = sum^((x \in A ⟼ sum^((k \in (B \cap y) ⟼ C))))$
174	173	a1i	$⊢ φ \to sum^((w \in A ⟼ sum^((k \in (⦋ w / x ⦌ B \cap y) ⟼ C)))) = sum^((x \in A ⟼ sum^((k \in (B \cap y) ⟼ C))))$
175	138	inex2	$⊢ B \cap y \in V$
176	175	a1i	$⊢ (φ \land x \in A) \to B \cap y \in V$
177	110 36	sylan2	$⊢ ((φ \land x \in A) \land k \in (B \cap y)) \to C \in [0, +∞]$
178		eqid	$⊢ (k \in (B \cap y) ⟼ C) = (k \in (B \cap y) ⟼ C)$
179	177 178	fmptd	$⊢ (φ \land x \in A) \to (k \in (B \cap y) ⟼ C) : B \cap y ⟶ [0, +∞]$
180	176 179	sge0cl	$⊢ (φ \land x \in A) \to sum^((k \in (B \cap y) ⟼ C)) \in [0, +∞]$
181	2 37	sge0cl	$⊢ (φ \land x \in A) \to sum^((k \in B ⟼ C)) \in [0, +∞]$
182		inss1	$⊢ B \cap y \subseteq B$
183	182	a1i	$⊢ (φ \land x \in A) \to B \cap y \subseteq B$
184	2 36 183	sge0lessmpt	$⊢ (φ \land x \in A) \to sum^((k \in (B \cap y) ⟼ C)) \leq sum^((k \in B ⟼ C))$
185	20 1 180 181 184	sge0lempt	$⊢ φ \to sum^((x \in A ⟼ sum^((k \in (B \cap y) ⟼ C)))) \leq sum^((x \in A ⟼ sum^((k \in B ⟼ C))))$
186	174 185	eqbrtrd	$⊢ φ \to sum^((w \in A ⟼ sum^((k \in (⦋ w / x ⦌ B \cap y) ⟼ C)))) \leq sum^((x \in A ⟼ sum^((k \in B ⟼ C))))$
187	186	adantr	$⊢ (φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin)) \to sum^((w \in A ⟼ sum^((k \in (⦋ w / x ⦌ B \cap y) ⟼ C)))) \leq sum^((x \in A ⟼ sum^((k \in B ⟼ C))))$
188	160 164 165 170 187	xrletrd	$⊢ (φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin)) \to sum^((x \in \{x \in A \| B \cap y \neq \emptyset\} ⟼ sum^((k \in (B \cap y) ⟼ C)))) \leq sum^((x \in A ⟼ sum^((k \in B ⟼ C))))$
189	134 188	eqbrtrd	$⊢ (φ \land y \in (𝒫 ⋃_{x \in A} B \cap Fin)) \to sum^({(k \in ⋃_{x \in A} B ⟼ C) ↾}_{y}) \leq sum^((x \in A ⟼ sum^((k \in B ⟼ C))))$
190	189	ralrimiva	$⊢ φ \to \forall y \in (𝒫 ⋃_{x \in A} B \cap Fin) sum^({(k \in ⋃_{x \in A} B ⟼ C) ↾}_{y}) \leq sum^((x \in A ⟼ sum^((k \in B ⟼ C))))$
191	9 8 7	sge0lefi	$⊢ φ \to (sum^((k \in ⋃_{x \in A} B ⟼ C)) \leq sum^((x \in A ⟼ sum^((k \in B ⟼ C)))) \leftrightarrow \forall y \in (𝒫 ⋃_{x \in A} B \cap Fin) sum^({(k \in ⋃_{x \in A} B ⟼ C) ↾}_{y}) \leq sum^((x \in A ⟼ sum^((k \in B ⟼ C)))))$
192	190 191	mpbird	$⊢ φ \to sum^((k \in ⋃_{x \in A} B ⟼ C)) \leq sum^((x \in A ⟼ sum^((k \in B ⟼ C))))$
193		elpwinss	$⊢ y \in (𝒫 A \cap Fin) \to y \subseteq A$
194	193	resmptd	$⊢ y \in (𝒫 A \cap Fin) \to {(x \in A ⟼ sum^((k \in B ⟼ C))) ↾}_{y} = (x \in y ⟼ sum^((k \in B ⟼ C)))$
195	194	fveq2d	$⊢ y \in (𝒫 A \cap Fin) \to sum^({(x \in A ⟼ sum^((k \in B ⟼ C))) ↾}_{y}) = sum^((x \in y ⟼ sum^((k \in B ⟼ C))))$
196	195	adantl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to sum^({(x \in A ⟼ sum^((k \in B ⟼ C))) ↾}_{y}) = sum^((x \in y ⟼ sum^((k \in B ⟼ C))))$
197		elinel2	$⊢ y \in (𝒫 A \cap Fin) \to y \in Fin$
198	197	adantl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to y \in Fin$
199		0xr	$⊢ 0 \in ℝ^{*}$
200	199	a1i	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y) \to 0 \in ℝ^{*}$
201		pnfxr	$⊢ +∞ \in ℝ^{*}$
202	201	a1i	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y) \to +∞ \in ℝ^{*}$
203		simpll	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y) \to φ$
204	193	sselda	$⊢ (y \in (𝒫 A \cap Fin) \land x \in y) \to x \in A$
205	204	adantll	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y) \to x \in A$
206	203 205 2	syl2anc	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y) \to B \in W$
207	203 205 37	syl2anc	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y) \to (k \in B ⟼ C) : B ⟶ [0, +∞]$
208	206 207	sge0xrcl	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y) \to sum^((k \in B ⟼ C)) \in ℝ^{*}$
209	206 207	sge0ge0	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y) \to 0 \leq sum^((k \in B ⟼ C))$
210	203 205 5	syl2anc	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y) \to sum^((k \in B ⟼ C)) \in ℝ$
211		ltpnf	$⊢ sum^((k \in B ⟼ C)) \in ℝ \to sum^((k \in B ⟼ C)) < +∞$
212	210 211	syl	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y) \to sum^((k \in B ⟼ C)) < +∞$
213	200 202 208 209 212	elicod	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y) \to sum^((k \in B ⟼ C)) \in [0, +∞)$
214	198 213	sge0fsummpt	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to sum^((x \in y ⟼ sum^((k \in B ⟼ C)))) = \sum_{x \in y} sum^((k \in B ⟼ C))$
215	196 214	eqtrd	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to sum^({(x \in A ⟼ sum^((k \in B ⟼ C))) ↾}_{y}) = \sum_{x \in y} sum^((k \in B ⟼ C))$
216		nfv	$⊢ Ⅎ k (φ \land y \in (𝒫 A \cap Fin))$
217	9	adantr	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to ⋃_{x \in A} B \in V$
218	8	fvmptelcdm	$⊢ (φ \land k \in ⋃_{x \in A} B) \to C \in [0, +∞]$
219	218	adantlr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land k \in ⋃_{x \in A} B) \to C \in [0, +∞]$
220	198 210	fsumrecl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \sum_{x \in y} sum^((k \in B ⟼ C)) \in ℝ$
221	220	rexrd	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \sum_{x \in y} sum^((k \in B ⟼ C)) \in ℝ^{*}$
222		nfv	$⊢ Ⅎ k ((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+})$
223		iunss1	$⊢ y \subseteq A \to ⋃_{x \in y} B \subseteq ⋃_{x \in A} B$
224	193 223	syl	$⊢ y \in (𝒫 A \cap Fin) \to ⋃_{x \in y} B \subseteq ⋃_{x \in A} B$
225	224	adantl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to ⋃_{x \in y} B \subseteq ⋃_{x \in A} B$
226	217 225	ssexd	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to ⋃_{x \in y} B \in V$
227	226	adantr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \to ⋃_{x \in y} B \in V$
228		simpll	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land k \in ⋃_{x \in y} B) \to φ$
229	225	sselda	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land k \in ⋃_{x \in y} B) \to k \in ⋃_{x \in A} B$
230	228 229 218	syl2anc	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land k \in ⋃_{x \in y} B) \to C \in [0, +∞]$
231	230	adantlr	$⊢ (((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \land k \in ⋃_{x \in y} B) \to C \in [0, +∞]$
232		simpr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \to p \in ℝ^{+}$
233	193	adantl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to y \subseteq A$
234	3	adantr	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \underset{x \in A}{Disj} B$
235		disjss1	$⊢ y \subseteq A \to (\underset{x \in A}{Disj} B \to \underset{x \in y}{Disj} B)$
236	233 234 235	sylc	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \underset{x \in y}{Disj} B$
237	203	3adant3	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y \land k \in B) \to φ$
238	205	3adant3	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y \land k \in B) \to x \in A$
239		simp3	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y \land k \in B) \to k \in B$
240	237 238 239 4	syl3anc	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y \land k \in B) \to C \in [0, +∞]$
241	198 206 236 240 210	sge0iunmptlemfi	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to sum^((k \in ⋃_{x \in y} B ⟼ C)) = sum^((x \in y ⟼ sum^((k \in B ⟼ C))))$
242	214 220	eqeltrd	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to sum^((x \in y ⟼ sum^((k \in B ⟼ C)))) \in ℝ$
243	241 242	eqeltrd	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to sum^((k \in ⋃_{x \in y} B ⟼ C)) \in ℝ$
244	243	adantr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \to sum^((k \in ⋃_{x \in y} B ⟼ C)) \in ℝ$
245	222 227 231 232 244	sge0ltfirpmpt	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \to \exists b \in (𝒫 ⋃_{x \in y} B \cap Fin) sum^((k \in ⋃_{x \in y} B ⟼ C)) < sum^((k \in b ⟼ C)) + p$
246		nfv	$⊢ Ⅎ b ((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+})$
247		nfre1	$⊢ Ⅎ b \exists b \in (𝒫 ⋃_{x \in A} B \cap Fin) \sum_{x \in y} sum^((k \in B ⟼ C)) \leq sum^((k \in b ⟼ C)) +_{𝑒} p$
248	223	sspwd	$⊢ y \subseteq A \to 𝒫 ⋃_{x \in y} B \subseteq 𝒫 ⋃_{x \in A} B$
249	193 248	syl	$⊢ y \in (𝒫 A \cap Fin) \to 𝒫 ⋃_{x \in y} B \subseteq 𝒫 ⋃_{x \in A} B$
250	249	adantr	$⊢ (y \in (𝒫 A \cap Fin) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin)) \to 𝒫 ⋃_{x \in y} B \subseteq 𝒫 ⋃_{x \in A} B$
251		elinel1	$⊢ b \in (𝒫 ⋃_{x \in y} B \cap Fin) \to b \in 𝒫 ⋃_{x \in y} B$
252	251	adantl	$⊢ (y \in (𝒫 A \cap Fin) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin)) \to b \in 𝒫 ⋃_{x \in y} B$
253	250 252	sseldd	$⊢ (y \in (𝒫 A \cap Fin) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin)) \to b \in 𝒫 ⋃_{x \in A} B$
254		elinel2	$⊢ b \in (𝒫 ⋃_{x \in y} B \cap Fin) \to b \in Fin$
255	254	adantl	$⊢ (y \in (𝒫 A \cap Fin) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin)) \to b \in Fin$
256	253 255	elind	$⊢ (y \in (𝒫 A \cap Fin) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin)) \to b \in (𝒫 ⋃_{x \in A} B \cap Fin)$
257	256	ad4ant24	$⊢ (((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin)) \to b \in (𝒫 ⋃_{x \in A} B \cap Fin)$
258	257	3adant3	$⊢ (((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin) \land sum^((k \in ⋃_{x \in y} B ⟼ C)) < sum^((k \in b ⟼ C)) + p) \to b \in (𝒫 ⋃_{x \in A} B \cap Fin)$
259	221	ad2antrr	$⊢ (((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin)) \to \sum_{x \in y} sum^((k \in B ⟼ C)) \in ℝ^{*}$
260	259	3adant3	$⊢ (((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin) \land sum^((k \in ⋃_{x \in y} B ⟼ C)) < sum^((k \in b ⟼ C)) + p) \to \sum_{x \in y} sum^((k \in B ⟼ C)) \in ℝ^{*}$
261		nfv	$⊢ Ⅎ k ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin))$
262	226	adantr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin)) \to ⋃_{x \in y} B \in V$
263	230	adantlr	$⊢ (((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin)) \land k \in ⋃_{x \in y} B) \to C \in [0, +∞]$
264	243	adantr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin)) \to sum^((k \in ⋃_{x \in y} B ⟼ C)) \in ℝ$
265	251	elpwid	$⊢ b \in (𝒫 ⋃_{x \in y} B \cap Fin) \to b \subseteq ⋃_{x \in y} B$
266	265	adantl	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin)) \to b \subseteq ⋃_{x \in y} B$
267	261 262 263 264 266	sge0ssrempt	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin)) \to sum^((k \in b ⟼ C)) \in ℝ$
268	267	rexrd	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin)) \to sum^((k \in b ⟼ C)) \in ℝ^{*}$
269	268	adantlr	$⊢ (((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin)) \to sum^((k \in b ⟼ C)) \in ℝ^{*}$
270		rpxr	$⊢ p \in ℝ^{+} \to p \in ℝ^{*}$
271	270	ad2antlr	$⊢ (((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin)) \to p \in ℝ^{*}$
272	269 271	xaddcld	$⊢ (((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin)) \to sum^((k \in b ⟼ C)) +_{𝑒} p \in ℝ^{*}$
273	272	3adant3	$⊢ (((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin) \land sum^((k \in ⋃_{x \in y} B ⟼ C)) < sum^((k \in b ⟼ C)) + p) \to sum^((k \in b ⟼ C)) +_{𝑒} p \in ℝ^{*}$
274		simp3	$⊢ (((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin) \land sum^((k \in ⋃_{x \in y} B ⟼ C)) < sum^((k \in b ⟼ C)) + p) \to sum^((k \in ⋃_{x \in y} B ⟼ C)) < sum^((k \in b ⟼ C)) + p$
275	241 214	eqtr2d	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \sum_{x \in y} sum^((k \in B ⟼ C)) = sum^((k \in ⋃_{x \in y} B ⟼ C))$
276	275	adantr	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \to \sum_{x \in y} sum^((k \in B ⟼ C)) = sum^((k \in ⋃_{x \in y} B ⟼ C))$
277	276	3ad2ant1	$⊢ (((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin) \land sum^((k \in ⋃_{x \in y} B ⟼ C)) < sum^((k \in b ⟼ C)) + p) \to \sum_{x \in y} sum^((k \in B ⟼ C)) = sum^((k \in ⋃_{x \in y} B ⟼ C))$
278	267	adantlr	$⊢ (((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin)) \to sum^((k \in b ⟼ C)) \in ℝ$
279		rpre	$⊢ p \in ℝ^{+} \to p \in ℝ$
280	279	ad2antlr	$⊢ (((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin)) \to p \in ℝ$
281		rexadd	$⊢ (sum^((k \in b ⟼ C)) \in ℝ \land p \in ℝ) \to sum^((k \in b ⟼ C)) +_{𝑒} p = sum^((k \in b ⟼ C)) + p$
282	278 280 281	syl2anc	$⊢ (((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin)) \to sum^((k \in b ⟼ C)) +_{𝑒} p = sum^((k \in b ⟼ C)) + p$
283	282	3adant3	$⊢ (((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin) \land sum^((k \in ⋃_{x \in y} B ⟼ C)) < sum^((k \in b ⟼ C)) + p) \to sum^((k \in b ⟼ C)) +_{𝑒} p = sum^((k \in b ⟼ C)) + p$
284	277 283	breq12d	$⊢ (((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin) \land sum^((k \in ⋃_{x \in y} B ⟼ C)) < sum^((k \in b ⟼ C)) + p) \to (\sum_{x \in y} sum^((k \in B ⟼ C)) < sum^((k \in b ⟼ C)) +_{𝑒} p \leftrightarrow sum^((k \in ⋃_{x \in y} B ⟼ C)) < sum^((k \in b ⟼ C)) + p)$
285	274 284	mpbird	$⊢ (((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin) \land sum^((k \in ⋃_{x \in y} B ⟼ C)) < sum^((k \in b ⟼ C)) + p) \to \sum_{x \in y} sum^((k \in B ⟼ C)) < sum^((k \in b ⟼ C)) +_{𝑒} p$
286	260 273 285	xrltled	$⊢ (((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin) \land sum^((k \in ⋃_{x \in y} B ⟼ C)) < sum^((k \in b ⟼ C)) + p) \to \sum_{x \in y} sum^((k \in B ⟼ C)) \leq sum^((k \in b ⟼ C)) +_{𝑒} p$
287		rspe	$⊢ (b \in (𝒫 ⋃_{x \in A} B \cap Fin) \land \sum_{x \in y} sum^((k \in B ⟼ C)) \leq sum^((k \in b ⟼ C)) +_{𝑒} p) \to \exists b \in (𝒫 ⋃_{x \in A} B \cap Fin) \sum_{x \in y} sum^((k \in B ⟼ C)) \leq sum^((k \in b ⟼ C)) +_{𝑒} p$
288	258 286 287	syl2anc	$⊢ (((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \land b \in (𝒫 ⋃_{x \in y} B \cap Fin) \land sum^((k \in ⋃_{x \in y} B ⟼ C)) < sum^((k \in b ⟼ C)) + p) \to \exists b \in (𝒫 ⋃_{x \in A} B \cap Fin) \sum_{x \in y} sum^((k \in B ⟼ C)) \leq sum^((k \in b ⟼ C)) +_{𝑒} p$
289	288	3exp	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \to (b \in (𝒫 ⋃_{x \in y} B \cap Fin) \to (sum^((k \in ⋃_{x \in y} B ⟼ C)) < sum^((k \in b ⟼ C)) + p \to \exists b \in (𝒫 ⋃_{x \in A} B \cap Fin) \sum_{x \in y} sum^((k \in B ⟼ C)) \leq sum^((k \in b ⟼ C)) +_{𝑒} p))$
290	246 247 289	rexlimd	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \to (\exists b \in (𝒫 ⋃_{x \in y} B \cap Fin) sum^((k \in ⋃_{x \in y} B ⟼ C)) < sum^((k \in b ⟼ C)) + p \to \exists b \in (𝒫 ⋃_{x \in A} B \cap Fin) \sum_{x \in y} sum^((k \in B ⟼ C)) \leq sum^((k \in b ⟼ C)) +_{𝑒} p)$
291	245 290	mpd	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land p \in ℝ^{+}) \to \exists b \in (𝒫 ⋃_{x \in A} B \cap Fin) \sum_{x \in y} sum^((k \in B ⟼ C)) \leq sum^((k \in b ⟼ C)) +_{𝑒} p$
292	216 217 219 221 291	sge0gerpmpt	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \sum_{x \in y} sum^((k \in B ⟼ C)) \leq sum^((k \in ⋃_{x \in A} B ⟼ C))$
293	215 292	eqbrtrd	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to sum^({(x \in A ⟼ sum^((k \in B ⟼ C))) ↾}_{y}) \leq sum^((k \in ⋃_{x \in A} B ⟼ C))$
294	293	ralrimiva	$⊢ φ \to \forall y \in (𝒫 A \cap Fin) sum^({(x \in A ⟼ sum^((k \in B ⟼ C))) ↾}_{y}) \leq sum^((k \in ⋃_{x \in A} B ⟼ C))$
295		eqid	$⊢ (x \in A ⟼ sum^((k \in B ⟼ C))) = (x \in A ⟼ sum^((k \in B ⟼ C)))$
296	181 295	fmptd	$⊢ φ \to (x \in A ⟼ sum^((k \in B ⟼ C))) : A ⟶ [0, +∞]$
297	1 296 6	sge0lefi	$⊢ φ \to (sum^((x \in A ⟼ sum^((k \in B ⟼ C)))) \leq sum^((k \in ⋃_{x \in A} B ⟼ C)) \leftrightarrow \forall y \in (𝒫 A \cap Fin) sum^({(x \in A ⟼ sum^((k \in B ⟼ C))) ↾}_{y}) \leq sum^((k \in ⋃_{x \in A} B ⟼ C)))$
298	294 297	mpbird	$⊢ φ \to sum^((x \in A ⟼ sum^((k \in B ⟼ C)))) \leq sum^((k \in ⋃_{x \in A} B ⟼ C))$
299	6 7 192 298	xrletrid	$⊢ φ \to sum^((k \in ⋃_{x \in A} B ⟼ C)) = sum^((x \in A ⟼ sum^((k \in B ⟼ C))))$

Metamath Proof Explorer

Theorem sge0iunmptlemre

Proof