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 34768

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 13271	. . . 4 ⊢ < Or ℝ^*
2	1	a1i 11	. . 3 ⊢ (𝜑 → < Or ℝ^*)
3		nfv 1946	. . . . . . . . 9 ⊢ Ⅎ𝑐𝜑
4		nfcv 2922	. . . . . . . . . 10 ⊢ Ⅎ𝑐𝑠
5		nfmpt1 5203	. . . . . . . . . . 11 ⊢ Ⅎ𝑐(𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
6	5	nfrn 5933	. . . . . . . . . 10 ⊢ Ⅎ𝑐ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
7	4, 6	nfel 2936	. . . . . . . . 9 ⊢ Ⅎ𝑐 𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
8	3, 7	nfan 1931	. . . . . . . 8 ⊢ Ⅎ𝑐(𝜑 ∧ 𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))))
9		iccssxr 13562	. . . . . . . . . . . . . 14 ⊢ (0[,]+∞) ⊆ ℝ^*
10		xrge0base 17780	. . . . . . . . . . . . . . 15 ⊢ (0[,]+∞) = (Base‘(ℝ^*_𝑠 ↾_s (0[,]+∞)))
11		xrge0cmn 21751	. . . . . . . . . . . . . . . 16 ⊢ (ℝ^*_𝑠 ↾_s (0[,]+∞)) ∈ CMnd
12	11	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → (ℝ^*_𝑠 ↾_s (0[,]+∞)) ∈ CMnd)
13		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin))
14	13	elin2d 4102	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → 𝑐 ∈ Fin)
15		simpll 779	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑧 ∈ 𝑐) → 𝜑)
16	13	elin1d 4101	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → 𝑐 ∈ 𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
17	16	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑧 ∈ 𝑐) → 𝑐 ∈ 𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
18		vex 3454	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑐 ∈ V
19	18	elpw 4560	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∈ 𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
20	17, 19	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑧 ∈ 𝑐) → 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
21		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑧 ∈ 𝑐) → 𝑧 ∈ 𝑐)
22	20, 21	sseldd 3909	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑧 ∈ 𝑐) → 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
23		nfv 1946	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗𝜑
24		nfcv 2922	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑗𝑧
25		nfiu1 4985	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑗∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
26	24, 25	nfel 2936	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑗 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
27	23, 26	nfan 1931	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
28		nfv 1946	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑘(((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵))
29		esum2d.0	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑘𝐹
30		nfcv 2922	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑘(0[,]+∞)
31	29, 30	nfel 2936	. . . . . . . . . . . . . . . . . . 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 2860	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ 𝐵) ∧ 𝑧 = ⟨𝑗, 𝑘⟩) → 𝐹 ∈ (0[,]+∞))
40		elsnxp 6294	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ 𝐴 → (𝑧 ∈ ({𝑗} × 𝐵) ↔ ∃𝑘 ∈ 𝐵 𝑧 = ⟨𝑗, 𝑘⟩))
41	40	biimpa 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑗 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → ∃𝑘 ∈ 𝐵 𝑧 = ⟨𝑗, 𝑘⟩)
42	41	adantll 727	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → ∃𝑘 ∈ 𝐵 𝑧 = ⟨𝑗, 𝑘⟩)
43	28, 31, 39, 42	r19.29af2 3270	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → 𝐹 ∈ (0[,]+∞))
44		eliun 4954	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗 ∈ 𝐴 𝑧 ∈ ({𝑗} × 𝐵))
45	44	bilani 510	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) → ∃𝑗 ∈ 𝐴 𝑧 ∈ ({𝑗} × 𝐵))
46	27, 43, 45	r19.29af 3271	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) → 𝐹 ∈ (0[,]+∞))
47	15, 22, 46	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑧 ∈ 𝑐) → 𝐹 ∈ (0[,]+∞))
48	47	ralrimiva 3154	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ∀𝑧 ∈ 𝑐 𝐹 ∈ (0[,]+∞))
49	10, 12, 14, 48	gsummptcl 20182	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) ∈ (0[,]+∞))
50	9, 49	sselid 3906	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) ∈ ℝ^)
51	50	ralrimiva 3154	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) ∈ ℝ^)
52		eqid 2760	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) = (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
53	52	rnmptss 7123	. . . . . . . . . . . 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 3909	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) → 𝑠 ∈ ℝ^*)
58		esum2d.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
59		vsnex 5392	. . . . . . . . . . . . . . 15 ⊢ {𝑗} ∈ V
60		esum2d.3	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)
61		xpexg 7764	. . . . . . . . . . . . . . 15 ⊢ (({𝑗} ∈ V ∧ 𝐵 ∈ 𝑊) → ({𝑗} × 𝐵) ∈ V)
62	59, 60, 61	sylancr 599	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ({𝑗} × 𝐵) ∈ V)
63	62	ralrimiva 3154	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V)
64		iunexg 7975	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V) → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V)
65	58, 63, 64	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝜑 → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V)
66	46	ralrimiva 3154	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 ∈ (0[,]+∞))
67		nfcv 2922	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑧∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
68	67	esumcl 34705	. . . . . . . . . . . 12 ⊢ ((∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V ∧ ∀𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 ∈ (0[,]+∞)) → Σ^*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 ∈ (0[,]+∞))
69	65, 66, 68	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → Σ^*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 ∈ (0[,]+∞))
70	9, 69	sselid 3906	. . . . . . . . . 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 1946	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧(𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin))
74		nfcv 2922	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧𝑐
75	73, 74, 14, 47	esumgsum 34720	. . . . . . . . . . . . 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 34729	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → Σ^𝑧 ∈ 𝑐𝐹 ≤ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)
80	75, 79	eqbrtrrd 5128	. . . . . . . . . . . 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 5126	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) → 𝑠 ≤ Σ^*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)
84		xrlenlt 11375	. . . . . . . . . 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 7453	. . . . . . . . . 10 ⊢ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) ∈ V
88	52, 87	elrnmpti 5943	. . . . . . . . 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 3271	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) → ¬ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 < 𝑠)
91	90	ralrimiva 3154	. . . . . 6 ⊢ (𝜑 → ∀𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ¬ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 < 𝑠)
92		nfv 1946	. . . . . . . . 9 ⊢ Ⅎ𝑐((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)
93		nfv 1946	. . . . . . . . . 10 ⊢ Ⅎ𝑐 𝑠 < 𝑡
94	6, 93	nfrexw 3310	. . . . . . . . 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 5941	. . . . . . . . . . . 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 2860	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 < Σ^𝑧 ∈ 𝑐𝐹) → Σ^𝑧 ∈ 𝑐𝐹 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))))
103		simpr 490	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 < Σ^𝑧 ∈ 𝑐𝐹) ∧ 𝑡 = Σ^𝑧 ∈ 𝑐𝐹) → 𝑡 = Σ^*𝑧 ∈ 𝑐𝐹)
104	103	breq2d 5114	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 < Σ^𝑧 ∈ 𝑐𝐹) ∧ 𝑡 = Σ^𝑧 ∈ 𝑐𝐹) → (𝑠 < 𝑡 ↔ 𝑠 < Σ^*𝑧 ∈ 𝑐𝐹))
105		simpr 490	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 < Σ^𝑧 ∈ 𝑐𝐹) → 𝑠 < Σ^𝑧 ∈ 𝑐𝐹)
106	102, 104, 105	rspcedvd 3578	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑠 < Σ^𝑧 ∈ 𝑐𝐹) → ∃𝑡 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑡)
107		nfv 1946	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(𝜑 ∧ 𝑠 ∈ ℝ^*)
108		nfcv 2922	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧𝑠
109		nfcv 2922	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧 <
110	67	nfesum1 34715	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧Σ^*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹
111	108, 109, 110	nfbr 5151	. . . . . . . . . . 11 ⊢ Ⅎ𝑧 𝑠 < Σ^*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹
112	107, 111	nfan 1931	. . . . . . . . . 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 34735	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) → ∃𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)𝑠 < Σ^*𝑧 ∈ 𝑐𝐹)
119	92, 94, 106, 118	r19.29af2 3270	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) → ∃𝑡 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑡)
120	119	ex 418	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ℝ^) → (𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 → ∃𝑡 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑡))
121	120	ralrimiva 3154	. . . . . 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 5112	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 = Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) → (𝑟 < 𝑠 ↔ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 < 𝑠))
125	124	notbid 321	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 = Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) → (¬ 𝑟 < 𝑠 ↔ ¬ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 < 𝑠))
126	125	ralbidv 3185	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 = Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) → (∀𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ¬ 𝑟 < 𝑠 ↔ ∀𝑠 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ¬ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 < 𝑠))
127	123	breq2d 5114	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 = Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) → (𝑠 < 𝑟 ↔ 𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹))
128	127	imbi1d 344	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 = Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹) → ((𝑠 < 𝑟 → ∃𝑡 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑡) ↔ (𝑠 < Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 → ∃𝑡 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))𝑠 < 𝑡)))
129	128	ralbidv 3185	. . . . . . 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 3569	. . . . 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 9451	. . 3 ⊢ (𝜑 → sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ) ∈ ℝ^*)
134		nfv 1946	. . . . 5 ⊢ Ⅎ𝑎𝜑
135		nfcv 2922	. . . . . 6 ⊢ Ⅎ𝑎𝑠
136		nfmpt1 5203	. . . . . . 7 ⊢ Ⅎ𝑎(𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
137	136	nfrn 5933	. . . . . 6 ⊢ Ⅎ𝑎ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
138	135, 137	nfel 2936	. . . . 5 ⊢ Ⅎ𝑎 𝑠 ∈ ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
139	134, 138	nfan 1931	. . . 4 ⊢ Ⅎ𝑎(𝜑 ∧ 𝑠 ∈ ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶))))
140		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑎 ∈ (𝒫 𝐴 ∩ Fin))
141		simpll 779	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑗 ∈ 𝑎) → 𝜑)
142	140	elin1d 4101	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑎 ∈ 𝒫 𝐴)
143		elpwi 4563	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ 𝒫 𝐴 → 𝑎 ⊆ 𝐴)
144	142, 143	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑎 ⊆ 𝐴)
145	144	sselda 3908	. . . . . . . . . . . . 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 4102	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑎 ∈ Fin)
152	29, 32, 140, 146, 150, 151	esum2dlem 34767	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → Σ^𝑗 ∈ 𝑎Σ^𝑘 ∈ 𝐵𝐶 = Σ^*𝑧 ∈ ∪ 𝑗 ∈ 𝑎 ({𝑗} × 𝐵)𝐹)
153		nfv 1946	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin))
154		nfcv 2922	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗𝑎
155	37	anassrs 473	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
156	155	ralrimiva 3154	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ∀𝑘 ∈ 𝐵 𝐶 ∈ (0[,]+∞))
157		nfcv 2922	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘𝐵
158	157	esumcl 34705	. . . . . . . . . . . . . 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 34720	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → Σ^𝑗 ∈ 𝑎Σ^𝑘 ∈ 𝐵𝐶 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
162	152, 161	eqtr3d 2797	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝑎 ({𝑗} × 𝐵)𝐹 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^*𝑘 ∈ 𝐵𝐶)))
163		nfv 1946	. . . . . . . . . . 11 ⊢ Ⅎ𝑧(𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin))
164	65	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V)
165	46	adantlr 728	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) → 𝐹 ∈ (0[,]+∞))
166		iunss1 4965	. . . . . . . . . . . 12 ⊢ (𝑎 ⊆ 𝐴 → ∪ 𝑗 ∈ 𝑎 ({𝑗} × 𝐵) ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
167	144, 166	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ∪ 𝑗 ∈ 𝑎 ({𝑗} × 𝐵) ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
168	163, 164, 165, 167	esummono 34729	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝑎 ({𝑗} × 𝐵)𝐹 ≤ Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)
169	162, 168	eqbrtrrd 5128	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)) ≤ Σ^*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)
170	11	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → (ℝ^*_𝑠 ↾_s (0[,]+∞)) ∈ CMnd)
171	160	ralrimiva 3154	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ∀𝑗 ∈ 𝑎 Σ^*𝑘 ∈ 𝐵𝐶 ∈ (0[,]+∞))
172	10, 170, 151, 171	gsummptcl 20182	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)) ∈ (0[,]+∞))
173	9, 172	sselid 3906	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)) ∈ ℝ^*)
174	70	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 ∈ ℝ^)
175		xrlenlt 11375	. . . . . . . . . 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 1946	. . . . . . . . . . 11 ⊢ Ⅎ𝑧𝜑
179		eqidd 2761	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
180	178, 67, 65, 46, 179	esumval 34721	. . . . . . . . . 10 ⊢ (𝜑 → Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 = sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^*, < ))
181	180	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → Σ^𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹 = sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^*, < ))
182	181	breq1d 5112	. . . . . . . 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 5114	. . . . . 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 2760	. . . . . 6 ⊢ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶))) = (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
191		ovex 7453	. . . . . 6 ⊢ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)) ∈ V
192	190, 191	elrnmpti 5943	. . . . 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 3271	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))) → ¬ sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ) < 𝑠)
195	4	nfel1 2938	. . . . . . . . 9 ⊢ Ⅎ𝑐 𝑠 ∈ ℝ^*
196		nfcv 2922	. . . . . . . . . 10 ⊢ Ⅎ𝑐 <
197		nfcv 2922	. . . . . . . . . . 11 ⊢ Ⅎ𝑐ℝ^*
198	6, 197, 196	nfsup 9444	. . . . . . . . . 10 ⊢ Ⅎ𝑐sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < )
199	4, 196, 198	nfbr 5151	. . . . . . . . 9 ⊢ Ⅎ𝑐 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < )
200	195, 199	nfan 1931	. . . . . . . 8 ⊢ Ⅎ𝑐(𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))
201	3, 200	nfan 1931	. . . . . . 7 ⊢ Ⅎ𝑐(𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < )))
202		nfcv 2922	. . . . . . . 8 ⊢ Ⅎ𝑐𝑢
203	202, 6	nfel 2936	. . . . . . 7 ⊢ Ⅎ𝑐 𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
204	201, 203	nfan 1931	. . . . . 6 ⊢ Ⅎ𝑐((𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))) ∧ 𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))))
205		nfv 1946	. . . . . 6 ⊢ Ⅎ𝑐 𝑠 < 𝑢
206	204, 205	nfan 1931	. . . . 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 5130	. . . . . 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 4101	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → 𝑐 ∈ 𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
222		elpwi 4563	. . . . . . . . . . 11 ⊢ (𝑐 ∈ 𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
223		dmss 5883	. . . . . . . . . . . . . 14 ⊢ (𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → dom 𝑐 ⊆ dom ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
224		dmiun 5894	. . . . . . . . . . . . . 14 ⊢ dom ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) = ∪ 𝑗 ∈ 𝐴 dom ({𝑗} × 𝐵)
225	223, 224	sseqtrdi 3948	. . . . . . . . . . . . 13 ⊢ (𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → dom 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 dom ({𝑗} × 𝐵))
226		dmxpss 6162	. . . . . . . . . . . . . . . . 17 ⊢ dom ({𝑗} × 𝐵) ⊆ {𝑗}
227	226	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ 𝐴 → dom ({𝑗} × 𝐵) ⊆ {𝑗})
228		snssi 4745	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ 𝐴 → {𝑗} ⊆ 𝐴)
229	227, 228	sstrd 3918	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ 𝐴 → dom ({𝑗} × 𝐵) ⊆ 𝐴)
230	229	rgen 3078	. . . . . . . . . . . . . 14 ⊢ ∀𝑗 ∈ 𝐴 dom ({𝑗} × 𝐵) ⊆ 𝐴
231		iunss 5002	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑗 ∈ 𝐴 dom ({𝑗} × 𝐵) ⊆ 𝐴 ↔ ∀𝑗 ∈ 𝐴 dom ({𝑗} × 𝐵) ⊆ 𝐴)
232	230, 231	mpbir 234	. . . . . . . . . . . . 13 ⊢ ∪ 𝑗 ∈ 𝐴 dom ({𝑗} × 𝐵) ⊆ 𝐴
233	225, 232	sstrdi 3920	. . . . . . . . . . . 12 ⊢ (𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → dom 𝑐 ⊆ 𝐴)
234	18	dmex 7921	. . . . . . . . . . . . 13 ⊢ dom 𝑐 ∈ V
235	234	elpw 4560	. . . . . . . . . . . 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 4102	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → 𝑐 ∈ Fin)
239		dmfi 9325	. . . . . . . . . . 11 ⊢ (𝑐 ∈ Fin → dom 𝑐 ∈ Fin)
240	238, 239	syl 18	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → dom 𝑐 ∈ Fin)
241	237, 240	elind 4097	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → dom 𝑐 ∈ (𝒫 𝐴 ∩ Fin))
242		ovex 7453	. . . . . . . . . 10 ⊢ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶)) ∈ V
243	242	a1i 11	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶)) ∈ V)
244		mpteq1 5193	. . . . . . . . . . 11 ⊢ (𝑎 = dom 𝑐 → (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶) = (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶))
245	244	oveq2d 7436	. . . . . . . . . 10 ⊢ (𝑎 = dom 𝑐 → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)) = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
246	190, 245	elrnmpt1s 5940	. . . . . . . . 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 5114	. . . . . . . 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 2922	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧(ℝ^*_𝑠 ↾_s (0[,]+∞))
253		nfcv 2922	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧 Σ_g
254		nfmpt1 5203	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑧(𝑧 ∈ 𝑐 ↦ 𝐹)
255	252, 253, 254	nfov 7450	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑧((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))
256	108, 109, 255	nfbr 5151	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧 𝑠 < ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))
257	107, 256	nfan 1931	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑧((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
258		nfv 1946	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑧 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)
259	257, 258	nfan 1931	. . . . . . . . . . . 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 3908	. . . . . . . . . . . . . 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 3260	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ∀𝑧 ∈ 𝑐 𝐹 ∈ (0[,]+∞))
266	10, 251, 238, 265	gsummptcl 20182	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) ∈ (0[,]+∞))
267	9, 266	sselid 3906	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) ∈ ℝ^)
268		nfv 1946	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
269		nfcv 2922	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗𝑐
270	25	nfpw 4575	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
271		nfcv 2922	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑗Fin
272	270, 271	nfin 4121	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑗(𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)
273	269, 272	nfel 2936	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)
274	268, 273	nfan 1931	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗(((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin))
275		simpll 779	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → 𝜑)
276	78, 233	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → dom 𝑐 ⊆ 𝐴)
277	276	sselda 3908	. . . . . . . . . . . . . . . 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 3260	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ∀𝑗 ∈ dom 𝑐Σ^*𝑘 ∈ 𝐵𝐶 ∈ (0[,]+∞))
283	10, 251, 240, 282	gsummptcl 20182	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶)) ∈ (0[,]+∞))
284	9, 283	sselid 3906	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶)) ∈ ℝ^*)
285		simplr 781	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → 𝑠 < ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))
286	23, 273	nfan 1931	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin))
287		id 23	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
288		xpss 5666	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑗} × 𝐵) ⊆ (V × V)
289	288	rgenw 3080	. . . . . . . . . . . . . . . . . 18 ⊢ ∀𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ⊆ (V × V)
290		iunss 5002	. . . . . . . . . . . . . . . . . 18 ⊢ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ⊆ (V × V) ↔ ∀𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ⊆ (V × V))
291	289, 290	mpbir 234	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ⊆ (V × V)
292	291	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ⊆ (V × V))
293	287, 292	sstrd 3918	. . . . . . . . . . . . . . 15 ⊢ (𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → 𝑐 ⊆ (V × V))
294	78, 293	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → 𝑐 ⊆ (V × V))
295		df-rel 5657	. . . . . . . . . . . . . 14 ⊢ (Rel 𝑐 ↔ 𝑐 ⊆ (V × V))
296	294, 295	sylibr 237	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → Rel 𝑐)
297	29, 286, 10, 32, 296, 14, 12, 47	gsummpt2d 33653	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)) = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ ((ℝ^*_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑘 ∈ (𝑐 “ {𝑗}) ↦ 𝐶)))))
298		nfcv 2922	. . . . . . . . . . . . . 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 6053	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → (𝑐 “ {𝑗}) ⊆ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) “ {𝑗}))
304	302, 303	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → (𝑐 “ {𝑗}) ⊆ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) “ {𝑗}))
305	58, 60	iunsnima 33255	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) “ {𝑗}) = 𝐵)
306	275, 277, 305	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) “ {𝑗}) = 𝐵)
307	304, 306	sseqtrd 3944	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → (𝑐 “ {𝑗}) ⊆ 𝐵)
308	307	sselda 3908	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) ∧ 𝑘 ∈ (𝑐 “ {𝑗})) → 𝑘 ∈ 𝐵)
309	300, 301, 308, 37	syl12anc 850	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) ∧ 𝑘 ∈ (𝑐 “ {𝑗})) → 𝐶 ∈ (0[,]+∞))
310	309	ralrimiva 3154	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → ∀𝑘 ∈ (𝑐 “ {𝑗})𝐶 ∈ (0[,]+∞))
311		imaexg 7925	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ V → (𝑐 “ {𝑗}) ∈ V)
312	18, 311	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 “ {𝑗}) ∈ V
313		nfcv 2922	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘(𝑐 “ {𝑗})
314	313	esumcl 34705	. . . . . . . . . . . . . . . 16 ⊢ (((𝑐 “ {𝑗}) ∈ V ∧ ∀𝑘 ∈ (𝑐 “ {𝑗})𝐶 ∈ (0[,]+∞)) → Σ^*𝑘 ∈ (𝑐 “ {𝑗})𝐶 ∈ (0[,]+∞))
315	312, 314	mpan 703	. . . . . . . . . . . . . . 15 ⊢ (∀𝑘 ∈ (𝑐 “ {𝑗})𝐶 ∈ (0[,]+∞) → Σ^*𝑘 ∈ (𝑐 “ {𝑗})𝐶 ∈ (0[,]+∞))
316	310, 315	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → Σ^*𝑘 ∈ (𝑐 “ {𝑗})𝐶 ∈ (0[,]+∞))
317		nfv 1946	. . . . . . . . . . . . . . 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 34729	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → Σ^𝑘 ∈ (𝑐 “ {𝑗})𝐶 ≤ Σ^𝑘 ∈ 𝐵𝐶)
324	286, 298, 299, 316, 278, 323	esumlef 34737	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → Σ^𝑗 ∈ dom 𝑐Σ^𝑘 ∈ (𝑐 “ {𝑗})𝐶 ≤ Σ^𝑗 ∈ dom 𝑐Σ^𝑘 ∈ 𝐵𝐶)
325	14, 239	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → dom 𝑐 ∈ Fin)
326	286, 298, 325, 316	esumgsum 34720	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → Σ^𝑗 ∈ dom 𝑐Σ^𝑘 ∈ (𝑐 “ {𝑗})𝐶 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ (𝑐 “ {𝑗})𝐶)))
327	14	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → 𝑐 ∈ Fin)
328		imafi2 9351	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ Fin → (𝑐 “ {𝑗}) ∈ Fin)
329	327, 328	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → (𝑐 “ {𝑗}) ∈ Fin)
330	317, 313, 329, 309	esumgsum 34720	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) ∧ 𝑗 ∈ dom 𝑐) → Σ^𝑘 ∈ (𝑐 “ {𝑗})𝐶 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑘 ∈ (𝑐 “ {𝑗}) ↦ 𝐶)))
331	286, 330	mpteq2da 5196	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ (𝑐 “ {𝑗})𝐶) = (𝑗 ∈ dom 𝑐 ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑘 ∈ (𝑐 “ {𝑗}) ↦ 𝐶))))
332	331	oveq2d 7436	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ (𝑐 “ {𝑗})𝐶)) = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑘 ∈ (𝑐 “ {𝑗}) ↦ 𝐶)))))
333	326, 332	eqtrd 2795	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → Σ^𝑗 ∈ dom 𝑐Σ^𝑘 ∈ (𝑐 “ {𝑗})𝐶 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑘 ∈ (𝑐 “ {𝑗}) ↦ 𝐶)))))
334	286, 298, 325, 278	esumgsum 34720	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → Σ^𝑗 ∈ dom 𝑐Σ^𝑘 ∈ 𝐵𝐶 = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
335	324, 333, 334	3brtr3d 5135	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑘 ∈ (𝑐 “ {𝑗}) ↦ 𝐶)))) ≤ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
336	297, 335	eqbrtrd 5126	. . . . . . . . . . 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 13291	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ^) ∧ 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))) ∧ 𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin)) → 𝑠 < ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ dom 𝑐 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
340	247, 249, 339	rspcedvd 3578	. . . . . . 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 5943	. . . . . . 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 3271	. . . 4 ⊢ ((((𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))) ∧ 𝑢 ∈ ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹)))) ∧ 𝑠 < 𝑢) → ∃𝑡 ∈ ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^*𝑘 ∈ 𝐵𝐶)))𝑠 < 𝑡)
347	2, 132	suplub 9453	. . . . . 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 5106	. . . . . 6 ⊢ (𝑡 = 𝑢 → (𝑠 < 𝑡 ↔ 𝑠 < 𝑢))
350	349	cbvrexvw 3241	. . . . 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 3170	. . 3 ⊢ ((𝜑 ∧ (𝑠 ∈ ℝ^* ∧ 𝑠 < sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^, < ))) → ∃𝑡 ∈ ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))𝑠 < 𝑡)
353	2, 133, 194, 352	eqsupd 9450	. 2 ⊢ (𝜑 → sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶))), ℝ^, < ) = sup(ran (𝑐 ∈ (𝒫 ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑧 ∈ 𝑐 ↦ 𝐹))), ℝ^*, < ))
354		nfcv 2922	. . 3 ⊢ Ⅎ𝑗𝐴
355		eqidd 2761	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)) = ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶)))
356	23, 354, 58, 159, 355	esumval 34721	. 2 ⊢ (𝜑 → Σ^𝑗 ∈ 𝐴Σ^𝑘 ∈ 𝐵𝐶 = sup(ran (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦ ((ℝ^_𝑠 ↾_s (0[,]+∞)) Σ_g (𝑗 ∈ 𝑎 ↦ Σ^𝑘 ∈ 𝐵𝐶))), ℝ^*, < ))
357	353, 356, 180	3eqtr4d 2805	1 ⊢ (𝜑 → Σ^𝑗 ∈ 𝐴Σ^𝑘 ∈ 𝐵𝐶 = Σ^*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)𝐹)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 Ⅎwnfc 2907 ∀wral 3076 ∃wrex 3086 Vcvv 3450 ⊆ wss 3895 ∩ cin 4089 𝒫 cpw 4556 {csn 4583 ⟨cop 4589 ∪ ciun 4950 class class class wbr 5102 ↦ cmpt 5185 Or wor 5557 × cxp 5648 dom cdm 5650 ran crn 5651 “ cima 5653 Rel wrel 5655 (class class class)co 7420 Fincfn 8974 supcsup 9433 0cc0 11201 +∞cpnf 11341 ℝ^*cxr 11343 < clt 11344 ≤ cle 11345 [,]cicc 13480 ↾_s cress 17409 Σ_g cgsu 17612 ℝ^*_𝑠cxrs 17673 CMndccmn 19995 Σ^*cesum 34702

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-inf2 9643 ax-cnex 11257 ax-resscn 11258 ax-1cn 11259 ax-icn 11260 ax-addcl 11261 ax-addrcl 11262 ax-mulcl 11263 ax-mulrcl 11264 ax-mulcom 11265 ax-addass 11266 ax-mulass 11267 ax-distr 11268 ax-i2m1 11269 ax-1ne0 11270 ax-1rid 11271 ax-rnegex 11272 ax-rrecex 11273 ax-cnre 11274 ax-pre-lttri 11275 ax-pre-lttrn 11276 ax-pre-ltadd 11277 ax-pre-mulgt0 11278 ax-pre-sup 11279 ax-addf 11280 ax-mulf 11281

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-tp 4588 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-om 7878 df-1st 8001 df-2nd 8002 df-supp 8178 df-frecs 8300 df-wrecs 8331 df-recs 8380 df-rdg 8419 df-1o 8477 df-2o 8478 df-er 8718 df-map 8850 df-pm 8851 df-ixp 8927 df-en 8975 df-dom 8976 df-sdom 8977 df-fin 8978 df-fsupp 9355 df-fi 9404 df-sup 9435 df-inf 9436 df-oi 9505 df-card 10021 df-pnf 11346 df-mnf 11347 df-xr 11348 df-ltxr 11349 df-le 11350 df-sub 11544 df-neg 11545 df-div 11975 df-nn 12337 df-2 12406 df-3 12407 df-4 12408 df-5 12409 df-6 12410 df-7 12411 df-8 12412 df-9 12413 df-n0 12608 df-z 12695 df-dec 12816 df-uz 12967 df-q 13077 df-rp 13122 df-xneg 13242 df-xadd 13243 df-xmul 13244 df-ioo 13481 df-ioc 13482 df-ico 13483 df-icc 13484 df-fz 13641 df-fzo 13790 df-fl 13933 df-mod 14011 df-seq 14146 df-exp 14206 df-fac 14419 df-bc 14448 df-hash 14476 df-shft 15221 df-cj 15267 df-re 15268 df-im 15269 df-sqrt 15403 df-abs 15404 df-limsup 15639 df-clim 15656 df-rlim 15657 df-sum 15855 df-ef 16234 df-sin 16236 df-cos 16237 df-pi 16239 df-struct 17326 df-sets 17343 df-slot 17361 df-ndx 17373 df-base 17389 df-ress 17410 df-plusg 17442 df-mulr 17443 df-starv 17444 df-sca 17445 df-vsca 17446 df-ip 17447 df-tset 17448 df-ple 17449 df-ds 17451 df-unif 17452 df-hom 17453 df-cco 17454 df-rest 17594 df-topn 17595 df-0g 17613 df-gsum 17614 df-topgen 17615 df-pt 17616 df-prds 17619 df-ordt 17674 df-xrs 17675 df-qtop 17680 df-imas 17681 df-xps 17683 df-mre 17757 df-mrc 17758 df-acs 17760 df-ps 18741 df-tsr 18742 df-plusf 18816 df-mgm 18817 df-sgrp 18909 df-mnd 18925 df-mhm 18979 df-submnd 18980 df-grp 19148 df-minusg 19149 df-sbg 19150 df-mulg 19279 df-subg 19334 df-cntz 19532 df-cmn 19997 df-abl 19998 df-mgp 20362 df-rng 20376 df-ur 20409 df-ring 20462 df-cring 20463 df-subrng 20799 df-subrg 20823 df-abv 21067 df-lmod 21138 df-scaf 21139 df-sra 21449 df-rgmod 21450 df-psmet 21671 df-xmet 21672 df-met 21673 df-bl 21674 df-mopn 21675 df-fbas 21676 df-fg 21677 df-cnfld 21680 df-top 23213 df-topon 23230 df-topsp 23252 df-bases 23265 df-cld 23338 df-ntr 23339 df-cls 23340 df-nei 23417 df-lp 23455 df-perf 23456 df-cn 23546 df-cnp 23547 df-haus 23634 df-tx 23882 df-hmeo 24075 df-fil 24166 df-fm 24258 df-flim 24259 df-flf 24260 df-tmd 24392 df-tgp 24393 df-tsms 24447 df-trg 24480 df-xms 24640 df-ms 24641 df-tms 24642 df-nm 24902 df-ngp 24903 df-nrg 24905 df-nlm 24906 df-ii 25199 df-cncf 25200 df-limc 26187 df-dv 26188 df-log 26885 df-esum 34703

This theorem is used by: esumiun 34769

W3C validator