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 46994

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 45634	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
4	3	resmptd 6031	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → ((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦) = (𝑘 ∈ 𝑦 ↦ 𝐶))
5	4	fveq2d 6873	. . . . . . . 8 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → (Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) = (Σ^{^}‘(𝑘 ∈ 𝑦 ↦ 𝐶)))
6	5	adantl 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) = (Σ^{^}‘(𝑘 ∈ 𝑦 ↦ 𝐶)))
7		elinel2 4156	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → 𝑦 ∈ Fin)
8	7	adantl 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → 𝑦 ∈ Fin)
9	3	sselda 3938	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
10		eliun 4955	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
11	9, 10	sylib 220	. . . . . . . . . 10 ⊢ ((𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) ∧ 𝑘 ∈ 𝑦) → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
12	11	adantll 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
13		nfv 1936	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝜑
14		nfcv 2926	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥𝑦
15		nfiu1 4987	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
16	15	nfpw 4576	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥𝒫 ∪ 𝑥 ∈ 𝐴 𝐵
17		nfcv 2926	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥Fin
18	16, 17	nfin 4178	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)
19	14, 18	nfel 2940	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)
20	13, 19	nfan 1921	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin))
21		nfv 1936	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑘 ∈ 𝑦
22	20, 21	nfan 1921	. . . . . . . . . 10 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) ∧ 𝑘 ∈ 𝑦)
23		nfv 1936	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝐶 ∈ (0[,)+∞)
24		simp3 1152	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝑘 ∈ 𝐵)
25		sge0iunmptlemre.c	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
26		eqid 2764	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ 𝐵 ↦ 𝐶)
27	26	fvmpt2 6989	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ 𝐵 ∧ 𝐶 ∈ (0[,]+∞)) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘) = 𝐶)
28	24, 25, 27	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘) = 𝐶)
29	28	eqcomd 2770	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘))
30	25	3expa 1132	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
31	30, 26	fmptd 7097	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞))
32	31	3adant3 1146	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞))
33		sge0iunmptlemre.b	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)
34	33	3adant3 1146	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐵 ∈ 𝑊)
35		sge0iunmptlemre.re	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ)
36	35	3adant3 1146	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ)
37	34, 32, 36	sge0rern 46967	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → ¬ +∞ ∈ ran (𝑘 ∈ 𝐵 ↦ 𝐶))
38	32, 37	fge0iccico 46949	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,)+∞))
39	38, 24	ffvelcdmd 7068	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘) ∈ (0[,)+∞))
40	29, 39	eqeltrd 2864	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,)+∞))
41	40	3exp 1133	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,)+∞))))
42	41	ad2antrr 736	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (𝑥 ∈ 𝐴 → (𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,)+∞))))
43	22, 23, 42	rexlimd 3271	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,)+∞)))
44	12, 43	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝐶 ∈ (0[,)+∞))
45	8, 44	sge0fsummpt 46969	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑦 ↦ 𝐶)) = Σ𝑘 ∈ 𝑦 𝐶)
46		sseqin2 4177	. . . . . . . . . . . . . 14 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦) = 𝑦)
47	46	biimpi 218	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦) = 𝑦)
48	47	eqcomd 2770	. . . . . . . . . . . 12 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦))
49		iunin1 5031	. . . . . . . . . . . . 13 ⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦) = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦)
50	49	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦) = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦))
51	48, 50	eqtr4d 2802	. . . . . . . . . . 11 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 = ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦))
52	3, 51	syl 17	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → 𝑦 = ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦))
53	52	sumeq1d 15729	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → Σ𝑘 ∈ 𝑦 𝐶 = Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦)𝐶)
54	53	adantl 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → Σ𝑘 ∈ 𝑦 𝐶 = Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦)𝐶)
55		simpl 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → 𝜑)
56	33	adantlr 725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)
57		sge0iunmptlemre.dj	. . . . . . . . . . 11 ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)
58	57	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → Disj 𝑥 ∈ 𝐴 𝐵)
59		rge0ssre 13462	. . . . . . . . . . . . 13 ⊢ (0[,)+∞) ⊆ ℝ
60		ax-resscn 11132	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
61	59, 60	sstri 3947	. . . . . . . . . . . 12 ⊢ (0[,)+∞) ⊆ ℂ
62	61, 40	sselid 3936	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
63	62	3adant1r 1192	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
64		simpr 488	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → 𝑦 ∈ Fin)
65	56, 58, 63, 64	fsumiunss 46156	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦)𝐶 = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
66	55, 8, 65	syl2anc 593	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦)𝐶 = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
67	54, 66	eqtrd 2799	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → Σ𝑘 ∈ 𝑦 𝐶 = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
68	6, 45, 67	3eqtrd 2803	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
69	56, 58, 64	disjinfi 45775	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ∈ Fin)
70		id 22	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ Fin → 𝑦 ∈ Fin)
71		inss2 4191	. . . . . . . . . . . . . 14 ⊢ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ⊆ 𝑦
72	71	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ Fin → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ⊆ 𝑦)
73		ssfi 9143	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ Fin ∧ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ⊆ 𝑦) → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ∈ Fin)
74	70, 72, 73	syl2anc 593	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ Fin → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ∈ Fin)
75	74	ad2antlr 737	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ∈ Fin)
76		simpll 776	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝜑)
77		elrabi 3648	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} → 𝑤 ∈ 𝐴)
78	77	ad2antlr 737	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝑤 ∈ 𝐴)
79		elinel1 4155	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) → 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵)
80	79	adantl 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵)
81		nfv 1936	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑤 ∈ 𝐴
82		nfcv 2926	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥𝑘
83		nfcsb1v 3878	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝐵
84	82, 83	nfel 2940	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵
85	13, 81, 84	nf3an 1923	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵)
86	85, 23	nfim 1918	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,)+∞))
87		eleq1w 2847	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))
88		csbeq1a 3868	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑤 → 𝐵 = ⦋𝑤 / 𝑥⦌𝐵)
89	88	eleq2d 2850	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (𝑘 ∈ 𝐵 ↔ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵))
90	87, 89	3anbi23d 1462	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) ↔ (𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵)))
91	90	imbi1d 343	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,)+∞)) ↔ ((𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,)+∞))))
92	86, 91, 40	chvarfv 2277	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,)+∞))
93	76, 78, 80, 92	syl3anc 1392	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,)+∞))
94	93	adantllr 729	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,)+∞))
95	75, 94	fsumge0cl 46154	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) → Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶 ∈ (0[,)+∞))
96	69, 95	sge0fsummpt 46969	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)) = Σ𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)
97		inss2 4191	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∩ 𝑦) ⊆ 𝑦
98	97	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ Fin → (𝐵 ∩ 𝑦) ⊆ 𝑦)
99		ssfi 9143	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ Fin ∧ (𝐵 ∩ 𝑦) ⊆ 𝑦) → (𝐵 ∩ 𝑦) ∈ Fin)
100	70, 98, 99	syl2anc 593	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ Fin → (𝐵 ∩ 𝑦) ∈ Fin)
101	100	ad2antlr 737	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) → (𝐵 ∩ 𝑦) ∈ Fin)
102		simpll 776	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵 ∩ 𝑦)) → 𝜑)
103		rabid 3437	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↔ (𝑥 ∈ 𝐴 ∧ (𝐵 ∩ 𝑦) ≠ ∅))
104	103	biimpi 218	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} → (𝑥 ∈ 𝐴 ∧ (𝐵 ∩ 𝑦) ≠ ∅))
105	104	simpld 498	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} → 𝑥 ∈ 𝐴)
106	105	ad2antlr 737	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵 ∩ 𝑦)) → 𝑥 ∈ 𝐴)
107		elinel1 4155	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (𝐵 ∩ 𝑦) → 𝑘 ∈ 𝐵)
108	107	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵 ∩ 𝑦)) → 𝑘 ∈ 𝐵)
109	102, 106, 108, 40	syl3anc 1392	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,)+∞))
110	109	adantllr 729	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,)+∞))
111	101, 110	sge0fsummpt 46969	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) → (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)) = Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
112	111	mpteq2dva 5195	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶))
113		nfrab1 3436	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}
114		nfcv 2926	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}
115		nfcv 2926	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶
116	83, 14	nfin 4178	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)
117		nfcv 2926	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥𝐶
118	116, 117	nfsum 15720	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶
119	88	ineq1d 4173	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → (𝐵 ∩ 𝑦) = (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦))
120	119	sumeq1d 15729	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶 = Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)
121	113, 114, 115, 118, 120	cbvmptf 5202	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶) = (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)
122	121	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶) = (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶))
123	112, 122	eqtr2d 2800	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶) = (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))))
124	123	fveq2d 6873	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)) = (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))))
125	124	eqcomd 2770	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) = (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)))
126	120, 115, 118	cbvsum 15724	. . . . . . . . . 10 ⊢ Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶 = Σ𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶
127	126	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶 = Σ𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)
128	96, 125, 127	3eqtr4d 2809	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
129	55, 8, 128	syl2anc 593	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
130	129	eqcomd 2770	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶 = (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))))
131	68, 130	eqtrd 2799	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) = (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))))
132		sge0iunmptlemre.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
133	77	ssriv 3942	. . . . . . . . . 10 ⊢ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ⊆ 𝐴
134	133	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ⊆ 𝐴)
135	132, 134	ssexd 5282	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ∈ V)
136		vex 3460	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
137	136	inex2 5276	. . . . . . . . . . . 12 ⊢ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ∈ V
138	137	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ∈ V)
139		icossicc 13442	. . . . . . . . . . . . 13 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
140		simpll 776	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝜑)
141		simplr 778	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝑤 ∈ 𝐴)
142	79	adantl 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵)
143	140, 141, 142, 92	syl3anc 1392	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,)+∞))
144	139, 143	sselid 3936	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,]+∞))
145		eqid 2764	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶) = (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)
146	144, 145	fmptd 7097	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶):(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)⟶(0[,]+∞))
147	138, 146	sge0cl 46960	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
148	77, 147	sylan2 602	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) → (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
149		nfcv 2926	. . . . . . . . . 10 ⊢ Ⅎ𝑤(Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))
150		nfcv 2926	. . . . . . . . . . 11 ⊢ Ⅎ𝑥Σ^{^}
151	116, 117	nfmpt 5200	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)
152	150, 151	nffv 6879	. . . . . . . . . 10 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))
153	119	mpteq1d 5192	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → (𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶) = (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))
154	153	fveq2d 6873	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))
155	113, 114, 149, 152, 154	cbvmptf 5202	. . . . . . . . 9 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))
156	148, 155	fmptd 7097	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))):{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}⟶(0[,]+∞))
157	135, 156	sge0xrcl 46964	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ∈ ℝ^*)
158	157	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ∈ ℝ^*)
159		eqid 2764	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))
160	147, 159	fmptd 7097	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))):𝐴⟶(0[,]+∞))
161	132, 160	sge0xrcl 46964	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ∈ ℝ^*)
162	161	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ∈ ℝ^*)
163	55, 2	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ∈ ℝ^*)
164	155	fveq2i 6872	. . . . . . . . 9 ⊢ (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) = (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))))
165	164	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) = (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))))
166	132, 147, 134	sge0lessmpt 46978	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))))
167	165, 166	eqbrtrd 5124	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))))
168	167	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))))
169	149, 152, 154	cbvmpt 5204	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))
170	169	eqcomi 2773	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))
171	170	fveq2i 6872	. . . . . . . . 9 ⊢ (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))))
172	171	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))))
173	136	inex2 5276	. . . . . . . . . . 11 ⊢ (𝐵 ∩ 𝑦) ∈ V
174	173	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ∩ 𝑦) ∈ V)
175	107, 30	sylan2 602	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ (𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,]+∞))
176		eqid 2764	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶) = (𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)
177	175, 176	fmptd 7097	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶):(𝐵 ∩ 𝑦)⟶(0[,]+∞))
178	174, 177	sge0cl 46960	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
179	33, 31	sge0cl 46960	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ (0[,]+∞))
180		inss1 4190	. . . . . . . . . . 11 ⊢ (𝐵 ∩ 𝑦) ⊆ 𝐵
181	180	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ∩ 𝑦) ⊆ 𝐵)
182	33, 30, 181	sge0lessmpt 46978	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)) ≤ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
183	13, 132, 178, 179, 182	sge0lempt 46989	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
184	172, 183	eqbrtrd 5124	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
185	184	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
186	158, 162, 163, 168, 185	xrletrd 13166	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
187	131, 186	eqbrtrd 5124	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
188	187	ralrimiva 3156	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)(Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
189		sge0iunmptlemre.iue	. . . 4 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
190		sge0iunmptlemre.f	. . . 4 ⊢ (𝜑 → (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶):∪ 𝑥 ∈ 𝐴 𝐵⟶(0[,]+∞))
191	189, 190, 2	sge0lefi 46977	. . 3 ⊢ (𝜑 → ((Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ↔ ∀𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)(Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))))
192	188, 191	mpbird 259	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
193		elpwinss 45634	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴)
194	193	resmptd 6031	. . . . . . . 8 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → ((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦) = (𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
195	194	fveq2d 6873	. . . . . . 7 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → (Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) = (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
196	195	adantl 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) = (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
197		elinel2 4156	. . . . . . . 8 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin)
198	197	adantl 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ∈ Fin)
199		0xr 11231	. . . . . . . . 9 ⊢ 0 ∈ ℝ^*
200	199	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 0 ∈ ℝ^*)
201		pnfxr 11238	. . . . . . . . 9 ⊢ +∞ ∈ ℝ^*
202	201	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → +∞ ∈ ℝ^*)
203		simpll 776	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 𝜑)
204	193	sselda 3938	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴)
205	204	adantll 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴)
206	203, 205, 33	syl2anc 593	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 𝐵 ∈ 𝑊)
207	203, 205, 31	syl2anc 593	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞))
208	206, 207	sge0xrcl 46964	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ^*)
209	206, 207	sge0ge0 46963	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 0 ≤ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
210	203, 205, 35	syl2anc 593	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ)
211		ltpnf 13124	. . . . . . . . 9 ⊢ ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) < +∞)
212	210, 211	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) < +∞)
213	200, 202, 208, 209, 212	elicod 13401	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ (0[,)+∞))
214	198, 213	sge0fsummpt 46969	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
215	196, 214	eqtrd 2799	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) = Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
216		nfv 1936	. . . . . 6 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
217	189	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
218	190	fvmptelcdm 7096	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
219	218	adantlr 725	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
220	198, 210	fsumrecl 15763	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ)
221	220	rexrd 11234	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ^*)
222		nfv 1936	. . . . . . . 8 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺)
223		iunss1 4966	. . . . . . . . . . . 12 ⊢ (𝑦 ⊆ 𝐴 → ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
224	193, 223	syl 17	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
225	224	adantl 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
226	217, 225	ssexd 5282	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)
227	226	adantr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)
228		simpll 776	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵) → 𝜑)
229	225	sselda 3938	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵) → 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
230	228, 229, 218	syl2anc 593	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵) → 𝐶 ∈ (0[,]+∞))
231	230	adantlr 725	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵) → 𝐶 ∈ (0[,]+∞))
232		simpr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → 𝑝 ∈ ℝ⁺)
233	193	adantl 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ⊆ 𝐴)
234	57	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Disj 𝑥 ∈ 𝐴 𝐵)
235		disjss1 5075	. . . . . . . . . . . 12 ⊢ (𝑦 ⊆ 𝐴 → (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑥 ∈ 𝑦 𝐵))
236	233, 234, 235	sylc 65	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Disj 𝑥 ∈ 𝑦 𝐵)
237	203	3adant3 1146	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦 ∧ 𝑘 ∈ 𝐵) → 𝜑)
238	205	3adant3 1146	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦 ∧ 𝑘 ∈ 𝐵) → 𝑥 ∈ 𝐴)
239		simp3 1152	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦 ∧ 𝑘 ∈ 𝐵) → 𝑘 ∈ 𝐵)
240	237, 238, 239, 25	syl3anc 1392	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
241	198, 206, 236, 240, 210	sge0iunmptlemfi 46992	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
242	214, 220	eqeltrd 2864	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ∈ ℝ)
243	241, 242	eqeltrd 2864	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) ∈ ℝ)
244	243	adantr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) ∈ ℝ)
245	222, 227, 231, 232, 244	sge0ltfirpmpt 46987	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)(Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝))
246		nfv 1936	. . . . . . . 8 ⊢ Ⅎ𝑏((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺)
247		nfre1 3289	. . . . . . . 8 ⊢ Ⅎ𝑏∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝)
248	223	sspwd 4570	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊆ 𝐴 → 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵)
249	193, 248	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵)
250	249	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵)
251		elinel1 4155	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) → 𝑏 ∈ 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵)
252	251	adantl 485	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵)
253	250, 252	sseldd 3939	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵)
254		elinel2 4156	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) → 𝑏 ∈ Fin)
255	254	adantl 485	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ Fin)
256	253, 255	elind 4154	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin))
257	256	ad4ant24 764	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin))
258	257	3adant3 1146	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin))
259	221	ad2antrr 736	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ^*)
260	259	3adant3 1146	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ^*)
261		nfv 1936	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin))
262	226	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)
263	230	adantlr 725	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵) → 𝐶 ∈ (0[,]+∞))
264	243	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) ∈ ℝ)
265	251	elpwid 4566	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) → 𝑏 ⊆ ∪ 𝑥 ∈ 𝑦 𝐵)
266	265	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ⊆ ∪ 𝑥 ∈ 𝑦 𝐵)
267	261, 262, 263, 264, 266	sge0ssrempt 46984	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) ∈ ℝ)
268	267	rexrd 11234	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) ∈ ℝ^*)
269	268	adantlr 725	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) ∈ ℝ^*)
270		rpxr 13005	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ℝ⁺ → 𝑝 ∈ ℝ^*)
271	270	ad2antlr 737	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑝 ∈ ℝ^*)
272	269, 271	xaddcld 13306	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝) ∈ ℝ^*)
273	272	3adant3 1146	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝) ∈ ℝ^*)
274		simp3 1152	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝))
275	241, 214	eqtr2d 2800	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)))
276	275	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)))
277	276	3ad2ant1 1147	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)))
278	267	adantlr 725	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) ∈ ℝ)
279		rpre 13004	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ∈ ℝ⁺ → 𝑝 ∈ ℝ)
280	279	ad2antlr 737	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑝 ∈ ℝ)
281		rexadd 13237	. . . . . . . . . . . . . . 15 ⊢ (((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) ∈ ℝ ∧ 𝑝 ∈ ℝ) → ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝) = ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝))
282	278, 280, 281	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝) = ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝))
283	282	3adant3 1146	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝) = ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝))
284	277, 283	breq12d 5115	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → (Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝) ↔ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)))
285	274, 284	mpbird 259	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝))
286	260, 273, 285	xrltled 13154	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝))
287		rspe 3254	. . . . . . . . . 10 ⊢ ((𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) ∧ Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝)) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝))
288	258, 286, 287	syl2anc 593	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝))
289	288	3exp 1133	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → (𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) → ((Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝))))
290	246, 247, 289	rexlimd 3271	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → (∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)(Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝)))
291	245, 290	mpd 15	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_𝑒 𝑝))
292	216, 217, 219, 221, 291	sge0gerpmpt 46981	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
293	215, 292	eqbrtrd 5124	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
294	293	ralrimiva 3156	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
295		eqid 2764	. . . . 5 ⊢ (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
296	179, 295	fmptd 7097	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞))
297	132, 296, 1	sge0lefi 46977	. . 3 ⊢ (𝜑 → ((Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ↔ ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶))))
298	294, 297	mpbird 259	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
299	1, 2, 192, 298	xrletrid 13159	1 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1099 = wceq 1562 ∈ wcel 2144 ≠ wne 2959 ∀wral 3078 ∃wrex 3088 {crab 3416 Vcvv 3456 ⦋csb 3854 ∩ cin 3905 ⊆ wss 3906 ∅c0 4287 𝒫 cpw 4557 ∪ ciun 4951 Disj wdisj 5069 class class class wbr 5102 ↦ cmpt 5183 ↾ cres 5651 ⟶wf 6519 ‘cfv 6523 (class class class)co 7398 Fincfn 8929 ℂcc 11073 ℝcr 11074 0cc0 11075 + caddc 11078 +∞cpnf 11215 ℝ^*cxr 11217 < clt 11218 ≤ cle 11219 ℝ⁺crp 12995 +_𝑒 cxad 13114 [,)cico 13353 [,]cicc 13354 Σcsu 15715 Σ^{^}csumge0 46941

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1817 ax-4 1831 ax-5 1932 ax-6 1989 ax-7 2030 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2214 ax-ext 2736 ax-rep 5229 ax-sep 5248 ax-nul 5258 ax-pow 5324 ax-pr 5392 ax-un 7720 ax-inf2 9598 ax-ac2 10422 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 209 df-an 400 df-or 859 df-3or 1100 df-3an 1101 df-tru 1565 df-fal 1575 df-ex 1802 df-nf 1806 df-sb 2093 df-mo 2568 df-eu 2598 df-clab 2743 df-cleq 2756 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3458 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-disj 5070 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5544 df-eprel 5549 df-po 5557 df-so 5558 df-fr 5602 df-se 5603 df-we 5604 df-xp 5655 df-rel 5656 df-cnv 5657 df-co 5658 df-dm 5659 df-rn 5660 df-res 5661 df-ima 5662 df-pred 6290 df-ord 6351 df-on 6352 df-lim 6353 df-suc 6354 df-iota 6479 df-fun 6525 df-fn 6526 df-f 6527 df-f1 6528 df-fo 6529 df-f1o 6530 df-fv 6531 df-isom 6532 df-riota 7355 df-ov 7401 df-oprab 7402 df-mpo 7403 df-om 7849 df-1st 7972 df-2nd 7973 df-frecs 8264 df-wrecs 8295 df-recs 8344 df-rdg 8383 df-1o 8439 df-er 8680 df-map 8812 df-en 8930 df-dom 8931 df-sdom 8932 df-fin 8933 df-sup 9390 df-oi 9460 df-card 9899 df-acn 9902 df-ac 10074 df-pnf 11220 df-mnf 11221 df-xr 11222 df-ltxr 11223 df-le 11224 df-sub 11418 df-neg 11419 df-div 11847 df-nn 12213 df-2 12282 df-3 12283 df-n0 12484 df-z 12571 df-uz 12842 df-rp 12996 df-xadd 13117 df-ico 13357 df-icc 13358 df-fz 13515 df-fzo 13662 df-seq 14017 df-exp 14077 df-hash 14346 df-cj 15128 df-re 15129 df-im 15130 df-sqrt 15264 df-abs 15265 df-clim 15517 df-sum 15716 df-sumge0 46942

This theorem is referenced by: sge0iunmpt 46997

W3C validator