esum2d - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > esum2d		Structured version Visualization version GIF version

Theorem esum2d 34718

Description: Write a double extended sum as a sum over a two-dimensional region. Note that 𝐵(𝑗) is a function of 𝑗. This can be seen as "slicing" the relation 𝐴. (Contributed by Thierry Arnoux, 17-May-2020.)

**Hypotheses**
Ref	Expression
esum2d.0	⊢ Ⅎ𝑘𝐹
esum2d.1	⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐹 = 𝐶)
esum2d.2	⊢ (𝜑 → 𝐴 ∈ 𝑉)
esum2d.3	⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)
esum2d.4	⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ (0[,]+∞))

**Assertion**
Ref	Expression
esum2d	⊢ (𝜑 → Σ^𝑗 ∈ 𝐴Σ^𝑘 ∈ 𝐵𝐶 = Σ^*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)

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

Proof of Theorem esum2d Dummy variables 𝑡 𝑎 𝑐 𝑟 𝑠 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xrltso 13263	. . . 4 ⊢ < Or ℝ^*
2	1	a1i 11	. . 3 ⊢ (𝜑 → < Or ℝ^*)
3		nfv 1947	. . . . . . . . 9 ⊢ Ⅎ𝑐𝜑
4		nfcv 2923	. . . . . . . . . 10 ⊢ Ⅎ𝑐𝑠
5		nfmpt1 5204	. . . . . . . . . . 11 ⊢ Ⅎ𝑐(𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
6	5	nfrn 5934	. . . . . . . . . 10 ⊢ Ⅎ𝑐ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
7	4, 6	nfel 2937	. . . . . . . . 9 ⊢ Ⅎ𝑐 𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
8	3, 7	nfan 1932	. . . . . . . 8 ⊢ Ⅎ𝑐(𝜑 ∧ 𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))))
9		iccssxr 13554	. . . . . . . . . . . . . 14 ⊢ (0[,]+∞) ⊆ ℝ^*
10		xrge0base 17772	. . . . . . . . . . . . . . 15 ⊢ (0[,]+∞) = (Base‘(ℝ^*_𝑠 ↾_s (0[,]+∞)))
11		xrge0cmn 21743	. . . . . . . . . . . . . . . 16 ⊢ (ℝ^*_𝑠 ↾_s (0[,]+∞)) ∈ CMnd
12	11	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → (ℝ^*_𝑠 ↾_s (0[,]+∞)) ∈ CMnd)
13		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin))
14	13	elin2d 4151	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → 𝑐 ∈ Fin)
15		simpll 779	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑧 ∈ 𝑐) → 𝜑)
16	13	elin1d 4150	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → 𝑐 ∈ 𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
17	16	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑧 ∈ 𝑐) → 𝑐 ∈ 𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
18		vex 3455	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑐 ∈ V
19	18	elpw 4561	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∈ 𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
20	17, 19	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑧 ∈ 𝑐) → 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
21		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑧 ∈ 𝑐) → 𝑧 ∈ 𝑐)
22	20, 21	sseldd 3932	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑧 ∈ 𝑐) → 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
23		nfv 1947	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗𝜑
24		nfcv 2923	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑗𝑧
25		nfiu1 4986	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑗∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
26	24, 25	nfel 2937	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
27	23, 26	nfan 1932	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
28		nfv 1947	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑘(((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵))
29		esum2d.0	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑘𝐹
30		nfcv 2923	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑘(0[,]+∞)
31	29, 30	nfel 2937	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑘 𝐹 ∈ (0[,]+∞)
32		esum2d.1	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐹 = 𝐶)
33	32	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ 𝐵) ∧ 𝑧 = ⟨𝑗, 𝑘⟩) → 𝐹 = 𝐶)
34		simp-5l 797	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ 𝐵) ∧ 𝑧 = ⟨𝑗, 𝑘⟩) → 𝜑)
35		simp-4r 796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ 𝐵) ∧ 𝑧 = ⟨𝑗, 𝑘⟩) → 𝑗 ∈ 𝐴)
36		simplr 781	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ 𝐵) ∧ 𝑧 = ⟨𝑗, 𝑘⟩) → 𝑘 ∈ 𝐵)
37		esum2d.4	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ (0[,]+∞))
38	34, 35, 36, 37	syl12anc 850	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ 𝐵) ∧ 𝑧 = ⟨𝑗, 𝑘⟩) → 𝐶 ∈ (0[,]+∞))
39	33, 38	eqeltrd 2861	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ 𝐵) ∧ 𝑧 = ⟨𝑗, 𝑘⟩) → 𝐹 ∈ (0[,]+∞))
40		elsnxp 6293	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ 𝐴 → (𝑧 ∈ ({𝑗} × 𝐵) ↔ ∃𝑘 ∈ 𝐵 𝑧 = ⟨𝑗, 𝑘⟩))
41	40	biimpa 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → ∃𝑘 ∈ 𝐵 𝑧 = ⟨𝑗, 𝑘⟩)
42	41	adantll 727	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → ∃𝑘 ∈ 𝐵 𝑧 = ⟨𝑗, 𝑘⟩)
43	28, 31, 39, 42	r19.29af2 3271	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → 𝐹 ∈ (0[,]+∞))
44		eliun 4955	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗 ∈ 𝐴 𝑧 ∈ ({𝑗} × 𝐵))
45	44	bilani 510	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) → ∃𝑗 ∈ 𝐴 𝑧 ∈ ({𝑗} × 𝐵))
46	27, 43, 45	r19.29af 3272	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) → 𝐹 ∈ (0[,]+∞))
47	15, 22, 46	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑧 ∈ 𝑐) → 𝐹 ∈ (0[,]+∞))
48	47	ralrimiva 3155	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ∀𝑧 ∈ 𝑐 𝐹 ∈ (0[,]+∞))
49	10, 12, 14, 48	gsummptcl 20174	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) ∈ (0[,]+∞))
50	9, 49	sselid 3929	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) ∈ ℝ^)
51	50	ralrimiva 3155	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) ∈ ℝ^)
52		eqid 2761	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) = (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
53	52	rnmptss 7121	. . . . . . . . . . . 12 ⊢ (∀𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) ∈ ℝ^ → ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ⊆ ℝ^)
54	51, 53	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ⊆ ℝ^)
55	54	ad3antrrr 743	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) → ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ⊆ ℝ^)
56		simpllr 788	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) → 𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))))
57	55, 56	sseldd 3932	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) → 𝑠 ∈ ℝ^*)
58		esum2d.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
59		vsnex 5393	. . . . . . . . . . . . . . 15 ⊢ {𝑗} ∈ V
60		esum2d.3	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)
61		xpexg 7762	. . . . . . . . . . . . . . 15 ⊢ (({𝑗} ∈ V ∧ 𝐵 ∈ 𝑊) → ({𝑗} × 𝐵) ∈ V)
62	59, 60, 61	sylancr 599	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ({𝑗} × 𝐵) ∈ V)
63	62	ralrimiva 3155	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V)
64		iunexg 7973	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V) → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V)
65	58, 63, 64	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V)
66	46	ralrimiva 3155	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 ∈ (0[,]+∞))
67		nfcv 2923	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑧∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
68	67	esumcl 34655	. . . . . . . . . . . 12 ⊢ ((∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V ∧ ∀𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 ∈ (0[,]+∞)) → Σ^*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 ∈ (0[,]+∞))
69	65, 66, 68	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → Σ^*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 ∈ (0[,]+∞))
70	9, 69	sselid 3929	. . . . . . . . . 10 ⊢ (𝜑 → Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 ∈ ℝ^)
71	70	ad3antrrr 743	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) → Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 ∈ ℝ^)
72		simpr 490	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) → 𝑠 = ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
73		nfv 1947	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧(𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin))
74		nfcv 2923	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧𝑐
75	73, 74, 14, 47	esumgsum 34670	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → Σ^𝑧 ∈ 𝑐𝐹 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
76	65	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V)
77	46	adantlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) → 𝐹 ∈ (0[,]+∞))
78	16, 19	sylib 221	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
79	73, 76, 77, 78	esummono 34679	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → Σ^𝑧 ∈ 𝑐𝐹 ≤ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)
80	75, 79	eqbrtrrd 5129	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) ≤ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)
81	80	adantlr 728	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) ≤ Σ^*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)
82	81	adantr 486	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) ≤ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)
83	72, 82	eqbrtrd 5127	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) → 𝑠 ≤ Σ^*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)
84		xrlenlt 11367	. . . . . . . . . 10 ⊢ ((𝑠 ∈ ℝ^* ∧ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 ∈ ℝ^) → (𝑠 ≤ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 ↔ ¬ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 < 𝑠))
85	84	biimpa 482	. . . . . . . . 9 ⊢ (((𝑠 ∈ ℝ^* ∧ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 ∈ ℝ^) ∧ 𝑠 ≤ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) → ¬ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 < 𝑠)
86	57, 71, 83, 85	syl21anc 851	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) → ¬ Σ^*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 < 𝑠)
87		ovex 7451	. . . . . . . . . 10 ⊢ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) ∈ V
88	52, 87	elrnmpti 5944	. . . . . . . . 9 ⊢ (𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ↔ ∃𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)𝑠 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
89	88	bilani 510	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) → ∃𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)𝑠 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
90	8, 86, 89	r19.29af 3272	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) → ¬ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 < 𝑠)
91	90	ralrimiva 3155	. . . . . 6 ⊢ (𝜑 → ∀𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ¬ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 < 𝑠)
92		nfv 1947	. . . . . . . . 9 ⊢ Ⅎ𝑐((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)
93		nfv 1947	. . . . . . . . . 10 ⊢ Ⅎ𝑐 𝑠 < 𝑡
94	6, 93	nfrexw 3311	. . . . . . . . 9 ⊢ Ⅎ𝑐∃𝑡 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑡
95	75	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → Σ^𝑧 ∈ 𝑐𝐹 = ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
96	95	adantlr 728	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → Σ^𝑧 ∈ 𝑐𝐹 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
97	96	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 < Σ^𝑧 ∈ 𝑐𝐹) → Σ^𝑧 ∈ 𝑐𝐹 = ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
98		simplr 781	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 < Σ^*𝑧 ∈ 𝑐𝐹) → 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin))
99	87	a1i 11	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 < Σ^𝑧 ∈ 𝑐𝐹) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) ∈ V)
100	52	elrnmpt1 5942	. . . . . . . . . . . 12 ⊢ ((𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ∧ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) ∈ V) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))))
101	98, 99, 100	syl2anc 596	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 < Σ^𝑧 ∈ 𝑐𝐹) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))))
102	97, 101	eqeltrd 2861	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 < Σ^𝑧 ∈ 𝑐𝐹) → Σ^𝑧 ∈ 𝑐𝐹 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))))
103		simpr 490	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 < Σ^𝑧 ∈ 𝑐𝐹) ∧ 𝑡 = Σ^𝑧 ∈ 𝑐𝐹) → 𝑡 = Σ^*𝑧 ∈ 𝑐𝐹)
104	103	breq2d 5115	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 < Σ^𝑧 ∈ 𝑐𝐹) ∧ 𝑡 = Σ^𝑧 ∈ 𝑐𝐹) → (𝑠 < 𝑡 ↔ 𝑠 < Σ^*𝑧 ∈ 𝑐𝐹))
105		simpr 490	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 < Σ^𝑧 ∈ 𝑐𝐹) → 𝑠 < Σ^𝑧 ∈ 𝑐𝐹)
106	102, 104, 105	rspcedvd 3579	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 < Σ^𝑧 ∈ 𝑐𝐹) → ∃𝑡 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑡)
107		nfv 1947	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(𝜑 ∧ 𝑠 ∈ ℝ^*)
108		nfcv 2923	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧𝑠
109		nfcv 2923	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧 <
110	67	nfesum1 34665	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧Σ^*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹
111	108, 109, 110	nfbr 5152	. . . . . . . . . . 11 ⊢ Ⅎ𝑧 𝑠 < Σ^*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹
112	107, 111	nfan 1932	. . . . . . . . . 10 ⊢ Ⅎ𝑧((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)
113	65	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V)
114	46	3ad2antr3 1209	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < Σ^*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → 𝐹 ∈ (0[,]+∞))
115	114	3anassrs 1381	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) → 𝐹 ∈ (0[,]+∞))
116		simplr 781	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) → 𝑠 ∈ ℝ^*)
117		simpr 490	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) → 𝑠 < Σ^*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)
118	112, 113, 115, 116, 117	esumlub 34685	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) → ∃𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)𝑠 < Σ^*𝑧 ∈ 𝑐𝐹)
119	92, 94, 106, 118	r19.29af2 3271	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) → ∃𝑡 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑡)
120	119	ex 418	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ℝ^) → (𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 → ∃𝑡 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑡))
121	120	ralrimiva 3155	. . . . . 6 ⊢ (𝜑 → ∀𝑠 ∈ ℝ^* (𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 → ∃𝑡 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑡))
122	91, 121	jca 521	. . . . 5 ⊢ (𝜑 → (∀𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ¬ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 < 𝑠 ∧ ∀𝑠 ∈ ℝ^* (𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 → ∃𝑡 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑡)))
123		simpr 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 = Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) → 𝑟 = Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)
124	123	breq1d 5113	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 = Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) → (𝑟 < 𝑠 ↔ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 < 𝑠))
125	124	notbid 321	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 = Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) → (¬ 𝑟 < 𝑠 ↔ ¬ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 < 𝑠))
126	125	ralbidv 3186	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 = Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) → (∀𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ¬ 𝑟 < 𝑠 ↔ ∀𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ¬ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 < 𝑠))
127	123	breq2d 5115	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 = Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) → (𝑠 < 𝑟 ↔ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹))
128	127	imbi1d 344	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 = Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) → ((𝑠 < 𝑟 → ∃𝑡 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑡) ↔ (𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 → ∃𝑡 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑡)))
129	128	ralbidv 3186	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 = Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) → (∀𝑠 ∈ ℝ^ (𝑠 < 𝑟 → ∃𝑡 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑡) ↔ ∀𝑠 ∈ ℝ^ (𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 → ∃𝑡 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑡)))
130	126, 129	anbi12d 644	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 = Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) → ((∀𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ¬ 𝑟 < 𝑠 ∧ ∀𝑠 ∈ ℝ^* (𝑠 < 𝑟 → ∃𝑡 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑡)) ↔ (∀𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ¬ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 < 𝑠 ∧ ∀𝑠 ∈ ℝ^ (𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 → ∃𝑡 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑡))))
131	70, 130	rspcedv 3570	. . . . 5 ⊢ (𝜑 → ((∀𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ¬ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 < 𝑠 ∧ ∀𝑠 ∈ ℝ^* (𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 → ∃𝑡 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑡)) → ∃𝑟 ∈ ℝ^* (∀𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ¬ 𝑟 < 𝑠 ∧ ∀𝑠 ∈ ℝ^ (𝑠 < 𝑟 → ∃𝑡 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑡))))
132	122, 131	mpd 16	. . . 4 ⊢ (𝜑 → ∃𝑟 ∈ ℝ^* (∀𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ¬ 𝑟 < 𝑠 ∧ ∀𝑠 ∈ ℝ^ (𝑠 < 𝑟 → ∃𝑡 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑡)))
133	2, 132	supcl 9443	. . 3 ⊢ (𝜑 → sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ) ∈ ℝ^*)
134		nfv 1947	. . . . 5 ⊢ Ⅎ𝑎𝜑
135		nfcv 2923	. . . . . 6 ⊢ Ⅎ𝑎𝑠
136		nfmpt1 5204	. . . . . . 7 ⊢ Ⅎ𝑎(𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
137	136	nfrn 5934	. . . . . 6 ⊢ Ⅎ𝑎ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
138	135, 137	nfel 2937	. . . . 5 ⊢ Ⅎ𝑎 𝑠 ∈ ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
139	134, 138	nfan 1932	. . . 4 ⊢ Ⅎ𝑎(𝜑 ∧ 𝑠 ∈ ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶))))
140		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑎 ∈ (𝒫 𝐴 ∩ Fin))
141		simpll 779	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑗 ∈ 𝑎) → 𝜑)
142	140	elin1d 4150	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑎 ∈ 𝒫 𝐴)
143		elpwi 4564	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ 𝒫 𝐴 → 𝑎 ⊆ 𝐴)
144	142, 143	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑎 ⊆ 𝐴)
145	144	sselda 3931	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑗 ∈ 𝑎) → 𝑗 ∈ 𝐴)
146	141, 145, 60	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑗 ∈ 𝑎) → 𝐵 ∈ 𝑊)
147	141	adantrr 730	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑗 ∈ 𝑎 ∧ 𝑘 ∈ 𝐵)) → 𝜑)
148	145	adantrr 730	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑗 ∈ 𝑎 ∧ 𝑘 ∈ 𝐵)) → 𝑗 ∈ 𝐴)
149		simprr 785	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑗 ∈ 𝑎 ∧ 𝑘 ∈ 𝐵)) → 𝑘 ∈ 𝐵)
150	147, 148, 149, 37	syl12anc 850	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑗 ∈ 𝑎 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ (0[,]+∞))
151	140	elin2d 4151	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑎 ∈ Fin)
152	29, 32, 140, 146, 150, 151	esum2dlem 34717	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → Σ^𝑗 ∈ 𝑎Σ^𝑘 ∈ 𝐵𝐶 = Σ^*𝑧 ∈ ∪ 𝑗 ∈ 𝑎 ({𝑗} × 𝐵)𝐹)
153		nfv 1947	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin))
154		nfcv 2923	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗𝑎
155	37	anassrs 473	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
156	155	ralrimiva 3155	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ∀𝑘 ∈ 𝐵 𝐶 ∈ (0[,]+∞))
157		nfcv 2923	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘𝐵
158	157	esumcl 34655	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ 𝑊 ∧ ∀𝑘 ∈ 𝐵 𝐶 ∈ (0[,]+∞)) → Σ^*𝑘 ∈ 𝐵𝐶 ∈ (0[,]+∞))
159	60, 156, 158	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → Σ^*𝑘 ∈ 𝐵𝐶 ∈ (0[,]+∞))
160	141, 145, 159	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑗 ∈ 𝑎) → Σ^*𝑘 ∈ 𝐵𝐶 ∈ (0[,]+∞))
161	153, 154, 151, 160	esumgsum 34670	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → Σ^𝑗 ∈ 𝑎Σ^𝑘 ∈ 𝐵𝐶 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
162	152, 161	eqtr3d 2798	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝑎 ({𝑗} × 𝐵)𝐹 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^*𝑘 ∈ 𝐵𝐶)))
163		nfv 1947	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin))
164	65	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V)
165	46	adantlr 728	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) → 𝐹 ∈ (0[,]+∞))
166		iunss1 4966	. . . . . . . . . . . 12 ⊢ (𝑎 ⊆ 𝐴 → ∪ 𝑗 ∈ 𝑎 ({𝑗} × 𝐵) ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
167	144, 166	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ∪ 𝑗 ∈ 𝑎 ({𝑗} × 𝐵) ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
168	163, 164, 165, 167	esummono 34679	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝑎 ({𝑗} × 𝐵)𝐹 ≤ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)
169	162, 168	eqbrtrrd 5129	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)) ≤ Σ^*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)
170	11	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → (ℝ^*_𝑠 ↾_s (0[,]+∞)) ∈ CMnd)
171	160	ralrimiva 3155	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ∀𝑗 ∈ 𝑎 Σ^*𝑘 ∈ 𝐵𝐶 ∈ (0[,]+∞))
172	10, 170, 151, 171	gsummptcl 20174	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)) ∈ (0[,]+∞))
173	9, 172	sselid 3929	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)) ∈ ℝ^*)
174	70	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 ∈ ℝ^)
175		xrlenlt 11367	. . . . . . . . . 10 ⊢ ((((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)) ∈ ℝ^* ∧ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 ∈ ℝ^) → (((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)) ≤ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 ↔ ¬ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶))))
176	173, 174, 175	syl2anc 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → (((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)) ≤ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 ↔ ¬ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶))))
177	169, 176	mpbid 235	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ¬ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^*𝑘 ∈ 𝐵𝐶)))
178		nfv 1947	. . . . . . . . . . 11 ⊢ Ⅎ𝑧𝜑
179		eqidd 2762	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
180	178, 67, 65, 46, 179	esumval 34671	. . . . . . . . . 10 ⊢ (𝜑 → Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 = sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^*, < ))
181	180	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 = sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^*, < ))
182	181	breq1d 5113	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → (Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)) ↔ sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ) < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^*𝑘 ∈ 𝐵𝐶))))
183	177, 182	mtbid 327	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ¬ sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ) < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
184	183	adantlr 728	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))) ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ¬ sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ) < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
185	184	adantr 486	. . . . 5 ⊢ ((((𝜑 ∧ 𝑠 ∈ ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))) ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑠 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶))) → ¬ sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ) < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
186		simpr 490	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 ∈ ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))) ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑠 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶))) → 𝑠 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
187	186	breq2d 5115	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 ∈ ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))) ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑠 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶))) → (sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ) < 𝑠 ↔ sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ) < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶))))
188	187	notbid 321	. . . . 5 ⊢ ((((𝜑 ∧ 𝑠 ∈ ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))) ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑠 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶))) → (¬ sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ) < 𝑠 ↔ ¬ sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ) < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶))))
189	185, 188	mpbird 260	. . . 4 ⊢ ((((𝜑 ∧ 𝑠 ∈ ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))) ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑠 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶))) → ¬ sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ) < 𝑠)
190		eqid 2761	. . . . . 6 ⊢ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶))) = (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
191		ovex 7451	. . . . . 6 ⊢ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)) ∈ V
192	190, 191	elrnmpti 5944	. . . . 5 ⊢ (𝑠 ∈ ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶))) ↔ ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑠 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
193	192	bilani 510	. . . 4 ⊢ ((𝜑 ∧ 𝑠 ∈ ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑠 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
194	139, 189, 193	r19.29af 3272	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))) → ¬ sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ) < 𝑠)
195	4	nfel1 2939	. . . . . . . . 9 ⊢ Ⅎ𝑐 𝑠 ∈ ℝ^*
196		nfcv 2923	. . . . . . . . . 10 ⊢ Ⅎ𝑐 <
197		nfcv 2923	. . . . . . . . . . 11 ⊢ Ⅎ𝑐ℝ^*
198	6, 197, 196	nfsup 9436	. . . . . . . . . 10 ⊢ Ⅎ𝑐sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < )
199	4, 196, 198	nfbr 5152	. . . . . . . . 9 ⊢ Ⅎ𝑐 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < )
200	195, 199	nfan 1932	. . . . . . . 8 ⊢ Ⅎ𝑐(𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))
201	3, 200	nfan 1932	. . . . . . 7 ⊢ Ⅎ𝑐(𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < )))
202		nfcv 2923	. . . . . . . 8 ⊢ Ⅎ𝑐𝑢
203	202, 6	nfel 2937	. . . . . . 7 ⊢ Ⅎ𝑐 𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
204	201, 203	nfan 1932	. . . . . 6 ⊢ Ⅎ𝑐((𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))) ∧ 𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))))
205		nfv 1947	. . . . . 6 ⊢ Ⅎ𝑐 𝑠 < 𝑢
206	204, 205	nfan 1932	. . . . 5 ⊢ Ⅎ𝑐(((𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))) ∧ 𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑠 < 𝑢)
207		simp-5l 797	. . . . . . . 8 ⊢ ((((((𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))) ∧ 𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑠 < 𝑢) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑢 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) → 𝜑)
208		simpr1l 1249	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < )) ∧ 𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ (𝑠 < 𝑢 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ∧ 𝑢 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))))) → 𝑠 ∈ ℝ^*)
209	208	3anassrs 1381	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))) ∧ 𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ (𝑠 < 𝑢 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ∧ 𝑢 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) → 𝑠 ∈ ℝ^*)
210	209	3anassrs 1381	. . . . . . . 8 ⊢ ((((((𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))) ∧ 𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑠 < 𝑢) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑢 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) → 𝑠 ∈ ℝ^*)
211	207, 210	jca 521	. . . . . . 7 ⊢ ((((((𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))) ∧ 𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑠 < 𝑢) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑢 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) → (𝜑 ∧ 𝑠 ∈ ℝ^*))
212		simpr1r 1250	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < )) ∧ 𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ (𝑠 < 𝑢 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ∧ 𝑢 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))))) → 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))
213	212	3anassrs 1381	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))) ∧ 𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ (𝑠 < 𝑢 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ∧ 𝑢 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) → 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))
214	213	3anassrs 1381	. . . . . . 7 ⊢ ((((((𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))) ∧ 𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑠 < 𝑢) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑢 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) → 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))
215	211, 214	jca 521	. . . . . 6 ⊢ ((((((𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))) ∧ 𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑠 < 𝑢) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑢 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) → ((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^*, < )))
216		simpllr 788	. . . . . . 7 ⊢ ((((((𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))) ∧ 𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑠 < 𝑢) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑢 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) → 𝑠 < 𝑢)
217		simpr 490	. . . . . . 7 ⊢ ((((((𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))) ∧ 𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑠 < 𝑢) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑢 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) → 𝑢 = ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
218	216, 217	breqtrd 5131	. . . . . 6 ⊢ ((((((𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))) ∧ 𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑠 < 𝑢) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑢 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) → 𝑠 < ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
219		simplr 781	. . . . . 6 ⊢ ((((((𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))) ∧ 𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑠 < 𝑢) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑢 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) → 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin))
220		simpr 490	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin))
221	220	elin1d 4150	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → 𝑐 ∈ 𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
222		elpwi 4564	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
223		dmss 5884	. . . . . . . . . . . . . 14 ⊢ (𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → dom 𝑐 ⊆ dom ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
224		dmiun 5895	. . . . . . . . . . . . . 14 ⊢ dom ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) = ∪ 𝑗 ∈ 𝐴 dom ({𝑗} × 𝐵)
225	223, 224	sseqtrdi 3971	. . . . . . . . . . . . 13 ⊢ (𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → dom 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 dom ({𝑗} × 𝐵))
226		dmxpss 6163	. . . . . . . . . . . . . . . . 17 ⊢ dom ({𝑗} × 𝐵) ⊆ {𝑗}
227	226	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ 𝐴 → dom ({𝑗} × 𝐵) ⊆ {𝑗})
228		snssi 4746	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ 𝐴 → {𝑗} ⊆ 𝐴)
229	227, 228	sstrd 3941	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ 𝐴 → dom ({𝑗} × 𝐵) ⊆ 𝐴)
230	229	rgen 3079	. . . . . . . . . . . . . 14 ⊢ ∀𝑗 ∈ 𝐴 dom ({𝑗} × 𝐵) ⊆ 𝐴
231		iunss 5003	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑗 ∈ 𝐴 dom ({𝑗} × 𝐵) ⊆ 𝐴 ↔ ∀𝑗 ∈ 𝐴 dom ({𝑗} × 𝐵) ⊆ 𝐴)
232	230, 231	mpbir 234	. . . . . . . . . . . . 13 ⊢ ∪ 𝑗 ∈ 𝐴 dom ({𝑗} × 𝐵) ⊆ 𝐴
233	225, 232	sstrdi 3943	. . . . . . . . . . . 12 ⊢ (𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → dom 𝑐 ⊆ 𝐴)
234	18	dmex 7919	. . . . . . . . . . . . 13 ⊢ dom 𝑐 ∈ V
235	234	elpw 4561	. . . . . . . . . . . 12 ⊢ (dom 𝑐 ∈ 𝒫 𝐴 ↔ dom 𝑐 ⊆ 𝐴)
236	233, 235	sylibr 237	. . . . . . . . . . 11 ⊢ (𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → dom 𝑐 ∈ 𝒫 𝐴)
237	221, 222, 236	3syl 19	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → dom 𝑐 ∈ 𝒫 𝐴)
238	220	elin2d 4151	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → 𝑐 ∈ Fin)
239		dmfi 9317	. . . . . . . . . . 11 ⊢ (𝑐 ∈ Fin → dom 𝑐 ∈ Fin)
240	238, 239	syl 18	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → dom 𝑐 ∈ Fin)
241	237, 240	elind 4146	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → dom 𝑐 ∈ (𝒫 𝐴 ∩ Fin))
242		ovex 7451	. . . . . . . . . 10 ⊢ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶)) ∈ V
243	242	a1i 11	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶)) ∈ V)
244		mpteq1 5194	. . . . . . . . . . 11 ⊢ (𝑎 = dom 𝑐 → (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶) = (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶))
245	244	oveq2d 7434	. . . . . . . . . 10 ⊢ (𝑎 = dom 𝑐 → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)) = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
246	190, 245	elrnmpt1s 5941	. . . . . . . . 9 ⊢ ((dom 𝑐 ∈ (𝒫 𝐴 ∩ Fin) ∧ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶)) ∈ V) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶)) ∈ ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶))))
247	241, 243, 246	syl2anc 596	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶)) ∈ ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶))))
248		simpr 490	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑡 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶))) → 𝑡 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
249	248	breq2d 5115	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑡 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶))) → (𝑠 < 𝑡 ↔ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶))))
250		simpllr 788	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → 𝑠 ∈ ℝ^*)
251	11	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → (ℝ^*_𝑠 ↾_s (0[,]+∞)) ∈ CMnd)
252		nfcv 2923	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧(ℝ^*_𝑠 ↾_s (0[,]+∞))
253		nfcv 2923	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧 Σ_g
254		nfmpt1 5204	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧(𝑧 ∈ 𝑐 ↦ 𝐹)
255	252, 253, 254	nfov 7448	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))
256	108, 109, 255	nfbr 5152	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧 𝑠 < ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))
257	107, 256	nfan 1932	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑧((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
258		nfv 1947	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑧 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)
259	257, 258	nfan 1932	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧(((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin))
260		simp-4l 795	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑧 ∈ 𝑐) → 𝜑)
261	221, 222	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
262	261	sselda 3931	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑧 ∈ 𝑐) → 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
263	260, 262, 46	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑧 ∈ 𝑐) → 𝐹 ∈ (0[,]+∞))
264	263	ex 418	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → (𝑧 ∈ 𝑐 → 𝐹 ∈ (0[,]+∞)))
265	259, 264	ralrimi 3261	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ∀𝑧 ∈ 𝑐 𝐹 ∈ (0[,]+∞))
266	10, 251, 238, 265	gsummptcl 20174	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) ∈ (0[,]+∞))
267	9, 266	sselid 3929	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) ∈ ℝ^)
268		nfv 1947	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
269		nfcv 2923	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗𝑐
270	25	nfpw 4576	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
271		nfcv 2923	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗Fin
272	270, 271	nfin 4170	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗(𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)
273	269, 272	nfel 2937	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)
274	268, 273	nfan 1932	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗(((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin))
275		simpll 779	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → 𝜑)
276	78, 233	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → dom 𝑐 ⊆ 𝐴)
277	276	sselda 3931	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → 𝑗 ∈ 𝐴)
278	275, 277, 159	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → Σ^*𝑘 ∈ 𝐵𝐶 ∈ (0[,]+∞))
279	278	adantllr 732	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → Σ^𝑘 ∈ 𝐵𝐶 ∈ (0[,]+∞))
280	279	adantllr 732	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → Σ^*𝑘 ∈ 𝐵𝐶 ∈ (0[,]+∞))
281	280	ex 418	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → (𝑗 ∈ dom 𝑐 → Σ^*𝑘 ∈ 𝐵𝐶 ∈ (0[,]+∞)))
282	274, 281	ralrimi 3261	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ∀𝑗 ∈ dom 𝑐Σ^*𝑘 ∈ 𝐵𝐶 ∈ (0[,]+∞))
283	10, 251, 240, 282	gsummptcl 20174	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶)) ∈ (0[,]+∞))
284	9, 283	sselid 3929	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶)) ∈ ℝ^*)
285		simplr 781	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → 𝑠 < ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
286	23, 273	nfan 1932	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin))
287		id 23	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
288		xpss 5667	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑗} × 𝐵) ⊆ (V × V)
289	288	rgenw 3081	. . . . . . . . . . . . . . . . . 18 ⊢ ∀𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ⊆ (V × V)
290		iunss 5003	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ⊆ (V × V) ↔ ∀𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ⊆ (V × V))
291	289, 290	mpbir 234	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ⊆ (V × V)
292	291	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ⊆ (V × V))
293	287, 292	sstrd 3941	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → 𝑐 ⊆ (V × V))
294	78, 293	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → 𝑐 ⊆ (V × V))
295		df-rel 5658	. . . . . . . . . . . . . 14 ⊢ (Rel 𝑐 ↔ 𝑐 ⊆ (V × V))
296	294, 295	sylibr 237	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → Rel 𝑐)
297	29, 286, 10, 32, 296, 14, 12, 47	gsummpt2d 33603	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑘 ∈ (𝑐 “ {𝑗}) ↦ 𝐶)))))
298		nfcv 2923	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗dom 𝑐
299	234	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → dom 𝑐 ∈ V)
300	275	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) ∧ 𝑘 ∈ (𝑐 “ {𝑗})) → 𝜑)
301	277	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) ∧ 𝑘 ∈ (𝑐 “ {𝑗})) → 𝑗 ∈ 𝐴)
302	78	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
303		imass1 6054	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → (𝑐 “ {𝑗}) ⊆ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) “ {𝑗}))
304	302, 303	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → (𝑐 “ {𝑗}) ⊆ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) “ {𝑗}))
305	58, 60	iunsnima 33205	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) “ {𝑗}) = 𝐵)
306	275, 277, 305	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) “ {𝑗}) = 𝐵)
307	304, 306	sseqtrd 3967	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → (𝑐 “ {𝑗}) ⊆ 𝐵)
308	307	sselda 3931	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) ∧ 𝑘 ∈ (𝑐 “ {𝑗})) → 𝑘 ∈ 𝐵)
309	300, 301, 308, 37	syl12anc 850	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) ∧ 𝑘 ∈ (𝑐 “ {𝑗})) → 𝐶 ∈ (0[,]+∞))
310	309	ralrimiva 3155	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → ∀𝑘 ∈ (𝑐 “ {𝑗})𝐶 ∈ (0[,]+∞))
311		imaexg 7923	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ V → (𝑐 “ {𝑗}) ∈ V)
312	18, 311	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 “ {𝑗}) ∈ V
313		nfcv 2923	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘(𝑐 “ {𝑗})
314	313	esumcl 34655	. . . . . . . . . . . . . . . 16 ⊢ (((𝑐 “ {𝑗}) ∈ V ∧ ∀𝑘 ∈ (𝑐 “ {𝑗})𝐶 ∈ (0[,]+∞)) → Σ^*𝑘 ∈ (𝑐 “ {𝑗})𝐶 ∈ (0[,]+∞))
315	312, 314	mpan 703	. . . . . . . . . . . . . . 15 ⊢ (∀𝑘 ∈ (𝑐 “ {𝑗})𝐶 ∈ (0[,]+∞) → Σ^*𝑘 ∈ (𝑐 “ {𝑗})𝐶 ∈ (0[,]+∞))
316	310, 315	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → Σ^*𝑘 ∈ (𝑐 “ {𝑗})𝐶 ∈ (0[,]+∞))
317		nfv 1947	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐)
318	275, 277, 60	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → 𝐵 ∈ 𝑊)
319	275	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) ∧ 𝑘 ∈ 𝐵) → 𝜑)
320	277	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) ∧ 𝑘 ∈ 𝐵) → 𝑗 ∈ 𝐴)
321		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) ∧ 𝑘 ∈ 𝐵) → 𝑘 ∈ 𝐵)
322	319, 320, 321, 37	syl12anc 850	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
323	317, 318, 322, 307	esummono 34679	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → Σ^𝑘 ∈ (𝑐 “ {𝑗})𝐶 ≤ Σ^𝑘 ∈ 𝐵𝐶)
324	286, 298, 299, 316, 278, 323	esumlef 34687	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → Σ^𝑗 ∈ dom 𝑐Σ^𝑘 ∈ (𝑐 “ {𝑗})𝐶 ≤ Σ^𝑗 ∈ dom 𝑐Σ^𝑘 ∈ 𝐵𝐶)
325	14, 239	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → dom 𝑐 ∈ Fin)
326	286, 298, 325, 316	esumgsum 34670	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → Σ^𝑗 ∈ dom 𝑐Σ^𝑘 ∈ (𝑐 “ {𝑗})𝐶 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ (𝑐 “ {𝑗})𝐶)))
327	14	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → 𝑐 ∈ Fin)
328		imafi2 9343	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ Fin → (𝑐 “ {𝑗}) ∈ Fin)
329	327, 328	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → (𝑐 “ {𝑗}) ∈ Fin)
330	317, 313, 329, 309	esumgsum 34670	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → Σ^𝑘 ∈ (𝑐 “ {𝑗})𝐶 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑘 ∈ (𝑐 “ {𝑗}) ↦ 𝐶)))
331	286, 330	mpteq2da 5197	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ (𝑐 “ {𝑗})𝐶) = (𝑗 ∈ dom 𝑐 ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑘 ∈ (𝑐 “ {𝑗}) ↦ 𝐶))))
332	331	oveq2d 7434	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ (𝑐 “ {𝑗})𝐶)) = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑘 ∈ (𝑐 “ {𝑗}) ↦ 𝐶)))))
333	326, 332	eqtrd 2796	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → Σ^𝑗 ∈ dom 𝑐Σ^𝑘 ∈ (𝑐 “ {𝑗})𝐶 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑘 ∈ (𝑐 “ {𝑗}) ↦ 𝐶)))))
334	286, 298, 325, 278	esumgsum 34670	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → Σ^𝑗 ∈ dom 𝑐Σ^𝑘 ∈ 𝐵𝐶 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
335	324, 333, 334	3brtr3d 5136	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑘 ∈ (𝑐 “ {𝑗}) ↦ 𝐶)))) ≤ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
336	297, 335	eqbrtrd 5127	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) ≤ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^*𝑘 ∈ 𝐵𝐶)))
337	336	adantlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) ≤ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
338	337	adantlr 728	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) ≤ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^*𝑘 ∈ 𝐵𝐶)))
339	250, 267, 284, 285, 338	xrltletrd 13283	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
340	247, 249, 339	rspcedvd 3579	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ∃𝑡 ∈ ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))𝑠 < 𝑡)
341	340	adantllr 732	. . . . . 6 ⊢ (((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < )) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ∃𝑡 ∈ ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))𝑠 < 𝑡)
342	215, 218, 219, 341	syl21anc 851	. . . . 5 ⊢ ((((((𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))) ∧ 𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑠 < 𝑢) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑢 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) → ∃𝑡 ∈ ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))𝑠 < 𝑡)
343	52, 87	elrnmpti 5944	. . . . . . 7 ⊢ (𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ↔ ∃𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)𝑢 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
344	343	biimpi 219	. . . . . 6 ⊢ (𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) → ∃𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)𝑢 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
345	344	ad2antlr 740	. . . . 5 ⊢ ((((𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))) ∧ 𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑠 < 𝑢) → ∃𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)𝑢 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
346	206, 342, 345	r19.29af 3272	. . . 4 ⊢ ((((𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))) ∧ 𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑠 < 𝑢) → ∃𝑡 ∈ ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^*𝑘 ∈ 𝐵𝐶)))𝑠 < 𝑡)
347	2, 132	suplub 9445	. . . . . 6 ⊢ (𝜑 → ((𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < )) → ∃𝑡 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑡))
348	347	imp 412	. . . . 5 ⊢ ((𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))) → ∃𝑡 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑡)
349		breq2 5107	. . . . . 6 ⊢ (𝑡 = 𝑢 → (𝑠 < 𝑡 ↔ 𝑠 < 𝑢))
350	349	cbvrexvw 3242	. . . . 5 ⊢ (∃𝑡 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑡 ↔ ∃𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑢)
351	348, 350	sylib 221	. . . 4 ⊢ ((𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))) → ∃𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑢)
352	346, 351	r19.29a 3171	. . 3 ⊢ ((𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))) → ∃𝑡 ∈ ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))𝑠 < 𝑡)
353	2, 133, 194, 352	eqsupd 9442	. 2 ⊢ (𝜑 → sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶))), ℝ^, < ) = sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^*, < ))
354		nfcv 2923	. . 3 ⊢ Ⅎ𝑗𝐴
355		eqidd 2762	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)) = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
356	23, 354, 58, 159, 355	esumval 34671	. 2 ⊢ (𝜑 → Σ^𝑗 ∈ 𝐴Σ^𝑘 ∈ 𝐵𝐶 = sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶))), ℝ^*, < ))
357	353, 356, 180	3eqtr4d 2806	1 ⊢ (𝜑 → Σ^𝑗 ∈ 𝐴Σ^𝑘 ∈ 𝐵𝐶 = Σ^*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 Ⅎwnfc 2908 ∀wral 3077 ∃wrex 3087 Vcvv 3451 ∩ cin 3898 ⊆ wss 3899 𝒫 cpw 4557 {csn 4584 ⟨cop 4590 ∪ ciun 4951 class class class wbr 5103 ↦ cmpt 5186 Or wor 5558 × cxp 5649 dom cdm 5651 ran crn 5652 “ cima 5654 Rel wrel 5656 (class class class)co 7418 Fincfn 8966 supcsup 9425 0cc0 11193 +∞cpnf 11333 ℝ^*cxr 11335 < clt 11336 ≤ cle 11337 [,]cicc 13472 ↾_s cress 17401 Σ_g cgsu 17604 ℝ^*_𝑠cxrs 17665 CMndccmn 19987 Σ^*cesum 34652

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 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-inf2 9635 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270 ax-pre-sup 11271 ax-addf 11272 ax-mulf 11273

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 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-of 7691 df-om 7876 df-1st 7999 df-2nd 8000 df-supp 8171 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-1o 8469 df-2o 8470 df-er 8710 df-map 8842 df-pm 8843 df-ixp 8919 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-fsupp 9347 df-fi 9396 df-sup 9427 df-inf 9428 df-oi 9497 df-card 10013 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-div 11967 df-nn 12329 df-2 12398 df-3 12399 df-4 12400 df-5 12401 df-6 12402 df-7 12403 df-8 12404 df-9 12405 df-n0 12600 df-z 12687 df-dec 12808 df-uz 12959 df-q 13069 df-rp 13114 df-xneg 13234 df-xadd 13235 df-xmul 13236 df-ioo 13473 df-ioc 13474 df-ico 13475 df-icc 13476 df-fz 13633 df-fzo 13782 df-fl 13925 df-mod 14003 df-seq 14138 df-exp 14198 df-fac 14411 df-bc 14440 df-hash 14468 df-shft 15213 df-cj 15259 df-re 15260 df-im 15261 df-sqrt 15395 df-abs 15396 df-limsup 15631 df-clim 15648 df-rlim 15649 df-sum 15847 df-ef 16226 df-sin 16228 df-cos 16229 df-pi 16231 df-struct 17318 df-sets 17335 df-slot 17353 df-ndx 17365 df-base 17381 df-ress 17402 df-plusg 17434 df-mulr 17435 df-starv 17436 df-sca 17437 df-vsca 17438 df-ip 17439 df-tset 17440 df-ple 17441 df-ds 17443 df-unif 17444 df-hom 17445 df-cco 17446 df-rest 17586 df-topn 17587 df-0g 17605 df-gsum 17606 df-topgen 17607 df-pt 17608 df-prds 17611 df-ordt 17666 df-xrs 17667 df-qtop 17672 df-imas 17673 df-xps 17675 df-mre 17749 df-mrc 17750 df-acs 17752 df-ps 18733 df-tsr 18734 df-plusf 18808 df-mgm 18809 df-sgrp 18901 df-mnd 18917 df-mhm 18971 df-submnd 18972 df-grp 19140 df-minusg 19141 df-sbg 19142 df-mulg 19271 df-subg 19326 df-cntz 19524 df-cmn 19989 df-abl 19990 df-mgp 20354 df-rng 20368 df-ur 20401 df-ring 20454 df-cring 20455 df-subrng 20791 df-subrg 20815 df-abv 21059 df-lmod 21130 df-scaf 21131 df-sra 21441 df-rgmod 21442 df-psmet 21663 df-xmet 21664 df-met 21665 df-bl 21666 df-mopn 21667 df-fbas 21668 df-fg 21669 df-cnfld 21672 df-top 23205 df-topon 23222 df-topsp 23244 df-bases 23257 df-cld 23330 df-ntr 23331 df-cls 23332 df-nei 23409 df-lp 23447 df-perf 23448 df-cn 23538 df-cnp 23539 df-haus 23626 df-tx 23874 df-hmeo 24067 df-fil 24158 df-fm 24250 df-flim 24251 df-flf 24252 df-tmd 24384 df-tgp 24385 df-tsms 24439 df-trg 24472 df-xms 24632 df-ms 24633 df-tms 24634 df-nm 24894 df-ngp 24895 df-nrg 24897 df-nlm 24898 df-ii 25191 df-cncf 25192 df-limc 26179 df-dv 26180 df-log 26877 df-esum 34653

This theorem is used by: esumiun 34719

W3C validator