sge0iunmptlemre - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > sge0iunmptlemre		Structured version Visualization version GIF version

Theorem sge0iunmptlemre 46512

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

**Hypotheses**
Ref	Expression
sge0iunmptlemre.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
sge0iunmptlemre.b	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)
sge0iunmptlemre.dj	⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)
sge0iunmptlemre.c	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
sge0iunmptlemre.re	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ)
sge0iunmptlemre.sxr	⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ∈ ℝ^*)
sge0iunmptlemre.ssxr	⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ∈ ℝ^*)
sge0iunmptlemre.f	⊢ (𝜑 → (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶):∪ 𝑥 ∈ 𝐴 𝐵⟶(0[,]+∞))
sge0iunmptlemre.iue	⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)

**Assertion**
Ref	Expression
sge0iunmptlemre	⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))

Distinct variable groups: 𝐴,𝑘,𝑥 𝐵,𝑘 𝑥,𝐶 𝑥,𝑊 𝜑,𝑘,𝑥 Allowed substitution hints: 𝐵(𝑥) 𝐶(𝑘) 𝑉(𝑥,𝑘) 𝑊(𝑘)

Proof of Theorem sge0iunmptlemre Dummy variables 𝑏 𝑝 𝑦 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sge0iunmptlemre.sxr	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ∈ ℝ^*)
2		sge0iunmptlemre.ssxr	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ∈ ℝ^*)
3		elpwinss 45145	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
4	3	resmptd 5988	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → ((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦) = (𝑘 ∈ 𝑦 ↦ 𝐶))
5	4	fveq2d 6826	. . . . . . . 8 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → (Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) = (Σ^{^}‘(𝑘 ∈ 𝑦 ↦ 𝐶)))
6	5	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) = (Σ^{^}‘(𝑘 ∈ 𝑦 ↦ 𝐶)))
7		elinel2 4149	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → 𝑦 ∈ Fin)
8	7	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → 𝑦 ∈ Fin)
9	3	sselda 3929	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
10		eliun 4943	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
11	9, 10	sylib 218	. . . . . . . . . 10 ⊢ ((𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) ∧ 𝑘 ∈ 𝑦) → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
12	11	adantll 714	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
13		nfv 1915	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝜑
14		nfcv 2894	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥𝑦
15		nfiu1 4975	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
16	15	nfpw 4566	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥𝒫 ∪ 𝑥 ∈ 𝐴 𝐵
17		nfcv 2894	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥Fin
18	16, 17	nfin 4171	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)
19	14, 18	nfel 2909	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)
20	13, 19	nfan 1900	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin))
21		nfv 1915	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑘 ∈ 𝑦
22	20, 21	nfan 1900	. . . . . . . . . 10 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) ∧ 𝑘 ∈ 𝑦)
23		nfv 1915	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝐶 ∈ (0[,)+∞)
24		simp3 1138	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝑘 ∈ 𝐵)
25		sge0iunmptlemre.c	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
26		eqid 2731	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ 𝐵 ↦ 𝐶)
27	26	fvmpt2 6940	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ 𝐵 ∧ 𝐶 ∈ (0[,]+∞)) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘) = 𝐶)
28	24, 25, 27	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘) = 𝐶)
29	28	eqcomd 2737	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘))
30	25	3expa 1118	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
31	30, 26	fmptd 7047	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞))
32	31	3adant3 1132	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞))
33		sge0iunmptlemre.b	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)
34	33	3adant3 1132	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐵 ∈ 𝑊)
35		sge0iunmptlemre.re	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ)
36	35	3adant3 1132	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ)
37	34, 32, 36	sge0rern 46485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → ¬ +∞ ∈ ran (𝑘 ∈ 𝐵 ↦ 𝐶))
38	32, 37	fge0iccico 46467	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,)+∞))
39	38, 24	ffvelcdmd 7018	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘) ∈ (0[,)+∞))
40	29, 39	eqeltrd 2831	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,)+∞))
41	40	3exp 1119	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,)+∞))))
42	41	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (𝑥 ∈ 𝐴 → (𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,)+∞))))
43	22, 23, 42	rexlimd 3239	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,)+∞)))
44	12, 43	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝐶 ∈ (0[,)+∞))
45	8, 44	sge0fsummpt 46487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑦 ↦ 𝐶)) = Σ𝑘 ∈ 𝑦 𝐶)
46		sseqin2 4170	. . . . . . . . . . . . . 14 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦) = 𝑦)
47	46	biimpi 216	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦) = 𝑦)
48	47	eqcomd 2737	. . . . . . . . . . . 12 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦))
49		iunin1 5018	. . . . . . . . . . . . 13 ⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦) = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦)
50	49	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦) = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦))
51	48, 50	eqtr4d 2769	. . . . . . . . . . 11 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 = ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦))
52	3, 51	syl 17	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → 𝑦 = ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦))
53	52	sumeq1d 15607	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → Σ𝑘 ∈ 𝑦 𝐶 = Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦)𝐶)
54	53	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → Σ𝑘 ∈ 𝑦 𝐶 = Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦)𝐶)
55		simpl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → 𝜑)
56	33	adantlr 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)
57		sge0iunmptlemre.dj	. . . . . . . . . . 11 ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)
58	57	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → Disj 𝑥 ∈ 𝐴 𝐵)
59		rge0ssre 13356	. . . . . . . . . . . . 13 ⊢ (0[,)+∞) ⊆ ℝ
60		ax-resscn 11063	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
61	59, 60	sstri 3939	. . . . . . . . . . . 12 ⊢ (0[,)+∞) ⊆ ℂ
62	61, 40	sselid 3927	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
63	62	3adant1r 1178	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
64		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → 𝑦 ∈ Fin)
65	56, 58, 63, 64	fsumiunss 45674	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦)𝐶 = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
66	55, 8, 65	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦)𝐶 = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
67	54, 66	eqtrd 2766	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → Σ𝑘 ∈ 𝑦 𝐶 = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
68	6, 45, 67	3eqtrd 2770	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
69	56, 58, 64	disjinfi 45288	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ∈ Fin)
70		id 22	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ Fin → 𝑦 ∈ Fin)
71		inss2 4185	. . . . . . . . . . . . . 14 ⊢ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ⊆ 𝑦
72	71	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ Fin → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ⊆ 𝑦)
73		ssfi 9082	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ Fin ∧ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ⊆ 𝑦) → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ∈ Fin)
74	70, 72, 73	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ Fin → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ∈ Fin)
75	74	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ∈ Fin)
76		simpll 766	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝜑)
77		elrabi 3638	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} → 𝑤 ∈ 𝐴)
78	77	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝑤 ∈ 𝐴)
79		elinel1 4148	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) → 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵)
80	79	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵)
81		nfv 1915	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑤 ∈ 𝐴
82		nfcv 2894	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥𝑘
83		nfcsb1v 3869	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝐵
84	82, 83	nfel 2909	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵
85	13, 81, 84	nf3an 1902	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵)
86	85, 23	nfim 1897	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,)+∞))
87		eleq1w 2814	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))
88		csbeq1a 3859	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑤 → 𝐵 = ⦋𝑤 / 𝑥⦌𝐵)
89	88	eleq2d 2817	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (𝑘 ∈ 𝐵 ↔ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵))
90	87, 89	3anbi23d 1441	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) ↔ (𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵)))
91	90	imbi1d 341	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,)+∞)) ↔ ((𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,)+∞))))
92	86, 91, 40	chvarfv 2243	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,)+∞))
93	76, 78, 80, 92	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,)+∞))
94	93	adantllr 719	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,)+∞))
95	75, 94	fsumge0cl 45672	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) → Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶 ∈ (0[,)+∞))
96	69, 95	sge0fsummpt 46487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)) = Σ𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)
97		inss2 4185	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∩ 𝑦) ⊆ 𝑦
98	97	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ Fin → (𝐵 ∩ 𝑦) ⊆ 𝑦)
99		ssfi 9082	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ Fin ∧ (𝐵 ∩ 𝑦) ⊆ 𝑦) → (𝐵 ∩ 𝑦) ∈ Fin)
100	70, 98, 99	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ Fin → (𝐵 ∩ 𝑦) ∈ Fin)
101	100	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) → (𝐵 ∩ 𝑦) ∈ Fin)
102		simpll 766	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵 ∩ 𝑦)) → 𝜑)
103		rabid 3416	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↔ (𝑥 ∈ 𝐴 ∧ (𝐵 ∩ 𝑦) ≠ ∅))
104	103	biimpi 216	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} → (𝑥 ∈ 𝐴 ∧ (𝐵 ∩ 𝑦) ≠ ∅))
105	104	simpld 494	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} → 𝑥 ∈ 𝐴)
106	105	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵 ∩ 𝑦)) → 𝑥 ∈ 𝐴)
107		elinel1 4148	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (𝐵 ∩ 𝑦) → 𝑘 ∈ 𝐵)
108	107	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵 ∩ 𝑦)) → 𝑘 ∈ 𝐵)
109	102, 106, 108, 40	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,)+∞))
110	109	adantllr 719	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,)+∞))
111	101, 110	sge0fsummpt 46487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) → (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)) = Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
112	111	mpteq2dva 5182	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶))
113		nfrab1 3415	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}
114		nfcv 2894	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}
115		nfcv 2894	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶
116	83, 14	nfin 4171	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)
117		nfcv 2894	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥𝐶
118	116, 117	nfsum 15598	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶
119	88	ineq1d 4166	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → (𝐵 ∩ 𝑦) = (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦))
120	119	sumeq1d 15607	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶 = Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)
121	113, 114, 115, 118, 120	cbvmptf 5189	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶) = (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)
122	121	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶) = (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶))
123	112, 122	eqtr2d 2767	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶) = (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))))
124	123	fveq2d 6826	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)) = (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))))
125	124	eqcomd 2737	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) = (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)))
126	120, 115, 118	cbvsum 15602	. . . . . . . . . 10 ⊢ Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶 = Σ𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶
127	126	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶 = Σ𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)
128	96, 125, 127	3eqtr4d 2776	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
129	55, 8, 128	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
130	129	eqcomd 2737	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶 = (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))))
131	68, 130	eqtrd 2766	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) = (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))))
132		sge0iunmptlemre.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
133	77	ssriv 3933	. . . . . . . . . 10 ⊢ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ⊆ 𝐴
134	133	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ⊆ 𝐴)
135	132, 134	ssexd 5260	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ∈ V)
136		vex 3440	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
137	136	inex2 5254	. . . . . . . . . . . 12 ⊢ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ∈ V
138	137	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ∈ V)
139		icossicc 13336	. . . . . . . . . . . . 13 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
140		simpll 766	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝜑)
141		simplr 768	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝑤 ∈ 𝐴)
142	79	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵)
143	140, 141, 142, 92	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,)+∞))
144	139, 143	sselid 3927	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,]+∞))
145		eqid 2731	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶) = (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)
146	144, 145	fmptd 7047	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶):(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)⟶(0[,]+∞))
147	138, 146	sge0cl 46478	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
148	77, 147	sylan2 593	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) → (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
149		nfcv 2894	. . . . . . . . . 10 ⊢ Ⅎ𝑤(Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))
150		nfcv 2894	. . . . . . . . . . 11 ⊢ Ⅎ𝑥Σ^{^}
151	116, 117	nfmpt 5187	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)
152	150, 151	nffv 6832	. . . . . . . . . 10 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))
153	119	mpteq1d 5179	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → (𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶) = (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))
154	153	fveq2d 6826	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))
155	113, 114, 149, 152, 154	cbvmptf 5189	. . . . . . . . 9 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))
156	148, 155	fmptd 7047	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))):{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}⟶(0[,]+∞))
157	135, 156	sge0xrcl 46482	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ∈ ℝ^*)
158	157	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ∈ ℝ^*)
159		eqid 2731	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))
160	147, 159	fmptd 7047	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))):𝐴⟶(0[,]+∞))
161	132, 160	sge0xrcl 46482	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ∈ ℝ^*)
162	161	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ∈ ℝ^*)
163	55, 2	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ∈ ℝ^*)
164	155	fveq2i 6825	. . . . . . . . 9 ⊢ (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) = (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))))
165	164	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) = (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))))
166	132, 147, 134	sge0lessmpt 46496	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))))
167	165, 166	eqbrtrd 5111	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))))
168	167	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))))
169	149, 152, 154	cbvmpt 5191	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))
170	169	eqcomi 2740	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))
171	170	fveq2i 6825	. . . . . . . . 9 ⊢ (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))))
172	171	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))))
173	136	inex2 5254	. . . . . . . . . . 11 ⊢ (𝐵 ∩ 𝑦) ∈ V
174	173	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ∩ 𝑦) ∈ V)
175	107, 30	sylan2 593	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ (𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,]+∞))
176		eqid 2731	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶) = (𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)
177	175, 176	fmptd 7047	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶):(𝐵 ∩ 𝑦)⟶(0[,]+∞))
178	174, 177	sge0cl 46478	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
179	33, 31	sge0cl 46478	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ (0[,]+∞))
180		inss1 4184	. . . . . . . . . . 11 ⊢ (𝐵 ∩ 𝑦) ⊆ 𝐵
181	180	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ∩ 𝑦) ⊆ 𝐵)
182	33, 30, 181	sge0lessmpt 46496	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)) ≤ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
183	13, 132, 178, 179, 182	sge0lempt 46507	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
184	172, 183	eqbrtrd 5111	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
185	184	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
186	158, 162, 163, 168, 185	xrletrd 13061	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
187	131, 186	eqbrtrd 5111	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
188	187	ralrimiva 3124	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)(Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
189		sge0iunmptlemre.iue	. . . 4 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
190		sge0iunmptlemre.f	. . . 4 ⊢ (𝜑 → (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶):∪ 𝑥 ∈ 𝐴 𝐵⟶(0[,]+∞))
191	189, 190, 2	sge0lefi 46495	. . 3 ⊢ (𝜑 → ((Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ↔ ∀𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)(Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))))
192	188, 191	mpbird 257	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
193		elpwinss 45145	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴)
194	193	resmptd 5988	. . . . . . . 8 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → ((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦) = (𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
195	194	fveq2d 6826	. . . . . . 7 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → (Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) = (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
196	195	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) = (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
197		elinel2 4149	. . . . . . . 8 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin)
198	197	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ∈ Fin)
199		0xr 11159	. . . . . . . . 9 ⊢ 0 ∈ ℝ^*
200	199	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 0 ∈ ℝ^*)
201		pnfxr 11166	. . . . . . . . 9 ⊢ +∞ ∈ ℝ^*
202	201	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → +∞ ∈ ℝ^*)
203		simpll 766	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 𝜑)
204	193	sselda 3929	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴)
205	204	adantll 714	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴)
206	203, 205, 33	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 𝐵 ∈ 𝑊)
207	203, 205, 31	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞))
208	206, 207	sge0xrcl 46482	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ^*)
209	206, 207	sge0ge0 46481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 0 ≤ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
210	203, 205, 35	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ)
211		ltpnf 13019	. . . . . . . . 9 ⊢ ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) < +∞)
212	210, 211	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) < +∞)
213	200, 202, 208, 209, 212	elicod 13295	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ (0[,)+∞))
214	198, 213	sge0fsummpt 46487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
215	196, 214	eqtrd 2766	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) = Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
216		nfv 1915	. . . . . 6 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
217	189	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
218	190	fvmptelcdm 7046	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
219	218	adantlr 715	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
220	198, 210	fsumrecl 15641	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ)
221	220	rexrd 11162	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ^*)
222		nfv 1915	. . . . . . . 8 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺)
223		iunss1 4954	. . . . . . . . . . . 12 ⊢ (𝑦 ⊆ 𝐴 → ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
224	193, 223	syl 17	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
225	224	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
226	217, 225	ssexd 5260	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)
227	226	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)
228		simpll 766	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵) → 𝜑)
229	225	sselda 3929	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵) → 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
230	228, 229, 218	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵) → 𝐶 ∈ (0[,]+∞))
231	230	adantlr 715	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵) → 𝐶 ∈ (0[,]+∞))
232		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → 𝑝 ∈ ℝ⁺)
233	193	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ⊆ 𝐴)
234	57	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Disj 𝑥 ∈ 𝐴 𝐵)
235		disjss1 5062	. . . . . . . . . . . 12 ⊢ (𝑦 ⊆ 𝐴 → (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑥 ∈ 𝑦 𝐵))
236	233, 234, 235	sylc 65	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Disj 𝑥 ∈ 𝑦 𝐵)
237	203	3adant3 1132	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦 ∧ 𝑘 ∈ 𝐵) → 𝜑)
238	205	3adant3 1132	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦 ∧ 𝑘 ∈ 𝐵) → 𝑥 ∈ 𝐴)
239		simp3 1138	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦 ∧ 𝑘 ∈ 𝐵) → 𝑘 ∈ 𝐵)
240	237, 238, 239, 25	syl3anc 1373	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
241	198, 206, 236, 240, 210	sge0iunmptlemfi 46510	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
242	214, 220	eqeltrd 2831	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ∈ ℝ)
243	241, 242	eqeltrd 2831	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) ∈ ℝ)
244	243	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) ∈ ℝ)
245	222, 227, 231, 232, 244	sge0ltfirpmpt 46505	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)(Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝))
246		nfv 1915	. . . . . . . 8 ⊢ Ⅎ𝑏((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺)
247		nfre1 3257	. . . . . . . 8 ⊢ Ⅎ𝑏∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝)
248	223	sspwd 4560	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊆ 𝐴 → 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵)
249	193, 248	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵)
250	249	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵)
251		elinel1 4148	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) → 𝑏 ∈ 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵)
252	251	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵)
253	250, 252	sseldd 3930	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵)
254		elinel2 4149	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) → 𝑏 ∈ Fin)
255	254	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ Fin)
256	253, 255	elind 4147	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin))
257	256	ad4ant24 754	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin))
258	257	3adant3 1132	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin))
259	221	ad2antrr 726	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ^*)
260	259	3adant3 1132	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ^*)
261		nfv 1915	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin))
262	226	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)
263	230	adantlr 715	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵) → 𝐶 ∈ (0[,]+∞))
264	243	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) ∈ ℝ)
265	251	elpwid 4556	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) → 𝑏 ⊆ ∪ 𝑥 ∈ 𝑦 𝐵)
266	265	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ⊆ ∪ 𝑥 ∈ 𝑦 𝐵)
267	261, 262, 263, 264, 266	sge0ssrempt 46502	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) ∈ ℝ)
268	267	rexrd 11162	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) ∈ ℝ^*)
269	268	adantlr 715	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) ∈ ℝ^*)
270		rpxr 12900	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ℝ⁺ → 𝑝 ∈ ℝ^*)
271	270	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑝 ∈ ℝ^*)
272	269, 271	xaddcld 13200	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝) ∈ ℝ^*)
273	272	3adant3 1132	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝) ∈ ℝ^*)
274		simp3 1138	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝))
275	241, 214	eqtr2d 2767	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)))
276	275	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)))
277	276	3ad2ant1 1133	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)))
278	267	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) ∈ ℝ)
279		rpre 12899	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ∈ ℝ⁺ → 𝑝 ∈ ℝ)
280	279	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑝 ∈ ℝ)
281		rexadd 13131	. . . . . . . . . . . . . . 15 ⊢ (((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) ∈ ℝ ∧ 𝑝 ∈ ℝ) → ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝) = ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝))
282	278, 280, 281	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝) = ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝))
283	282	3adant3 1132	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝) = ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝))
284	277, 283	breq12d 5102	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → (Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝) ↔ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)))
285	274, 284	mpbird 257	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝))
286	260, 273, 285	xrltled 13049	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝))
287		rspe 3222	. . . . . . . . . 10 ⊢ ((𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) ∧ Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝)) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝))
288	258, 286, 287	syl2anc 584	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝))
289	288	3exp 1119	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → (𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) → ((Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝))))
290	246, 247, 289	rexlimd 3239	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → (∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)(Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝)))
291	245, 290	mpd 15	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝))
292	216, 217, 219, 221, 291	sge0gerpmpt 46499	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
293	215, 292	eqbrtrd 5111	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
294	293	ralrimiva 3124	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
295		eqid 2731	. . . . 5 ⊢ (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
296	179, 295	fmptd 7047	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞))
297	132, 296, 1	sge0lefi 46495	. . 3 ⊢ (𝜑 → ((Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ↔ ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶))))
298	294, 297	mpbird 257	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
299	1, 2, 192, 298	xrletrid 13054	1 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2111 ≠ wne 2928 ∀wral 3047 ∃wrex 3056 {crab 3395 Vcvv 3436 ⦋csb 3845 ∩ cin 3896 ⊆ wss 3897 ∅c0 4280 𝒫 cpw 4547 ∪ ciun 4939 Disj wdisj 5056 class class class wbr 5089 ↦ cmpt 5170 ↾ cres 5616 ⟶wf 6477 ‘cfv 6481 (class class class)co 7346 Fincfn 8869 ℂcc 11004 ℝcr 11005 0cc0 11006 + caddc 11009 +∞cpnf 11143 ℝ^*cxr 11145 < clt 11146 ≤ cle 11147 ℝ⁺crp 12890 +_𝑒 cxad 13009 [,)cico 13247 [,]cicc 13248 Σcsu 15593 Σ^{^}csumge0 46459

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-inf2 9531 ax-ac2 10354 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083 ax-pre-sup 11084

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-int 4896 df-iun 4941 df-disj 5057 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-se 5568 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-isom 6490 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-er 8622 df-map 8752 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-sup 9326 df-oi 9396 df-card 9832 df-acn 9835 df-ac 10007 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-div 11775 df-nn 12126 df-2 12188 df-3 12189 df-n0 12382 df-z 12469 df-uz 12733 df-rp 12891 df-xadd 13012 df-ico 13251 df-icc 13252 df-fz 13408 df-fzo 13555 df-seq 13909 df-exp 13969 df-hash 14238 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-clim 15395 df-sum 15594 df-sumge0 46460

This theorem is referenced by: sge0iunmpt 46515

W3C validator