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 46432

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 45065	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
4	3	resmptd 5986	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → ((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦) = (𝑘 ∈ 𝑦 ↦ 𝐶))
5	4	fveq2d 6821	. . . . . . . 8 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → (Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) = (Σ^{^}‘(𝑘 ∈ 𝑦 ↦ 𝐶)))
6	5	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) = (Σ^{^}‘(𝑘 ∈ 𝑦 ↦ 𝐶)))
7		elinel2 4150	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → 𝑦 ∈ Fin)
8	7	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → 𝑦 ∈ Fin)
9	3	sselda 3932	. . . . . . . . . . 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 2892	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥𝑦
15		nfiu1 4975	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
16	15	nfpw 4567	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥𝒫 ∪ 𝑥 ∈ 𝐴 𝐵
17		nfcv 2892	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥Fin
18	16, 17	nfin 4172	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)
19	14, 18	nfel 2907	. . . . . . . . . . . 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 2730	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ 𝐵 ↦ 𝐶)
27	26	fvmpt2 6935	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ 𝐵 ∧ 𝐶 ∈ (0[,]+∞)) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘) = 𝐶)
28	24, 25, 27	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘) = 𝐶)
29	28	eqcomd 2736	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘))
30	25	3expa 1118	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
31	30, 26	fmptd 7042	. . . . . . . . . . . . . . . 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 46405	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → ¬ +∞ ∈ ran (𝑘 ∈ 𝐵 ↦ 𝐶))
38	32, 37	fge0iccico 46387	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,)+∞))
39	38, 24	ffvelcdmd 7013	. . . . . . . . . . . . 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 3237	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,)+∞)))
44	12, 43	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝐶 ∈ (0[,)+∞))
45	8, 44	sge0fsummpt 46407	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑦 ↦ 𝐶)) = Σ𝑘 ∈ 𝑦 𝐶)
46		sseqin2 4171	. . . . . . . . . . . . . 14 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦) = 𝑦)
47	46	biimpi 216	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦) = 𝑦)
48	47	eqcomd 2736	. . . . . . . . . . . 12 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦))
49		iunin1 5018	. . . . . . . . . . . . 13 ⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦) = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦)
50	49	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦) = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦))
51	48, 50	eqtr4d 2768	. . . . . . . . . . 11 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 = ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦))
52	3, 51	syl 17	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → 𝑦 = ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦))
53	52	sumeq1d 15599	. . . . . . . . 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 13348	. . . . . . . . . . . . 13 ⊢ (0[,)+∞) ⊆ ℝ
60		ax-resscn 11055	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
61	59, 60	sstri 3942	. . . . . . . . . . . 12 ⊢ (0[,)+∞) ⊆ ℂ
62	61, 40	sselid 3930	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
63	62	3adant1r 1178	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
64		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → 𝑦 ∈ Fin)
65	56, 58, 63, 64	fsumiunss 45594	. . . . . . . . 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 45208	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ∈ Fin)
70		id 22	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ Fin → 𝑦 ∈ Fin)
71		inss2 4186	. . . . . . . . . . . . . 14 ⊢ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ⊆ 𝑦
72	71	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ Fin → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ⊆ 𝑦)
73		ssfi 9077	. . . . . . . . . . . . 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 3641	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} → 𝑤 ∈ 𝐴)
78	77	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝑤 ∈ 𝐴)
79		elinel1 4149	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) → 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵)
80	79	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵)
81		nfv 1915	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑤 ∈ 𝐴
82		nfcv 2892	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥𝑘
83		nfcsb1v 3872	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝐵
84	82, 83	nfel 2907	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵
85	13, 81, 84	nf3an 1902	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵)
86	85, 23	nfim 1897	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,)+∞))
87		eleq1w 2812	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))
88		csbeq1a 3862	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑤 → 𝐵 = ⦋𝑤 / 𝑥⦌𝐵)
89	88	eleq2d 2815	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (𝑘 ∈ 𝐵 ↔ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵))
90	87, 89	3anbi23d 1441	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) ↔ (𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵)))
91	90	imbi1d 341	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,)+∞)) ↔ ((𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,)+∞))))
92	86, 91, 40	chvarfv 2242	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,)+∞))
93	76, 78, 80, 92	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,)+∞))
94	93	adantllr 719	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,)+∞))
95	75, 94	fsumge0cl 45592	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) → Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶 ∈ (0[,)+∞))
96	69, 95	sge0fsummpt 46407	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)) = Σ𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)
97		inss2 4186	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∩ 𝑦) ⊆ 𝑦
98	97	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ Fin → (𝐵 ∩ 𝑦) ⊆ 𝑦)
99		ssfi 9077	. . . . . . . . . . . . . . . 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 3414	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↔ (𝑥 ∈ 𝐴 ∧ (𝐵 ∩ 𝑦) ≠ ∅))
104	103	biimpi 216	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} → (𝑥 ∈ 𝐴 ∧ (𝐵 ∩ 𝑦) ≠ ∅))
105	104	simpld 494	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} → 𝑥 ∈ 𝐴)
106	105	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵 ∩ 𝑦)) → 𝑥 ∈ 𝐴)
107		elinel1 4149	. . . . . . . . . . . . . . . . 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 46407	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) → (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)) = Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
112	111	mpteq2dva 5182	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶))
113		nfrab1 3413	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}
114		nfcv 2892	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}
115		nfcv 2892	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶
116	83, 14	nfin 4172	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)
117		nfcv 2892	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥𝐶
118	116, 117	nfsum 15590	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶
119	88	ineq1d 4167	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → (𝐵 ∩ 𝑦) = (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦))
120	119	sumeq1d 15599	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶 = Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)
121	113, 114, 115, 118, 120	cbvmptf 5189	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶) = (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)
122	121	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶) = (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶))
123	112, 122	eqtr2d 2766	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶) = (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))))
124	123	fveq2d 6821	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)) = (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))))
125	124	eqcomd 2736	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) = (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)))
126	120, 115, 118	cbvsum 15594	. . . . . . . . . 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 3936	. . . . . . . . . 10 ⊢ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ⊆ 𝐴
134	133	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ⊆ 𝐴)
135	132, 134	ssexd 5260	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ∈ V)
136		vex 3438	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
137	136	inex2 5254	. . . . . . . . . . . 12 ⊢ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ∈ V
138	137	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ∈ V)
139		icossicc 13328	. . . . . . . . . . . . 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 3930	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,]+∞))
145		eqid 2730	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶) = (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)
146	144, 145	fmptd 7042	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶):(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)⟶(0[,]+∞))
147	138, 146	sge0cl 46398	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
148	77, 147	sylan2 593	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) → (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
149		nfcv 2892	. . . . . . . . . 10 ⊢ Ⅎ𝑤(Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))
150		nfcv 2892	. . . . . . . . . . 11 ⊢ Ⅎ𝑥Σ^{^}
151	116, 117	nfmpt 5187	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)
152	150, 151	nffv 6827	. . . . . . . . . 10 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))
153	119	mpteq1d 5179	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → (𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶) = (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))
154	153	fveq2d 6821	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))
155	113, 114, 149, 152, 154	cbvmptf 5189	. . . . . . . . 9 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))
156	148, 155	fmptd 7042	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))):{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}⟶(0[,]+∞))
157	135, 156	sge0xrcl 46402	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ∈ ℝ^*)
158	157	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ∈ ℝ^*)
159		eqid 2730	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))
160	147, 159	fmptd 7042	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))):𝐴⟶(0[,]+∞))
161	132, 160	sge0xrcl 46402	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ∈ ℝ^*)
162	161	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ∈ ℝ^*)
163	55, 2	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ∈ ℝ^*)
164	155	fveq2i 6820	. . . . . . . . 9 ⊢ (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) = (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))))
165	164	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) = (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))))
166	132, 147, 134	sge0lessmpt 46416	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))))
167	165, 166	eqbrtrd 5111	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))))
168	167	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))))
169	149, 152, 154	cbvmpt 5191	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))
170	169	eqcomi 2739	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))
171	170	fveq2i 6820	. . . . . . . . 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 2730	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶) = (𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)
177	175, 176	fmptd 7042	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶):(𝐵 ∩ 𝑦)⟶(0[,]+∞))
178	174, 177	sge0cl 46398	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
179	33, 31	sge0cl 46398	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ (0[,]+∞))
180		inss1 4185	. . . . . . . . . . 11 ⊢ (𝐵 ∩ 𝑦) ⊆ 𝐵
181	180	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ∩ 𝑦) ⊆ 𝐵)
182	33, 30, 181	sge0lessmpt 46416	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)) ≤ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
183	13, 132, 178, 179, 182	sge0lempt 46427	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
184	172, 183	eqbrtrd 5111	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
185	184	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
186	158, 162, 163, 168, 185	xrletrd 13053	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
187	131, 186	eqbrtrd 5111	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
188	187	ralrimiva 3122	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)(Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
189		sge0iunmptlemre.iue	. . . 4 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
190		sge0iunmptlemre.f	. . . 4 ⊢ (𝜑 → (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶):∪ 𝑥 ∈ 𝐴 𝐵⟶(0[,]+∞))
191	189, 190, 2	sge0lefi 46415	. . 3 ⊢ (𝜑 → ((Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ↔ ∀𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)(Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))))
192	188, 191	mpbird 257	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
193		elpwinss 45065	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴)
194	193	resmptd 5986	. . . . . . . 8 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → ((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦) = (𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
195	194	fveq2d 6821	. . . . . . 7 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → (Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) = (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
196	195	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) = (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
197		elinel2 4150	. . . . . . . 8 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin)
198	197	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ∈ Fin)
199		0xr 11151	. . . . . . . . 9 ⊢ 0 ∈ ℝ^*
200	199	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 0 ∈ ℝ^*)
201		pnfxr 11158	. . . . . . . . 9 ⊢ +∞ ∈ ℝ^*
202	201	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → +∞ ∈ ℝ^*)
203		simpll 766	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 𝜑)
204	193	sselda 3932	. . . . . . . . . . 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 46402	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ^*)
209	206, 207	sge0ge0 46401	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 0 ≤ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
210	203, 205, 35	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ)
211		ltpnf 13011	. . . . . . . . 9 ⊢ ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) < +∞)
212	210, 211	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) < +∞)
213	200, 202, 208, 209, 212	elicod 13287	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ (0[,)+∞))
214	198, 213	sge0fsummpt 46407	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
215	196, 214	eqtrd 2765	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) = Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
216		nfv 1915	. . . . . 6 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
217	189	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
218	190	fvmptelcdm 7041	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
219	218	adantlr 715	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
220	198, 210	fsumrecl 15633	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ)
221	220	rexrd 11154	. . . . . 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 3932	. . . . . . . . . 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 46430	. . . . . . . . . 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 46425	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)(Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝))
246		nfv 1915	. . . . . . . 8 ⊢ Ⅎ𝑏((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺)
247		nfre1 3255	. . . . . . . 8 ⊢ Ⅎ𝑏∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝)
248	223	sspwd 4561	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊆ 𝐴 → 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵)
249	193, 248	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵)
250	249	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵)
251		elinel1 4149	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) → 𝑏 ∈ 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵)
252	251	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵)
253	250, 252	sseldd 3933	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵)
254		elinel2 4150	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) → 𝑏 ∈ Fin)
255	254	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ Fin)
256	253, 255	elind 4148	. . . . . . . . . . . 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 4557	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) → 𝑏 ⊆ ∪ 𝑥 ∈ 𝑦 𝐵)
266	265	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ⊆ ∪ 𝑥 ∈ 𝑦 𝐵)
267	261, 262, 263, 264, 266	sge0ssrempt 46422	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) ∈ ℝ)
268	267	rexrd 11154	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) ∈ ℝ^*)
269	268	adantlr 715	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) ∈ ℝ^*)
270		rpxr 12892	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ℝ⁺ → 𝑝 ∈ ℝ^*)
271	270	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑝 ∈ ℝ^*)
272	269, 271	xaddcld 13192	. . . . . . . . . . . 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 12891	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ∈ ℝ⁺ → 𝑝 ∈ ℝ)
280	279	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑝 ∈ ℝ)
281		rexadd 13123	. . . . . . . . . . . . . . 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 13041	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝))
287		rspe 3220	. . . . . . . . . 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 3237	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → (∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)(Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝)))
291	245, 290	mpd 15	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝))
292	216, 217, 219, 221, 291	sge0gerpmpt 46419	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
293	215, 292	eqbrtrd 5111	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
294	293	ralrimiva 3122	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
295		eqid 2730	. . . . 5 ⊢ (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
296	179, 295	fmptd 7042	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞))
297	132, 296, 1	sge0lefi 46415	. . 3 ⊢ (𝜑 → ((Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ↔ ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶))))
298	294, 297	mpbird 257	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
299	1, 2, 192, 298	xrletrid 13046	1 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2110 ≠ wne 2926 ∀wral 3045 ∃wrex 3054 {crab 3393 Vcvv 3434 ⦋csb 3848 ∩ cin 3899 ⊆ wss 3900 ∅c0 4281 𝒫 cpw 4548 ∪ ciun 4939 Disj wdisj 5056 class class class wbr 5089 ↦ cmpt 5170 ↾ cres 5616 ⟶wf 6473 ‘cfv 6477 (class class class)co 7341 Fincfn 8864 ℂcc 10996 ℝcr 10997 0cc0 10998 + caddc 11001 +∞cpnf 11135 ℝ^*cxr 11137 < clt 11138 ≤ cle 11139 ℝ⁺crp 12882 +_𝑒 cxad 13001 [,)cico 13239 [,]cicc 13240 Σcsu 15585 Σ^{^}csumge0 46379

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 2112 ax-9 2120 ax-10 2143 ax-11 2159 ax-12 2179 ax-ext 2702 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7663 ax-inf2 9526 ax-ac2 10346 ax-cnex 11054 ax-resscn 11055 ax-1cn 11056 ax-icn 11057 ax-addcl 11058 ax-addrcl 11059 ax-mulcl 11060 ax-mulrcl 11061 ax-mulcom 11062 ax-addass 11063 ax-mulass 11064 ax-distr 11065 ax-i2m1 11066 ax-1ne0 11067 ax-1rid 11068 ax-rnegex 11069 ax-rrecex 11070 ax-cnre 11071 ax-pre-lttri 11072 ax-pre-lttrn 11073 ax-pre-ltadd 11074 ax-pre-mulgt0 11075 ax-pre-sup 11076

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 2067 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 3344 df-reu 3345 df-rab 3394 df-v 3436 df-sbc 3740 df-csb 3849 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-pss 3920 df-nul 4282 df-if 4474 df-pw 4550 df-sn 4575 df-pr 4577 df-op 4581 df-uni 4858 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 6244 df-ord 6305 df-on 6306 df-lim 6307 df-suc 6308 df-iota 6433 df-fun 6479 df-fn 6480 df-f 6481 df-f1 6482 df-fo 6483 df-f1o 6484 df-fv 6485 df-isom 6486 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-om 7792 df-1st 7916 df-2nd 7917 df-frecs 8206 df-wrecs 8237 df-recs 8286 df-rdg 8324 df-1o 8380 df-er 8617 df-map 8747 df-en 8865 df-dom 8866 df-sdom 8867 df-fin 8868 df-sup 9321 df-oi 9391 df-card 9824 df-acn 9827 df-ac 9999 df-pnf 11140 df-mnf 11141 df-xr 11142 df-ltxr 11143 df-le 11144 df-sub 11338 df-neg 11339 df-div 11767 df-nn 12118 df-2 12180 df-3 12181 df-n0 12374 df-z 12461 df-uz 12725 df-rp 12883 df-xadd 13004 df-ico 13243 df-icc 13244 df-fz 13400 df-fzo 13547 df-seq 13901 df-exp 13961 df-hash 14230 df-cj 14998 df-re 14999 df-im 15000 df-sqrt 15134 df-abs 15135 df-clim 15387 df-sum 15586 df-sumge0 46380

This theorem is referenced by: sge0iunmpt 46435

W3C validator