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 47628

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 46269	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
4	3	resmptd 6043	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → ((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦) = (𝑘 ∈ 𝑦 ↦ 𝐶))
5	4	fveq2d 6909	. . . . . . . 8 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → (Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) = (Σ^{^}‘(𝑘 ∈ 𝑦 ↦ 𝐶)))
6	5	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) = (Σ^{^}‘(𝑘 ∈ 𝑦 ↦ 𝐶)))
7		elinel2 4102	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → 𝑦 ∈ Fin)
8	7	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → 𝑦 ∈ Fin)
9	3	sselda 3913	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) ∧ 𝑘 ∈ 𝑦) → 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
10		eliun 4958	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
11	9, 10	sylib 221	. . . . . . . . . 10 ⊢ ((𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) ∧ 𝑘 ∈ 𝑦) → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
12	11	adantll 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
13		nfv 1949	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝜑
14		nfcv 2926	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥𝑦
15		nfiu1 4989	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
16	15	nfpw 4580	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥𝒫 ∪ 𝑥 ∈ 𝐴 𝐵
17		nfcv 2926	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥Fin
18	16, 17	nfin 4124	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)
19	14, 18	nfel 2940	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)
20	13, 19	nfan 1934	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin))
21		nfv 1949	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑘 ∈ 𝑦
22	20, 21	nfan 1934	. . . . . . . . . 10 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) ∧ 𝑘 ∈ 𝑦)
23		nfv 1949	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝐶 ∈ (0[,)+∞)
24		simp3 1156	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝑘 ∈ 𝐵)
25		sge0iunmptlemre.c	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
26		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ 𝐵 ↦ 𝐶)
27	26	fvmpt2 7025	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ 𝐵 ∧ 𝐶 ∈ (0[,]+∞)) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘) = 𝐶)
28	24, 25, 27	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘) = 𝐶)
29	28	eqcomd 2769	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘))
30	25	3expa 1136	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
31	30, 26	fmptd 7135	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞))
32	31	3adant3 1150	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞))
33		sge0iunmptlemre.b	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)
34	33	3adant3 1150	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐵 ∈ 𝑊)
35		sge0iunmptlemre.re	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ)
36	35	3adant3 1150	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ)
37	34, 32, 36	sge0rern 47601	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → ¬ +∞ ∈ ran (𝑘 ∈ 𝐵 ↦ 𝐶))
38	32, 37	fge0iccico 47583	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,)+∞))
39	38, 24	ffvelcdmd 7106	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘) ∈ (0[,)+∞))
40	29, 39	eqeltrd 2864	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,)+∞))
41	40	3exp 1137	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,)+∞))))
42	41	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (𝑥 ∈ 𝐴 → (𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,)+∞))))
43	22, 23, 42	rexlimd 3273	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → (∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 → 𝐶 ∈ (0[,)+∞)))
44	12, 43	mpd 16	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) ∧ 𝑘 ∈ 𝑦) → 𝐶 ∈ (0[,)+∞))
45	8, 44	sge0fsummpt 47603	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑦 ↦ 𝐶)) = Σ𝑘 ∈ 𝑦 𝐶)
46		sseqin2 4123	. . . . . . . . . . . . . 14 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦) = 𝑦)
47	46	biimpi 219	. . . . . . . . . . . . 13 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦) = 𝑦)
48	47	eqcomd 2769	. . . . . . . . . . . 12 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦))
49		iunin1 5033	. . . . . . . . . . . . 13 ⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦) = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦)
50	49	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦) = (∪ 𝑥 ∈ 𝐴 𝐵 ∩ 𝑦))
51	48, 50	eqtr4d 2801	. . . . . . . . . . 11 ⊢ (𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 = ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦))
52	3, 51	syl 18	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → 𝑦 = ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦))
53	52	sumeq1d 15893	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) → Σ𝑘 ∈ 𝑦 𝐶 = Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦)𝐶)
54	53	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → Σ𝑘 ∈ 𝑦 𝐶 = Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦)𝐶)
55		simpl 488	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → 𝜑)
56	33	adantlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)
57		sge0iunmptlemre.dj	. . . . . . . . . . 11 ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵)
58	57	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → Disj 𝑥 ∈ 𝐴 𝐵)
59		rge0ssre 13611	. . . . . . . . . . . . 13 ⊢ (0[,)+∞) ⊆ ℝ
60		ax-resscn 11281	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
61	59, 60	sstri 3922	. . . . . . . . . . . 12 ⊢ (0[,)+∞) ⊆ ℂ
62	61, 40	sselid 3911	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
63	62	3adant1r 1196	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
64		simpr 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → 𝑦 ∈ Fin)
65	56, 58, 63, 64	fsumiunss 46790	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦)𝐶 = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
66	55, 8, 65	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ∩ 𝑦)𝐶 = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
67	54, 66	eqtrd 2798	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → Σ𝑘 ∈ 𝑦 𝐶 = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
68	6, 45, 67	3eqtrd 2802	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
69	56, 58, 64	disjinfi 46410	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ∈ Fin)
70		id 23	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ Fin → 𝑦 ∈ Fin)
71		inss2 4137	. . . . . . . . . . . . . 14 ⊢ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ⊆ 𝑦
72	71	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ Fin → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ⊆ 𝑦)
73		ssfi 9213	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ Fin ∧ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ⊆ 𝑦) → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ∈ Fin)
74	70, 72, 73	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ Fin → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ∈ Fin)
75	74	ad2antlr 740	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ∈ Fin)
76		simpll 779	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝜑)
77		elrabi 3644	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} → 𝑤 ∈ 𝐴)
78	77	ad2antlr 740	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝑤 ∈ 𝐴)
79		elinel1 4101	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) → 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵)
80	79	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵)
81		nfv 1949	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑤 ∈ 𝐴
82		nfcv 2926	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥𝑘
83		nfcsb1v 3875	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥⦋𝑤 / 𝑥⦌𝐵
84	82, 83	nfel 2940	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵
85	13, 81, 84	nf3an 1936	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵)
86	85, 23	nfim 1931	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥((𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,)+∞))
87		eleq1w 2847	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))
88		csbeq1a 3865	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑤 → 𝐵 = ⦋𝑤 / 𝑥⦌𝐵)
89	88	eleq2d 2850	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (𝑘 ∈ 𝐵 ↔ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵))
90	87, 89	3anbi23d 1468	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) ↔ (𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵)))
91	90	imbi1d 344	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,)+∞)) ↔ ((𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,)+∞))))
92	86, 91, 40	chvarfv 2280	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴 ∧ 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵) → 𝐶 ∈ (0[,)+∞))
93	76, 78, 80, 92	syl3anc 1399	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,)+∞))
94	93	adantllr 732	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,)+∞))
95	75, 94	fsumge0cl 46788	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) → Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶 ∈ (0[,)+∞))
96	69, 95	sge0fsummpt 47603	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)) = Σ𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)
97		inss2 4137	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∩ 𝑦) ⊆ 𝑦
98	97	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ Fin → (𝐵 ∩ 𝑦) ⊆ 𝑦)
99		ssfi 9213	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ Fin ∧ (𝐵 ∩ 𝑦) ⊆ 𝑦) → (𝐵 ∩ 𝑦) ∈ Fin)
100	70, 98, 99	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ Fin → (𝐵 ∩ 𝑦) ∈ Fin)
101	100	ad2antlr 740	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) → (𝐵 ∩ 𝑦) ∈ Fin)
102		simpll 779	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵 ∩ 𝑦)) → 𝜑)
103		rabid 3436	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↔ (𝑥 ∈ 𝐴 ∧ (𝐵 ∩ 𝑦) ≠ ∅))
104	103	biimpi 219	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} → (𝑥 ∈ 𝐴 ∧ (𝐵 ∩ 𝑦) ≠ ∅))
105	104	simpld 500	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} → 𝑥 ∈ 𝐴)
106	105	ad2antlr 740	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵 ∩ 𝑦)) → 𝑥 ∈ 𝐴)
107		elinel1 4101	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ (𝐵 ∩ 𝑦) → 𝑘 ∈ 𝐵)
108	107	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵 ∩ 𝑦)) → 𝑘 ∈ 𝐵)
109	102, 106, 108, 40	syl3anc 1399	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,)+∞))
110	109	adantllr 732	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) ∧ 𝑘 ∈ (𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,)+∞))
111	101, 110	sge0fsummpt 47603	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ Fin) ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) → (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)) = Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
112	111	mpteq2dva 5201	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶))
113		nfrab1 3435	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}
114		nfcv 2926	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}
115		nfcv 2926	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶
116	83, 14	nfin 4124	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)
117		nfcv 2926	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥𝐶
118	116, 117	nfsum 15884	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶
119	88	ineq1d 4119	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → (𝐵 ∩ 𝑦) = (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦))
120	119	sumeq1d 15893	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶 = Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)
121	113, 114, 115, 118, 120	cbvmptf 5208	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶) = (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)
122	121	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶) = (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶))
123	112, 122	eqtr2d 2799	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶) = (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))))
124	123	fveq2d 6909	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)) = (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))))
125	124	eqcomd 2769	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) = (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)))
126	120, 115, 118	cbvsum 15888	. . . . . . . . . 10 ⊢ Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶 = Σ𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶
127	126	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶 = Σ𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)𝐶)
128	96, 125, 127	3eqtr4d 2808	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ Fin) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
129	55, 8, 128	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) = Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶)
130	129	eqcomd 2769	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → Σ𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}Σ𝑘 ∈ (𝐵 ∩ 𝑦)𝐶 = (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))))
131	68, 130	eqtrd 2798	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) = (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))))
132		sge0iunmptlemre.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
133	77	ssriv 3917	. . . . . . . . . 10 ⊢ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ⊆ 𝐴
134	133	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ⊆ 𝐴)
135	132, 134	ssexd 5290	. . . . . . . 8 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ∈ V)
136		vex 3458	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
137	136	inex2 5282	. . . . . . . . . . . 12 ⊢ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ∈ V
138	137	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ∈ V)
139		icossicc 13591	. . . . . . . . . . . . 13 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
140		simpll 779	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝜑)
141		simplr 781	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝑤 ∈ 𝐴)
142	79	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝑘 ∈ ⦋𝑤 / 𝑥⦌𝐵)
143	140, 141, 142, 92	syl3anc 1399	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,)+∞))
144	139, 143	sselid 3911	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑤 ∈ 𝐴) ∧ 𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,]+∞))
145		eqid 2763	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶) = (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)
146	144, 145	fmptd 7135	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶):(⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦)⟶(0[,]+∞))
147	138, 146	sge0cl 47594	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
148	77, 147	sylan2 605	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}) → (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
149		nfcv 2926	. . . . . . . . . 10 ⊢ Ⅎ𝑤(Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))
150		nfcv 2926	. . . . . . . . . . 11 ⊢ Ⅎ𝑥Σ^{^}
151	116, 117	nfmpt 5206	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)
152	150, 151	nffv 6915	. . . . . . . . . 10 ⊢ Ⅎ𝑥(Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))
153	119	mpteq1d 5198	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → (𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶) = (𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))
154	153	fveq2d 6909	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))
155	113, 114, 149, 152, 154	cbvmptf 5208	. . . . . . . . 9 ⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))
156	148, 155	fmptd 7135	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))):{𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅}⟶(0[,]+∞))
157	135, 156	sge0xrcl 47598	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ∈ ℝ^*)
158	157	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ∈ ℝ^*)
159		eqid 2763	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))
160	147, 159	fmptd 7135	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))):𝐴⟶(0[,]+∞))
161	132, 160	sge0xrcl 47598	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ∈ ℝ^*)
162	161	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ∈ ℝ^*)
163	55, 2	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ∈ ℝ^*)
164	155	fveq2i 6908	. . . . . . . . 9 ⊢ (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) = (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))))
165	164	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) = (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))))
166	132, 147, 134	sge0lessmpt 47612	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))))
167	165, 166	eqbrtrd 5130	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))))
168	167	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))))
169	149, 152, 154	cbvmpt 5210	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))
170	169	eqcomi 2772	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶))) = (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))
171	170	fveq2i 6908	. . . . . . . . 9 ⊢ (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶))))
172	171	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))))
173	136	inex2 5282	. . . . . . . . . . 11 ⊢ (𝐵 ∩ 𝑦) ∈ V
174	173	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ∩ 𝑦) ∈ V)
175	107, 30	sylan2 605	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ (𝐵 ∩ 𝑦)) → 𝐶 ∈ (0[,]+∞))
176		eqid 2763	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶) = (𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)
177	175, 176	fmptd 7135	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶):(𝐵 ∩ 𝑦)⟶(0[,]+∞))
178	174, 177	sge0cl 47594	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)) ∈ (0[,]+∞))
179	33, 31	sge0cl 47594	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ (0[,]+∞))
180		inss1 4136	. . . . . . . . . . 11 ⊢ (𝐵 ∩ 𝑦) ⊆ 𝐵
181	180	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ∩ 𝑦) ⊆ 𝐵)
182	33, 30, 181	sge0lessmpt 47612	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)) ≤ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
183	13, 132, 178, 179, 182	sge0lempt 47623	. . . . . . . 8 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
184	172, 183	eqbrtrd 5130	. . . . . . 7 ⊢ (𝜑 → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
185	184	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑤 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ (⦋𝑤 / 𝑥⦌𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
186	158, 162, 163, 168, 185	xrletrd 13315	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ {𝑥 ∈ 𝐴 ∣ (𝐵 ∩ 𝑦) ≠ ∅} ↦ (Σ^{^}‘(𝑘 ∈ (𝐵 ∩ 𝑦) ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
187	131, 186	eqbrtrd 5130	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)) → (Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
188	187	ralrimiva 3158	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)(Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
189		sge0iunmptlemre.iue	. . . 4 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
190		sge0iunmptlemre.f	. . . 4 ⊢ (𝜑 → (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶):∪ 𝑥 ∈ 𝐴 𝐵⟶(0[,]+∞))
191	189, 190, 2	sge0lefi 47611	. . 3 ⊢ (𝜑 → ((Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ↔ ∀𝑦 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)(Σ^{^}‘((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))))
192	188, 191	mpbird 260	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ≤ (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
193		elpwinss 46269	. . . . . . . . 9 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴)
194	193	resmptd 6043	. . . . . . . 8 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → ((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦) = (𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))))
195	194	fveq2d 6909	. . . . . . 7 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → (Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) = (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
196	195	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) = (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
197		elinel2 4102	. . . . . . . 8 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin)
198	197	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ∈ Fin)
199		0xr 11380	. . . . . . . . 9 ⊢ 0 ∈ ℝ^*
200	199	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 0 ∈ ℝ^*)
201		pnfxr 11387	. . . . . . . . 9 ⊢ +∞ ∈ ℝ^*
202	201	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → +∞ ∈ ℝ^*)
203		simpll 779	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 𝜑)
204	193	sselda 3913	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴)
205	204	adantll 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴)
206	203, 205, 33	syl2anc 596	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 𝐵 ∈ 𝑊)
207	203, 205, 31	syl2anc 596	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶(0[,]+∞))
208	206, 207	sge0xrcl 47598	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ^*)
209	206, 207	sge0ge0 47597	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → 0 ≤ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
210	203, 205, 35	syl2anc 596	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ)
211		ltpnf 13273	. . . . . . . . 9 ⊢ ((Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) < +∞)
212	210, 211	syl 18	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) < +∞)
213	200, 202, 208, 209, 212	elicod 13550	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦) → (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ (0[,)+∞))
214	198, 213	sge0fsummpt 47603	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) = Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
215	196, 214	eqtrd 2798	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) = Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
216		nfv 1949	. . . . . 6 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
217	189	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
218	190	fvmptelcdm 7134	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
219	218	adantlr 728	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
220	198, 210	fsumrecl 15926	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ)
221	220	rexrd 11383	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ^*)
222		nfv 1949	. . . . . . . 8 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺)
223		iunss1 4969	. . . . . . . . . . . 12 ⊢ (𝑦 ⊆ 𝐴 → ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
224	193, 223	syl 18	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
225	224	adantl 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
226	217, 225	ssexd 5290	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)
227	226	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)
228		simpll 779	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵) → 𝜑)
229	225	sselda 3913	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵) → 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
230	228, 229, 218	syl2anc 596	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵) → 𝐶 ∈ (0[,]+∞))
231	230	adantlr 728	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵) → 𝐶 ∈ (0[,]+∞))
232		simpr 490	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → 𝑝 ∈ ℝ⁺)
233	193	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ⊆ 𝐴)
234	57	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Disj 𝑥 ∈ 𝐴 𝐵)
235		disjss1 5079	. . . . . . . . . . . 12 ⊢ (𝑦 ⊆ 𝐴 → (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑥 ∈ 𝑦 𝐵))
236	233, 234, 235	sylc 66	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Disj 𝑥 ∈ 𝑦 𝐵)
237	203	3adant3 1150	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦 ∧ 𝑘 ∈ 𝐵) → 𝜑)
238	205	3adant3 1150	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦 ∧ 𝑘 ∈ 𝐵) → 𝑥 ∈ 𝐴)
239		simp3 1156	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦 ∧ 𝑘 ∈ 𝐵) → 𝑘 ∈ 𝐵)
240	237, 238, 239, 25	syl3anc 1399	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑥 ∈ 𝑦 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
241	198, 206, 236, 240, 210	sge0iunmptlemfi 47626	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))
242	214, 220	eqeltrd 2864	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘(𝑥 ∈ 𝑦 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ∈ ℝ)
243	241, 242	eqeltrd 2864	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) ∈ ℝ)
244	243	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) ∈ ℝ)
245	222, 227, 231, 232, 244	sge0ltfirpmpt 47621	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)(Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝))
246		nfv 1949	. . . . . . . 8 ⊢ Ⅎ𝑏((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺)
247		nfre1 3291	. . . . . . . 8 ⊢ Ⅎ𝑏∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_e 𝑝)
248	223	sspwd 4573	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ⊆ 𝐴 → 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵)
249	193, 248	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵)
250	249	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ⊆ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵)
251		elinel1 4101	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) → 𝑏 ∈ 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵)
252	251	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ 𝒫 ∪ 𝑥 ∈ 𝑦 𝐵)
253	250, 252	sseldd 3914	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ 𝒫 ∪ 𝑥 ∈ 𝐴 𝐵)
254		elinel2 4102	. . . . . . . . . . . . . 14 ⊢ (𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) → 𝑏 ∈ Fin)
255	254	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ Fin)
256	253, 255	elind 4100	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin))
257	256	ad4ant24 767	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin))
258	257	3adant3 1150	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin))
259	221	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ^*)
260	259	3adant3 1150	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ∈ ℝ^*)
261		nfv 1949	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin))
262	226	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → ∪ 𝑥 ∈ 𝑦 𝐵 ∈ V)
263	230	adantlr 728	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵) → 𝐶 ∈ (0[,]+∞))
264	243	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) ∈ ℝ)
265	251	elpwid 4569	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) → 𝑏 ⊆ ∪ 𝑥 ∈ 𝑦 𝐵)
266	265	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑏 ⊆ ∪ 𝑥 ∈ 𝑦 𝐵)
267	261, 262, 263, 264, 266	sge0ssrempt 47618	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) ∈ ℝ)
268	267	rexrd 11383	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) ∈ ℝ^*)
269	268	adantlr 728	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) ∈ ℝ^*)
270		rpxr 13154	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ℝ⁺ → 𝑝 ∈ ℝ^*)
271	270	ad2antlr 740	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑝 ∈ ℝ^*)
272	269, 271	xaddcld 13455	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_e 𝑝) ∈ ℝ^*)
273	272	3adant3 1150	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_e 𝑝) ∈ ℝ^*)
274		simp3 1156	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝))
275	241, 214	eqtr2d 2799	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)))
276	275	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)))
277	276	3ad2ant1 1151	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)))
278	267	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → (Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) ∈ ℝ)
279		rpre 13153	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ∈ ℝ⁺ → 𝑝 ∈ ℝ)
280	279	ad2antlr 740	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → 𝑝 ∈ ℝ)
281		rexadd 13386	. . . . . . . . . . . . . . 15 ⊢ (((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) ∈ ℝ ∧ 𝑝 ∈ ℝ) → ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_e 𝑝) = ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝))
282	278, 280, 281	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)) → ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_e 𝑝) = ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝))
283	282	3adant3 1150	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_e 𝑝) = ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝))
284	277, 283	breq12d 5119	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → (Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_e 𝑝) ↔ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)))
285	274, 284	mpbird 260	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_e 𝑝))
286	260, 273, 285	xrltled 13303	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_e 𝑝))
287		rspe 3256	. . . . . . . . . 10 ⊢ ((𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin) ∧ Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_e 𝑝)) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_e 𝑝))
288	258, 286, 287	syl2anc 596	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) ∧ 𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) ∧ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝)) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_e 𝑝))
289	288	3exp 1137	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → (𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin) → ((Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_e 𝑝))))
290	246, 247, 289	rexlimd 3273	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → (∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝑦 𝐵 ∩ Fin)(Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝑦 𝐵 ↦ 𝐶)) < ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) + 𝑝) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_e 𝑝)))
291	245, 290	mpd 16	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑝 ∈ ℝ⁺) → ∃𝑏 ∈ (𝒫 ∪ 𝑥 ∈ 𝐴 𝐵 ∩ Fin)Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ ((Σ^{^}‘(𝑘 ∈ 𝑏 ↦ 𝐶)) +_e 𝑝))
292	216, 217, 219, 221, 291	sge0gerpmpt 47615	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → Σ𝑥 ∈ 𝑦 (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
293	215, 292	eqbrtrd 5130	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
294	293	ralrimiva 3158	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
295		eqid 2763	. . . . 5 ⊢ (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))
296	179, 295	fmptd 7135	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))):𝐴⟶(0[,]+∞))
297	132, 296, 1	sge0lefi 47611	. . 3 ⊢ (𝜑 → ((Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) ↔ ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(Σ^{^}‘((𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶))) ↾ 𝑦)) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶))))
298	294, 297	mpbird 260	. 2 ⊢ (𝜑 → (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) ≤ (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)))
299	1, 2, 192, 298	xrletrid 13308	1 ⊢ (𝜑 → (Σ^{^}‘(𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ 𝐶)) = (Σ^{^}‘(𝑥 ∈ 𝐴 ↦ (Σ^{^}‘(𝑘 ∈ 𝐵 ↦ 𝐶)))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 {crab 3416 Vcvv 3454 ⦋csb 3851 ⊆ wss 3900 ∩ cin 4092 ∅c0 4281 𝒫 cpw 4560 ∪ ciun 4954 Disj wdisj 5073 class class class wbr 5106 ↦ cmpt 5189 ↾ cres 5657 ⟶wf 6551 ‘cfv 6555 (class class class)co 7440 Fincfn 8998 ℂcc 11222 ℝcr 11223 0cc0 11224 + caddc 11227 +∞cpnf 11364 ℝ^*cxr 11366 < clt 11367 ≤ cle 11368 ℝ⁺crp 13144 +_e cxad 13263 [,)cico 13502 [,]cicc 13503 Σcsu 15879 Σ^{^}csumge0 47575

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7772 ax-inf2 9666 ax-cnex 11280 ax-resscn 11281 ax-1cn 11282 ax-icn 11283 ax-addcl 11284 ax-addrcl 11285 ax-mulcl 11286 ax-mulrcl 11287 ax-mulcom 11288 ax-addass 11289 ax-mulass 11290 ax-distr 11291 ax-i2m1 11292 ax-1ne0 11293 ax-1rid 11294 ax-rnegex 11295 ax-rrecex 11296 ax-cnre 11297 ax-pre-lttri 11298 ax-pre-lttrn 11299 ax-pre-ltadd 11300 ax-pre-mulgt0 11301 ax-pre-sup 11302

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-disj 5074 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6319 df-ord 6380 df-on 6381 df-lim 6382 df-suc 6383 df-iota 6509 df-fun 6557 df-fn 6558 df-f 6559 df-f1 6560 df-fo 6561 df-f1o 6562 df-fv 6563 df-isom 6564 df-riota 7397 df-ov 7443 df-oprab 7444 df-mpo 7445 df-om 7899 df-1st 8022 df-2nd 8023 df-frecs 8324 df-wrecs 8355 df-recs 8404 df-rdg 8443 df-1o 8501 df-er 8742 df-en 8999 df-dom 9000 df-sdom 9001 df-fin 9002 df-sup 9458 df-oi 9528 df-card 10044 df-pnf 11369 df-mnf 11370 df-xr 11371 df-ltxr 11372 df-le 11373 df-sub 11567 df-neg 11568 df-div 11998 df-nn 12360 df-2 12429 df-3 12430 df-n0 12631 df-z 12718 df-uz 12990 df-rp 13145 df-xadd 13266 df-ico 13506 df-icc 13507 df-fz 13664 df-fzo 13813 df-seq 14169 df-exp 14229 df-hash 14499 df-cj 15292 df-re 15293 df-im 15294 df-sqrt 15428 df-abs 15429 df-clim 15681 df-sum 15880 df-sumge0 47576

This theorem is used by: sge0iunmpt 47631

W3C validator