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 46420

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 45050	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
4	3	resmptd 6014	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → ((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦) = (𝑘 ∈ 𝑦 ↦ 𝐶))
5	4	fveq2d 6865	. . . . . . . 8 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → (Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) = (Σ^{^}‘(𝑘 ∈ 𝑦 ↦ 𝐶)))
6	5	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) = (Σ^{^}‘(𝑘 ∈ 𝑦 ↦ 𝐶)))
7		elinel2 4168	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → 𝑦 ∈ Fin)
8	7	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → 𝑦 ∈ Fin)
9	3	sselda 3949	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
10		eliun 4962	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
11	9, 10	sylib 218	. . . . . . . . . 10 ⊢ ((𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) ∧ 𝑘 ∈ 𝑦) → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
12	11	adantll 714	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
13		nfv 1914	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝜑
14		nfcv 2892	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥𝑦
15		nfiu1 4994	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
16	15	nfpw 4585	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥𝒫 ∪ 𝑥 ∈ 𝐴 𝐵
17		nfcv 2892	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥Fin
18	16, 17	nfin 4190	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)
19	14, 18	nfel 2907	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)
20	13, 19	nfan 1899	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin))
21		nfv 1914	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑘 ∈ 𝑦
22	20, 21	nfan 1899	. . . . . . . . . 10 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) ∧ 𝑘 ∈ 𝑦)
23		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝐶 ∈ (0[,)+∞)
24		simp3 1138	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝑘 ∈ 𝐵)
25		sge0iunmptlemre.c	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
26		eqid 2730	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ 𝐵 ↦ 𝐶)
27	26	fvmpt2 6982	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ 𝐵 ∧ 𝐶 ∈ (0[,]+∞)) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘) = 𝐶)
28	24, 25, 27	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘) = 𝐶)
29	28	eqcomd 2736	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘))
30	25	3expa 1118	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
31	30, 26	fmptd 7089	. . . . . . . . . . . . . . . 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 46393	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → ¬ +∞ ∈ ran (𝑘 ∈ 𝐵 ↦ 𝐶))
38	32, 37	fge0iccico 46375	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,)+∞))
39	38, 24	ffvelcdmd 7060	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘) ∈ (0[,)+∞))
40	29, 39	eqeltrd 2829	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,)+∞))
41	40	3exp 1119	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,)+∞))))
42	41	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (𝑥 ∈ 𝐴 → (𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,)+∞))))
43	22, 23, 42	rexlimd 3245	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,)+∞)))
44	12, 43	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝐶 ∈ (0[,)+∞))
45	8, 44	sge0fsummpt 46395	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑦 ↦ 𝐶)) = Σ𝑘 ∈ 𝑦 𝐶)
46		sseqin2 4189	. . . . . . . . . . . . . 14 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦) = 𝑦)
47	46	biimpi 216	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦) = 𝑦)
48	47	eqcomd 2736	. . . . . . . . . . . 12 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦))
49		iunin1 5039	. . . . . . . . . . . . 13 ⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦) = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦)
50	49	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦) = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦))
51	48, 50	eqtr4d 2768	. . . . . . . . . . 11 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 = ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦))
52	3, 51	syl 17	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → 𝑦 = ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦))
53	52	sumeq1d 15673	. . . . . . . . 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 13424	. . . . . . . . . . . . 13 ⊢ (0[,)+∞) ⊆ ℝ
60		ax-resscn 11132	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
61	59, 60	sstri 3959	. . . . . . . . . . . 12 ⊢ (0[,)+∞) ⊆ ℂ
62	61, 40	sselid 3947	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
63	62	3adant1r 1178	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
64		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → 𝑦 ∈ Fin)
65	56, 58, 63, 64	fsumiunss 45580	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦)𝐶 = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
66	55, 8, 65	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦)𝐶 = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
67	54, 66	eqtrd 2765	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → Σ𝑘 ∈ 𝑦 𝐶 = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
68	6, 45, 67	3eqtrd 2769	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
69	56, 58, 64	disjinfi 45193	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ∈ Fin)
70		id 22	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ Fin → 𝑦 ∈ Fin)
71		inss2 4204	. . . . . . . . . . . . . 14 ⊢ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ⊆ 𝑦
72	71	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ Fin → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ⊆ 𝑦)
73		ssfi 9143	. . . . . . . . . . . . 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 3657	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} → 𝑤 ∈ 𝐴)
78	77	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝑤 ∈ 𝐴)
79		elinel1 4167	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) → 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵)
80	79	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵)
81		nfv 1914	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑤 ∈ 𝐴
82		nfcv 2892	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥𝑘
83		nfcsb1v 3889	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝐵
84	82, 83	nfel 2907	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵
85	13, 81, 84	nf3an 1901	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵)
86	85, 23	nfim 1896	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,)+∞))
87		eleq1w 2812	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))
88		csbeq1a 3879	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑤 → 𝐵 = ⦋𝑤 / 𝑥⦌𝐵)
89	88	eleq2d 2815	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (𝑘 ∈ 𝐵 ↔ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵))
90	87, 89	3anbi23d 1441	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) ↔ (𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵)))
91	90	imbi1d 341	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,)+∞)) ↔ ((𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,)+∞))))
92	86, 91, 40	chvarfv 2241	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,)+∞))
93	76, 78, 80, 92	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,)+∞))
94	93	adantllr 719	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,)+∞))
95	75, 94	fsumge0cl 45578	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) → Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶 ∈ (0[,)+∞))
96	69, 95	sge0fsummpt 46395	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)) = Σ𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)
97		inss2 4204	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∩ 𝑦) ⊆ 𝑦
98	97	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ Fin → (𝐵 ∩ 𝑦) ⊆ 𝑦)
99		ssfi 9143	. . . . . . . . . . . . . . . 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 3430	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↔ (𝑥 ∈ 𝐴 ∧ (𝐵 ∩ 𝑦) ≠ ∅))
104	103	biimpi 216	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} → (𝑥 ∈ 𝐴 ∧ (𝐵 ∩ 𝑦) ≠ ∅))
105	104	simpld 494	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} → 𝑥 ∈ 𝐴)
106	105	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵 ∩ 𝑦)) → 𝑥 ∈ 𝐴)
107		elinel1 4167	. . . . . . . . . . . . . . . . 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 46395	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) → (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)) = Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
112	111	mpteq2dva 5203	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶))
113		nfrab1 3429	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}
114		nfcv 2892	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}
115		nfcv 2892	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶
116	83, 14	nfin 4190	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)
117		nfcv 2892	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥𝐶
118	116, 117	nfsum 15664	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶
119	88	ineq1d 4185	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → (𝐵 ∩ 𝑦) = (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦))
120	119	sumeq1d 15673	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶 = Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)
121	113, 114, 115, 118, 120	cbvmptf 5210	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶) = (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)
122	121	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶) = (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶))
123	112, 122	eqtr2d 2766	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶) = (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))))
124	123	fveq2d 6865	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)) = (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))))
125	124	eqcomd 2736	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) = (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)))
126	120, 115, 118	cbvsum 15668	. . . . . . . . . 10 ⊢ Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶 = Σ𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶
127	126	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶 = Σ𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)
128	96, 125, 127	3eqtr4d 2775	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
129	55, 8, 128	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
130	129	eqcomd 2736	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶 = (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))))
131	68, 130	eqtrd 2765	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) = (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))))
132		sge0iunmptlemre.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
133	77	ssriv 3953	. . . . . . . . . 10 ⊢ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ⊆ 𝐴
134	133	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ⊆ 𝐴)
135	132, 134	ssexd 5282	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ∈ V)
136		vex 3454	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
137	136	inex2 5276	. . . . . . . . . . . 12 ⊢ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ∈ V
138	137	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ∈ V)
139		icossicc 13404	. . . . . . . . . . . . 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 3947	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,]+∞))
145		eqid 2730	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶) = (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)
146	144, 145	fmptd 7089	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶):(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)⟶(0[,]+∞))
147	138, 146	sge0cl 46386	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
148	77, 147	sylan2 593	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) → (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
149		nfcv 2892	. . . . . . . . . 10 ⊢ Ⅎ𝑤(Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))
150		nfcv 2892	. . . . . . . . . . 11 ⊢ Ⅎ𝑥Σ^{^}
151	116, 117	nfmpt 5208	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)
152	150, 151	nffv 6871	. . . . . . . . . 10 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))
153	119	mpteq1d 5200	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → (𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶) = (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))
154	153	fveq2d 6865	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))
155	113, 114, 149, 152, 154	cbvmptf 5210	. . . . . . . . 9 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))
156	148, 155	fmptd 7089	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))):{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}⟶(0[,]+∞))
157	135, 156	sge0xrcl 46390	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ∈ ℝ^*)
158	157	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ∈ ℝ^*)
159		eqid 2730	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))
160	147, 159	fmptd 7089	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))):𝐴⟶(0[,]+∞))
161	132, 160	sge0xrcl 46390	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ∈ ℝ^*)
162	161	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ∈ ℝ^*)
163	55, 2	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ∈ ℝ^*)
164	155	fveq2i 6864	. . . . . . . . 9 ⊢ (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) = (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))))
165	164	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) = (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))))
166	132, 147, 134	sge0lessmpt 46404	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))))
167	165, 166	eqbrtrd 5132	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))))
168	167	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))))
169	149, 152, 154	cbvmpt 5212	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))
170	169	eqcomi 2739	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))
171	170	fveq2i 6864	. . . . . . . . 9 ⊢ (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))))
172	171	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))))
173	136	inex2 5276	. . . . . . . . . . 11 ⊢ (𝐵 ∩ 𝑦) ∈ V
174	173	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ∩ 𝑦) ∈ V)
175	107, 30	sylan2 593	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ (𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,]+∞))
176		eqid 2730	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶) = (𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)
177	175, 176	fmptd 7089	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶):(𝐵 ∩ 𝑦)⟶(0[,]+∞))
178	174, 177	sge0cl 46386	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
179	33, 31	sge0cl 46386	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ (0[,]+∞))
180		inss1 4203	. . . . . . . . . . 11 ⊢ (𝐵 ∩ 𝑦) ⊆ 𝐵
181	180	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ∩ 𝑦) ⊆ 𝐵)
182	33, 30, 181	sge0lessmpt 46404	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)) ≤ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
183	13, 132, 178, 179, 182	sge0lempt 46415	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
184	172, 183	eqbrtrd 5132	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
185	184	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
186	158, 162, 163, 168, 185	xrletrd 13129	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
187	131, 186	eqbrtrd 5132	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
188	187	ralrimiva 3126	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)(Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
189		sge0iunmptlemre.iue	. . . 4 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
190		sge0iunmptlemre.f	. . . 4 ⊢ (𝜑 → (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶):∪ 𝑥 ∈ 𝐴 𝐵⟶(0[,]+∞))
191	189, 190, 2	sge0lefi 46403	. . 3 ⊢ (𝜑 → ((Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ↔ ∀𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)(Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))))
192	188, 191	mpbird 257	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
193		elpwinss 45050	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴)
194	193	resmptd 6014	. . . . . . . 8 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → ((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦) = (𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
195	194	fveq2d 6865	. . . . . . 7 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → (Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) = (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
196	195	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) = (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
197		elinel2 4168	. . . . . . . 8 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin)
198	197	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ∈ Fin)
199		0xr 11228	. . . . . . . . 9 ⊢ 0 ∈ ℝ^*
200	199	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 0 ∈ ℝ^*)
201		pnfxr 11235	. . . . . . . . 9 ⊢ +∞ ∈ ℝ^*
202	201	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → +∞ ∈ ℝ^*)
203		simpll 766	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 𝜑)
204	193	sselda 3949	. . . . . . . . . . 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 46390	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ^*)
209	206, 207	sge0ge0 46389	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 0 ≤ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
210	203, 205, 35	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ)
211		ltpnf 13087	. . . . . . . . 9 ⊢ ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) < +∞)
212	210, 211	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) < +∞)
213	200, 202, 208, 209, 212	elicod 13363	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ (0[,)+∞))
214	198, 213	sge0fsummpt 46395	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
215	196, 214	eqtrd 2765	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) = Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
216		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
217	189	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
218	190	fvmptelcdm 7088	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
219	218	adantlr 715	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
220	198, 210	fsumrecl 15707	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ)
221	220	rexrd 11231	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ^*)
222		nfv 1914	. . . . . . . 8 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺)
223		iunss1 4973	. . . . . . . . . . . 12 ⊢ (𝑦 ⊆ 𝐴 → ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
224	193, 223	syl 17	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
225	224	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
226	217, 225	ssexd 5282	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)
227	226	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)
228		simpll 766	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵) → 𝜑)
229	225	sselda 3949	. . . . . . . . . 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 5083	. . . . . . . . . . . 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 46418	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
242	214, 220	eqeltrd 2829	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ∈ ℝ)
243	241, 242	eqeltrd 2829	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) ∈ ℝ)
244	243	adantr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) ∈ ℝ)
245	222, 227, 231, 232, 244	sge0ltfirpmpt 46413	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)(Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝))
246		nfv 1914	. . . . . . . 8 ⊢ Ⅎ𝑏((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺)
247		nfre1 3263	. . . . . . . 8 ⊢ Ⅎ𝑏∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝)
248	223	sspwd 4579	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊆ 𝐴 → 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵)
249	193, 248	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵)
250	249	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵)
251		elinel1 4167	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) → 𝑏 ∈ 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵)
252	251	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵)
253	250, 252	sseldd 3950	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵)
254		elinel2 4168	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) → 𝑏 ∈ Fin)
255	254	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ Fin)
256	253, 255	elind 4166	. . . . . . . . . . . 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 1914	. . . . . . . . . . . . . . . 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 4575	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) → 𝑏 ⊆ ∪ 𝑥 ∈ 𝑦 𝐵)
266	265	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ⊆ ∪ 𝑥 ∈ 𝑦 𝐵)
267	261, 262, 263, 264, 266	sge0ssrempt 46410	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) ∈ ℝ)
268	267	rexrd 11231	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) ∈ ℝ^*)
269	268	adantlr 715	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) ∈ ℝ^*)
270		rpxr 12968	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ℝ⁺ → 𝑝 ∈ ℝ^*)
271	270	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑝 ∈ ℝ^*)
272	269, 271	xaddcld 13268	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝) ∈ ℝ^*)
273	272	3adant3 1132	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝) ∈ ℝ^*)
274		simp3 1138	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝))
275	241, 214	eqtr2d 2766	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)))
276	275	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)))
277	276	3ad2ant1 1133	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)))
278	267	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) ∈ ℝ)
279		rpre 12967	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ∈ ℝ⁺ → 𝑝 ∈ ℝ)
280	279	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑝 ∈ ℝ)
281		rexadd 13199	. . . . . . . . . . . . . . 15 ⊢ (((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) ∈ ℝ ∧ 𝑝 ∈ ℝ) → ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝) = ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝))
282	278, 280, 281	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝) = ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝))
283	282	3adant3 1132	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝) = ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝))
284	277, 283	breq12d 5123	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → (Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝) ↔ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)))
285	274, 284	mpbird 257	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝))
286	260, 273, 285	xrltled 13117	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝))
287		rspe 3228	. . . . . . . . . 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 3245	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → (∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)(Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝)))
291	245, 290	mpd 15	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝))
292	216, 217, 219, 221, 291	sge0gerpmpt 46407	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
293	215, 292	eqbrtrd 5132	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
294	293	ralrimiva 3126	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
295		eqid 2730	. . . . 5 ⊢ (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
296	179, 295	fmptd 7089	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞))
297	132, 296, 1	sge0lefi 46403	. . 3 ⊢ (𝜑 → ((Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ↔ ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶))))
298	294, 297	mpbird 257	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
299	1, 2, 192, 298	xrletrid 13122	1 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2926 ∀wral 3045 ∃wrex 3054 {crab 3408 Vcvv 3450 ⦋csb 3865 ∩ cin 3916 ⊆ wss 3917 ∅c0 4299 𝒫 cpw 4566 ∪ ciun 4958 Disj wdisj 5077 class class class wbr 5110 ↦ cmpt 5191 ↾ cres 5643 ⟶wf 6510 ‘cfv 6514 (class class class)co 7390 Fincfn 8921 ℂcc 11073 ℝcr 11074 0cc0 11075 + caddc 11078 +∞cpnf 11212 ℝ^*cxr 11214 < clt 11215 ≤ cle 11216 ℝ⁺crp 12958 +_𝑒 cxad 13077 [,)cico 13315 [,]cicc 13316 Σcsu 15659 Σ^{^}csumge0 46367

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-inf2 9601 ax-ac2 10423 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152 ax-pre-sup 11153

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3356 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-int 4914 df-iun 4960 df-disj 5078 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-se 5595 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-isom 6523 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7846 df-1st 7971 df-2nd 7972 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8381 df-1o 8437 df-er 8674 df-map 8804 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-sup 9400 df-oi 9470 df-card 9899 df-acn 9902 df-ac 10076 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-sub 11414 df-neg 11415 df-div 11843 df-nn 12194 df-2 12256 df-3 12257 df-n0 12450 df-z 12537 df-uz 12801 df-rp 12959 df-xadd 13080 df-ico 13319 df-icc 13320 df-fz 13476 df-fzo 13623 df-seq 13974 df-exp 14034 df-hash 14303 df-cj 15072 df-re 15073 df-im 15074 df-sqrt 15208 df-abs 15209 df-clim 15461 df-sum 15660 df-sumge0 46368

This theorem is referenced by: sge0iunmpt 46423

W3C validator