esum2d

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

	Ref	Expression
Hypotheses	esum2d.0	$⊢ \underline{Ⅎ} k F$
	esum2d.1	$⊢ z = ⟨j, k⟩ \to F = C$
	esum2d.2	$⊢ φ \to A \in V$
	esum2d.3	$⊢ (φ \land j \in A) \to B \in W$
	esum2d.4	$⊢ (φ \land (j \in A \land k \in B)) \to C \in [0, +∞]$
Assertion	esum2d	$⊢ φ \to \underset{j \in A}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{*}} F$

Proof

Step	Hyp	Ref	Expression
1		esum2d.0	$⊢ \underline{Ⅎ} k F$
2		esum2d.1	$⊢ z = ⟨j, k⟩ \to F = C$
3		esum2d.2	$⊢ φ \to A \in V$
4		esum2d.3	$⊢ (φ \land j \in A) \to B \in W$
5		esum2d.4	$⊢ (φ \land (j \in A \land k \in B)) \to C \in [0, +∞]$
6		xrltso	$⊢ < Or ℝ^{*}$
7	6	a1i	$⊢ φ \to < Or ℝ^{*}$
8		nfv	$⊢ Ⅎ c φ$
9		nfcv	$⊢ \underline{Ⅎ} c s$
10		nfmpt1	$⊢ \underline{Ⅎ} c (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F)$
11	10	nfrn	$⊢ \underline{Ⅎ} c ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F)$
12	9 11	nfel	$⊢ Ⅎ c s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F)$
13	8 12	nfan	$⊢ Ⅎ c (φ \land s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F))$
14		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
15		xrge0base	$⊢ [0, +∞] = {Base}_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])}$
16		xrge0cmn	$⊢ ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in CMnd$
17	16	a1i	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in CMnd$
18		simpr	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)$
19	18	elin2d	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to c \in Fin$
20		simpll	$⊢ ((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land z \in c) \to φ$
21	18	elin1d	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to c \in 𝒫 ⋃_{j \in A} (\{j\} \times B)$
22	21	adantr	$⊢ ((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land z \in c) \to c \in 𝒫 ⋃_{j \in A} (\{j\} \times B)$
23		vex	$⊢ c \in V$
24	23	elpw	$⊢ c \in 𝒫 ⋃_{j \in A} (\{j\} \times B) \leftrightarrow c \subseteq ⋃_{j \in A} (\{j\} \times B)$
25	22 24	sylib	$⊢ ((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land z \in c) \to c \subseteq ⋃_{j \in A} (\{j\} \times B)$
26		simpr	$⊢ ((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land z \in c) \to z \in c$
27	25 26	sseldd	$⊢ ((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land z \in c) \to z \in ⋃_{j \in A} (\{j\} \times B)$
28		nfv	$⊢ Ⅎ j φ$
29		nfcv	$⊢ \underline{Ⅎ} j z$
30		nfiu1	$⊢ \underline{Ⅎ} j ⋃_{j \in A} (\{j\} \times B)$
31	29 30	nfel	$⊢ Ⅎ j z \in ⋃_{j \in A} (\{j\} \times B)$
32	28 31	nfan	$⊢ Ⅎ j (φ \land z \in ⋃_{j \in A} (\{j\} \times B))$
33		nfv	$⊢ Ⅎ k (((φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \land j \in A) \land z \in (\{j\} \times B))$
34		nfcv	$⊢ \underline{Ⅎ} k [0, +∞]$
35	1 34	nfel	$⊢ Ⅎ k F \in [0, +∞]$
36	2	adantl	$⊢ (((((φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \land j \in A) \land z \in (\{j\} \times B)) \land k \in B) \land z = ⟨j, k⟩) \to F = C$
37		simp-5l	$⊢ (((((φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \land j \in A) \land z \in (\{j\} \times B)) \land k \in B) \land z = ⟨j, k⟩) \to φ$
38		simp-4r	$⊢ (((((φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \land j \in A) \land z \in (\{j\} \times B)) \land k \in B) \land z = ⟨j, k⟩) \to j \in A$
39		simplr	$⊢ (((((φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \land j \in A) \land z \in (\{j\} \times B)) \land k \in B) \land z = ⟨j, k⟩) \to k \in B$
40	37 38 39 5	syl12anc	$⊢ (((((φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \land j \in A) \land z \in (\{j\} \times B)) \land k \in B) \land z = ⟨j, k⟩) \to C \in [0, +∞]$
41	36 40	eqeltrd	$⊢ (((((φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \land j \in A) \land z \in (\{j\} \times B)) \land k \in B) \land z = ⟨j, k⟩) \to F \in [0, +∞]$
42		elsnxp	$⊢ j \in A \to (z \in (\{j\} \times B) \leftrightarrow \exists k \in B z = ⟨j, k⟩)$
43	42	biimpa	$⊢ (j \in A \land z \in (\{j\} \times B)) \to \exists k \in B z = ⟨j, k⟩$
44	43	adantll	$⊢ (((φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \land j \in A) \land z \in (\{j\} \times B)) \to \exists k \in B z = ⟨j, k⟩$
45	33 35 41 44	r19.29af2	$⊢ (((φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \land j \in A) \land z \in (\{j\} \times B)) \to F \in [0, +∞]$
46		simpr	$⊢ (φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \to z \in ⋃_{j \in A} (\{j\} \times B)$
47		eliun	$⊢ z \in ⋃_{j \in A} (\{j\} \times B) \leftrightarrow \exists j \in A z \in (\{j\} \times B)$
48	46 47	sylib	$⊢ (φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \to \exists j \in A z \in (\{j\} \times B)$
49	32 45 48	r19.29af	$⊢ (φ \land z \in ⋃_{j \in A} (\{j\} \times B)) \to F \in [0, +∞]$
50	20 27 49	syl2anc	$⊢ ((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land z \in c) \to F \in [0, +∞]$
51	50	ralrimiva	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \forall z \in c F \in [0, +∞]$
52	15 17 19 51	gsummptcl	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F \in [0, +∞]$
53	14 52	sselid	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F \in ℝ^{}$
54	53	ralrimiva	$⊢ φ \to \forall c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F \in ℝ^{}$
55		eqid	$⊢ (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) = (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)$
56	55	rnmptss	$⊢ \forall c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F \in ℝ^{} \to ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \subseteq ℝ^{}$
57	54 56	syl	$⊢ φ \to ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \subseteq ℝ^{}$
58	57	ad3antrrr	$⊢ (((φ \land s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land s = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \to ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \subseteq ℝ^{}$
59		simpllr	$⊢ (((φ \land s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land s = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \to s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F)$
60	58 59	sseldd	$⊢ (((φ \land s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land s = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \to s \in ℝ^{*}$
61		vsnex	$⊢ \{j\} \in V$
62		xpexg	$⊢ (\{j\} \in V \land B \in W) \to \{j\} \times B \in V$
63	61 4 62	sylancr	$⊢ (φ \land j \in A) \to \{j\} \times B \in V$
64	63	ralrimiva	$⊢ φ \to \forall j \in A \{j\} \times B \in V$
65		iunexg	$⊢ (A \in V \land \forall j \in A \{j\} \times B \in V) \to ⋃_{j \in A} (\{j\} \times B) \in V$
66	3 64 65	syl2anc	$⊢ φ \to ⋃_{j \in A} (\{j\} \times B) \in V$
67	49	ralrimiva	$⊢ φ \to \forall z \in ⋃_{j \in A} (\{j\} \times B) F \in [0, +∞]$
68		nfcv	$⊢ \underline{Ⅎ} z ⋃_{j \in A} (\{j\} \times B)$
69	68	esumcl	$⊢ (⋃_{j \in A} (\{j\} \times B) \in V \land \forall z \in ⋃_{j \in A} (\{j\} \times B) F \in [0, +∞]) \to \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{*}} F \in [0, +∞]$
70	66 67 69	syl2anc	$⊢ φ \to \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{*}} F \in [0, +∞]$
71	14 70	sselid	$⊢ φ \to \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F \in ℝ^{}$
72	71	ad3antrrr	$⊢ (((φ \land s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land s = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \to \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F \in ℝ^{}$
73		simpr	$⊢ (((φ \land s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land s = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \to s = \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F$
74		nfv	$⊢ Ⅎ z (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin))$
75		nfcv	$⊢ \underline{Ⅎ} z c$
76	74 75 19 50	esumgsum	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{z \in c}{\sum^{}} F = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F$
77	66	adantr	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to ⋃_{j \in A} (\{j\} \times B) \in V$
78	49	adantlr	$⊢ ((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land z \in ⋃_{j \in A} (\{j\} \times B)) \to F \in [0, +∞]$
79	21 24	sylib	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to c \subseteq ⋃_{j \in A} (\{j\} \times B)$
80	74 77 78 79	esummono	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{z \in c}{\sum^{}} F \leq \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F$
81	76 80	eqbrtrrd	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F \leq \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F$
82	81	adantlr	$⊢ ((φ \land s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F \leq \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{*}} F$
83	82	adantr	$⊢ (((φ \land s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land s = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \to \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F \leq \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F$
84	73 83	eqbrtrd	$⊢ (((φ \land s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land s = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \to s \leq \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{*}} F$
85		xrlenlt	$⊢ (s \in ℝ^{} \land \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F \in ℝ^{}) \to (s \leq \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F \leftrightarrow \neg \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{*}} F < s)$
86	85	biimpa	$⊢ ((s \in ℝ^{} \land \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F \in ℝ^{}) \land s \leq \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \to \neg \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{*}} F < s$
87	60 72 84 86	syl21anc	$⊢ (((φ \land s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land s = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \to \neg \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{*}} F < s$
88		simpr	$⊢ (φ \land s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \to s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)$
89		ovex	$⊢ \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F \in V$
90	55 89	elrnmpti	$⊢ s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \leftrightarrow \exists c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) s = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F$
91	88 90	sylib	$⊢ (φ \land s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \to \exists c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) s = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F$
92	13 87 91	r19.29af	$⊢ (φ \land s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \to \neg \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F < s$
93	92	ralrimiva	$⊢ φ \to \forall s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \neg \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F < s$
94		nfv	$⊢ Ⅎ c ((φ \land s \in ℝ^{}) \land s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F)$
95		nfv	$⊢ Ⅎ c s < t$
96	11 95	nfrexw	$⊢ Ⅎ c \exists t \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F) s < t$
97	76	adantlr	$⊢ ((φ \land s \in ℝ^{}) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{z \in c}{\sum^{}} F = \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F$
98	97	adantlr	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{z \in c}{\sum^{}} F = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F$
99	98	adantr	$⊢ ((((φ \land s \in ℝ^{}) \land s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land s < \underset{z \in c}{\sum^{}} F) \to \underset{z \in c}{\sum^{}} F = \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F$
100		simplr	$⊢ ((((φ \land s \in ℝ^{}) \land s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land s < \underset{z \in c}{\sum^{*}} F) \to c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)$
101	89	a1i	$⊢ ((((φ \land s \in ℝ^{}) \land s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land s < \underset{z \in c}{\sum^{}} F) \to \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F \in V$
102	55	elrnmpt1	$⊢ (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) \land \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F \in V) \to \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F)$
103	100 101 102	syl2anc	$⊢ ((((φ \land s \in ℝ^{}) \land s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land s < \underset{z \in c}{\sum^{}} F) \to \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F)$
104	99 103	eqeltrd	$⊢ ((((φ \land s \in ℝ^{}) \land s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land s < \underset{z \in c}{\sum^{}} F) \to \underset{z \in c}{\sum^{}} F \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F)$
105		simpr	$⊢ (((((φ \land s \in ℝ^{}) \land s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land s < \underset{z \in c}{\sum^{}} F) \land t = \underset{z \in c}{\sum^{}} F) \to t = \underset{z \in c}{\sum^{*}} F$
106	105	breq2d	$⊢ (((((φ \land s \in ℝ^{}) \land s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land s < \underset{z \in c}{\sum^{}} F) \land t = \underset{z \in c}{\sum^{}} F) \to (s < t \leftrightarrow s < \underset{z \in c}{\sum^{*}} F)$
107		simpr	$⊢ ((((φ \land s \in ℝ^{}) \land s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land s < \underset{z \in c}{\sum^{}} F) \to s < \underset{z \in c}{\sum^{}} F$
108	104 106 107	rspcedvd	$⊢ ((((φ \land s \in ℝ^{}) \land s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land s < \underset{z \in c}{\sum^{}} F) \to \exists t \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) s < t$
109		nfv	$⊢ Ⅎ z (φ \land s \in ℝ^{*})$
110		nfcv	$⊢ \underline{Ⅎ} z s$
111		nfcv	$⊢ \underline{Ⅎ} z <$
112	68	nfesum1	$⊢ \underline{Ⅎ} z \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{*}} F$
113	110 111 112	nfbr	$⊢ Ⅎ z s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{*}} F$
114	109 113	nfan	$⊢ Ⅎ z ((φ \land s \in ℝ^{}) \land s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F)$
115	66	ad2antrr	$⊢ ((φ \land s \in ℝ^{}) \land s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \to ⋃_{j \in A} (\{j\} \times B) \in V$
116	49	3ad2antr3	$⊢ (φ \land (s \in ℝ^{} \land s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F \land z \in ⋃_{j \in A} (\{j\} \times B))) \to F \in [0, +∞]$
117	116	3anassrs	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \land z \in ⋃_{j \in A} (\{j\} \times B)) \to F \in [0, +∞]$
118		simplr	$⊢ ((φ \land s \in ℝ^{}) \land s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \to s \in ℝ^{*}$
119		simpr	$⊢ ((φ \land s \in ℝ^{}) \land s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \to s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{*}} F$
120	114 115 117 118 119	esumlub	$⊢ ((φ \land s \in ℝ^{}) \land s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \to \exists c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) s < \underset{z \in c}{\sum^{*}} F$
121	94 96 108 120	r19.29af2	$⊢ ((φ \land s \in ℝ^{}) \land s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \to \exists t \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F) s < t$
122	121	ex	$⊢ (φ \land s \in ℝ^{}) \to (s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F \to \exists t \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F) s < t)$
123	122	ralrimiva	$⊢ φ \to \forall s \in ℝ^{} (s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F \to \exists t \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F) s < t)$
124	93 123	jca	$⊢ φ \to (\forall s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \neg \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F < s \land \forall s \in ℝ^{} (s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F \to \exists t \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F) s < t))$
125		simpr	$⊢ (φ \land r = \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \to r = \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F$
126	125	breq1d	$⊢ (φ \land r = \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \to (r < s \leftrightarrow \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F < s)$
127	126	notbid	$⊢ (φ \land r = \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \to (\neg r < s \leftrightarrow \neg \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F < s)$
128	127	ralbidv	$⊢ (φ \land r = \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \to (\forall s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \neg r < s \leftrightarrow \forall s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \neg \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F < s)$
129	125	breq2d	$⊢ (φ \land r = \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \to (s < r \leftrightarrow s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F)$
130	129	imbi1d	$⊢ (φ \land r = \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \to ((s < r \to \exists t \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) s < t) \leftrightarrow (s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F \to \exists t \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) s < t))$
131	130	ralbidv	$⊢ (φ \land r = \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \to (\forall s \in ℝ^{} (s < r \to \exists t \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) s < t) \leftrightarrow \forall s \in ℝ^{} (s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F \to \exists t \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) s < t))$
132	128 131	anbi12d	$⊢ (φ \land r = \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F) \to ((\forall s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \neg r < s \land \forall s \in ℝ^{} (s < r \to \exists t \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) s < t)) \leftrightarrow (\forall s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \neg \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F < s \land \forall s \in ℝ^{} (s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F \to \exists t \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F) s < t)))$
133	71 132	rspcedv	$⊢ φ \to ((\forall s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \neg \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F < s \land \forall s \in ℝ^{} (s < \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F \to \exists t \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) s < t)) \to \exists r \in ℝ^{} (\forall s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \neg r < s \land \forall s \in ℝ^{} (s < r \to \exists t \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F) s < t)))$
134	124 133	mpd	$⊢ φ \to \exists r \in ℝ^{} (\forall s \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \neg r < s \land \forall s \in ℝ^{} (s < r \to \exists t \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) s < t))$
135	7 134	supcl	$⊢ φ \to sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <) \in ℝ^{*}$
136		nfv	$⊢ Ⅎ a φ$
137		nfcv	$⊢ \underline{Ⅎ} a s$
138		nfmpt1	$⊢ \underline{Ⅎ} a (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C)$
139	138	nfrn	$⊢ \underline{Ⅎ} a ran (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C)$
140	137 139	nfel	$⊢ Ⅎ a s \in ran (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C)$
141	136 140	nfan	$⊢ Ⅎ a (φ \land s \in ran (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C))$
142		simpr	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to a \in (𝒫 A \cap Fin)$
143		simpll	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land j \in a) \to φ$
144	142	elin1d	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to a \in 𝒫 A$
145		elpwi	$⊢ a \in 𝒫 A \to a \subseteq A$
146	144 145	syl	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to a \subseteq A$
147	146	sselda	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land j \in a) \to j \in A$
148	143 147 4	syl2anc	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land j \in a) \to B \in W$
149	143	adantrr	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land (j \in a \land k \in B)) \to φ$
150	147	adantrr	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land (j \in a \land k \in B)) \to j \in A$
151		simprr	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land (j \in a \land k \in B)) \to k \in B$
152	149 150 151 5	syl12anc	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land (j \in a \land k \in B)) \to C \in [0, +∞]$
153	142	elin2d	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to a \in Fin$
154	1 2 142 148 152 153	esum2dlem	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \underset{j \in a}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in a} (\{j\} \times B)}{\sum^{*}} F$
155		nfv	$⊢ Ⅎ j (φ \land a \in (𝒫 A \cap Fin))$
156		nfcv	$⊢ \underline{Ⅎ} j a$
157	5	anassrs	$⊢ ((φ \land j \in A) \land k \in B) \to C \in [0, +∞]$
158	157	ralrimiva	$⊢ (φ \land j \in A) \to \forall k \in B C \in [0, +∞]$
159		nfcv	$⊢ \underline{Ⅎ} k B$
160	159	esumcl	$⊢ (B \in W \land \forall k \in B C \in [0, +∞]) \to \underset{k \in B}{\sum^{*}} C \in [0, +∞]$
161	4 158 160	syl2anc	$⊢ (φ \land j \in A) \to \underset{k \in B}{\sum^{*}} C \in [0, +∞]$
162	143 147 161	syl2anc	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land j \in a) \to \underset{k \in B}{\sum^{*}} C \in [0, +∞]$
163	155 156 153 162	esumgsum	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \underset{j \in a}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C$
164	154 163	eqtr3d	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \underset{z \in ⋃_{j \in a} (\{j\} \times B)}{\sum^{}} F = \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{*}} C$
165		nfv	$⊢ Ⅎ z (φ \land a \in (𝒫 A \cap Fin))$
166	66	adantr	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to ⋃_{j \in A} (\{j\} \times B) \in V$
167	49	adantlr	$⊢ ((φ \land a \in (𝒫 A \cap Fin)) \land z \in ⋃_{j \in A} (\{j\} \times B)) \to F \in [0, +∞]$
168		iunss1	$⊢ a \subseteq A \to ⋃_{j \in a} (\{j\} \times B) \subseteq ⋃_{j \in A} (\{j\} \times B)$
169	146 168	syl	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to ⋃_{j \in a} (\{j\} \times B) \subseteq ⋃_{j \in A} (\{j\} \times B)$
170	165 166 167 169	esummono	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \underset{z \in ⋃_{j \in a} (\{j\} \times B)}{\sum^{}} F \leq \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F$
171	164 170	eqbrtrrd	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C \leq \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{*}} F$
172	16	a1i	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in CMnd$
173	162	ralrimiva	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \forall j \in a \underset{k \in B}{\sum^{*}} C \in [0, +∞]$
174	15 172 153 173	gsummptcl	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C \in [0, +∞]$
175	14 174	sselid	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C \in ℝ^{*}$
176	71	adantr	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F \in ℝ^{}$
177		xrlenlt	$⊢ (\underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C \in ℝ^{} \land \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F \in ℝ^{}) \to (\underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C \leq \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F \leftrightarrow \neg \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F < \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{*}} C)$
178	175 176 177	syl2anc	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to (\underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C \leq \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F \leftrightarrow \neg \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F < \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C)$
179	171 178	mpbid	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \neg \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F < \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{*}} C$
180		nfv	$⊢ Ⅎ z φ$
181		eqidd	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F$
182	180 68 66 49 181	esumval	$⊢ φ \to \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F = sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{*} <)$
183	182	adantr	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F = sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{*} <)$
184	183	breq1d	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to (\underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{}} F < \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C \leftrightarrow sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <) < \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{*}} C)$
185	179 184	mtbid	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \neg sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <) < \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C$
186	185	adantlr	$⊢ ((φ \land s \in ran (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C)) \land a \in (𝒫 A \cap Fin)) \to \neg sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <) < \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C$
187	186	adantr	$⊢ (((φ \land s \in ran (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C)) \land a \in (𝒫 A \cap Fin)) \land s = \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C) \to \neg sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <) < \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C$
188		simpr	$⊢ (((φ \land s \in ran (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C)) \land a \in (𝒫 A \cap Fin)) \land s = \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C) \to s = \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C$
189	188	breq2d	$⊢ (((φ \land s \in ran (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C)) \land a \in (𝒫 A \cap Fin)) \land s = \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C) \to (sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <) < s \leftrightarrow sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <) < \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C)$
190	189	notbid	$⊢ (((φ \land s \in ran (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C)) \land a \in (𝒫 A \cap Fin)) \land s = \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C) \to (\neg sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <) < s \leftrightarrow \neg sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <) < \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C)$
191	187 190	mpbird	$⊢ (((φ \land s \in ran (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C)) \land a \in (𝒫 A \cap Fin)) \land s = \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C) \to \neg sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <) < s$
192		eqid	$⊢ (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C) = (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C)$
193		ovex	$⊢ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C \in V$
194	192 193	elrnmpti	$⊢ s \in ran (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C) \leftrightarrow \exists a \in (𝒫 A \cap Fin) s = \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C$
195	194	biimpi	$⊢ s \in ran (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C) \to \exists a \in (𝒫 A \cap Fin) s = \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C$
196	195	adantl	$⊢ (φ \land s \in ran (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C)) \to \exists a \in (𝒫 A \cap Fin) s = \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C$
197	141 191 196	r19.29af	$⊢ (φ \land s \in ran (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C)) \to \neg sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <) < s$
198	9	nfel1	$⊢ Ⅎ c s \in ℝ^{*}$
199		nfcv	$⊢ \underline{Ⅎ} c <$
200		nfcv	$⊢ \underline{Ⅎ} c ℝ^{*}$
201	11 200 199	nfsup	$⊢ \underline{Ⅎ} c sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <)$
202	9 199 201	nfbr	$⊢ Ⅎ c s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <)$
203	198 202	nfan	$⊢ Ⅎ c (s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{*} <))$
204	8 203	nfan	$⊢ Ⅎ c (φ \land (s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{*} <)))$
205		nfcv	$⊢ \underline{Ⅎ} c u$
206	205 11	nfel	$⊢ Ⅎ c u \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F)$
207	204 206	nfan	$⊢ Ⅎ c ((φ \land (s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <))) \land u \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F))$
208		nfv	$⊢ Ⅎ c s < u$
209	207 208	nfan	$⊢ Ⅎ c (((φ \land (s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <))) \land u \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land s < u)$
210		simp-5l	$⊢ (((((φ \land (s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <))) \land u \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land s < u) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land u = \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F) \to φ$
211		simpr1l	$⊢ (φ \land ((s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <)) \land u \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land (s < u \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) \land u = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F))) \to s \in ℝ^{}$
212	211	3anassrs	$⊢ (((φ \land (s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <))) \land u \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land (s < u \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) \land u = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \to s \in ℝ^{}$
213	212	3anassrs	$⊢ (((((φ \land (s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <))) \land u \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land s < u) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land u = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \to s \in ℝ^{}$
214	210 213	jca	$⊢ (((((φ \land (s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <))) \land u \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land s < u) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land u = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \to (φ \land s \in ℝ^{})$
215		simpr1r	$⊢ (φ \land ((s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <)) \land u \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land (s < u \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) \land u = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F))) \to s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{*} <)$
216	215	3anassrs	$⊢ (((φ \land (s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <))) \land u \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land (s < u \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) \land u = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \to s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{*} <)$
217	216	3anassrs	$⊢ (((((φ \land (s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <))) \land u \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land s < u) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land u = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \to s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{*} <)$
218	214 217	jca	$⊢ (((((φ \land (s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <))) \land u \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land s < u) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land u = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \to ((φ \land s \in ℝ^{}) \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <))$
219		simpllr	$⊢ (((((φ \land (s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <))) \land u \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land s < u) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land u = \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F) \to s < u$
220		simpr	$⊢ (((((φ \land (s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <))) \land u \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land s < u) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land u = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \to u = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F$
221	219 220	breqtrd	$⊢ (((((φ \land (s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <))) \land u \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land s < u) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land u = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \to s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F$
222		simplr	$⊢ (((((φ \land (s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <))) \land u \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land s < u) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land u = \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F) \to c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)$
223		simpr	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)$
224	223	elin1d	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to c \in 𝒫 ⋃_{j \in A} (\{j\} \times B)$
225		elpwi	$⊢ c \in 𝒫 ⋃_{j \in A} (\{j\} \times B) \to c \subseteq ⋃_{j \in A} (\{j\} \times B)$
226		dmss	$⊢ c \subseteq ⋃_{j \in A} (\{j\} \times B) \to dom c \subseteq dom ⋃_{j \in A} (\{j\} \times B)$
227		dmiun	$⊢ dom ⋃_{j \in A} (\{j\} \times B) = ⋃_{j \in A} dom (\{j\} \times B)$
228	226 227	sseqtrdi	$⊢ c \subseteq ⋃_{j \in A} (\{j\} \times B) \to dom c \subseteq ⋃_{j \in A} dom (\{j\} \times B)$
229		dmxpss	$⊢ dom (\{j\} \times B) \subseteq \{j\}$
230	229	a1i	$⊢ j \in A \to dom (\{j\} \times B) \subseteq \{j\}$
231		snssi	$⊢ j \in A \to \{j\} \subseteq A$
232	230 231	sstrd	$⊢ j \in A \to dom (\{j\} \times B) \subseteq A$
233	232	rgen	$⊢ \forall j \in A dom (\{j\} \times B) \subseteq A$
234		iunss	$⊢ ⋃_{j \in A} dom (\{j\} \times B) \subseteq A \leftrightarrow \forall j \in A dom (\{j\} \times B) \subseteq A$
235	233 234	mpbir	$⊢ ⋃_{j \in A} dom (\{j\} \times B) \subseteq A$
236	228 235	sstrdi	$⊢ c \subseteq ⋃_{j \in A} (\{j\} \times B) \to dom c \subseteq A$
237	23	dmex	$⊢ dom c \in V$
238	237	elpw	$⊢ dom c \in 𝒫 A \leftrightarrow dom c \subseteq A$
239	236 238	sylibr	$⊢ c \subseteq ⋃_{j \in A} (\{j\} \times B) \to dom c \in 𝒫 A$
240	224 225 239	3syl	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to dom c \in 𝒫 A$
241	223	elin2d	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to c \in Fin$
242		dmfi	$⊢ c \in Fin \to dom c \in Fin$
243	241 242	syl	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to dom c \in Fin$
244	240 243	elind	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to dom c \in (𝒫 A \cap Fin)$
245		ovex	$⊢ \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C \in V$
246	245	a1i	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C \in V$
247		mpteq1	$⊢ a = dom c \to (j \in a ⟼ \underset{k \in B}{\sum^{}} C) = (j \in dom c ⟼ \underset{k \in B}{\sum^{}} C)$
248	247	oveq2d	$⊢ a = dom c \to \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C = \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C$
249	192 248	elrnmpt1s	$⊢ (dom c \in (𝒫 A \cap Fin) \land \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C \in V) \to \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C \in ran (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C)$
250	244 246 249	syl2anc	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C \in ran (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C)$
251		simpr	$⊢ ((((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land t = \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C) \to t = \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C$
252	251	breq2d	$⊢ ((((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land t = \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C) \to (s < t \leftrightarrow s < \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C)$
253		simpllr	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to s \in ℝ^{*}$
254	16	a1i	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in CMnd$
255		nfcv	$⊢ \underline{Ⅎ} z (ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])$
256		nfcv	$⊢ \underline{Ⅎ} z Σ_{𝑔}$
257		nfmpt1	$⊢ \underline{Ⅎ} z (z \in c ⟼ F)$
258	255 256 257	nfov	$⊢ \underline{Ⅎ} z (\underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}}, F)$
259	110 111 258	nfbr	$⊢ Ⅎ z s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F$
260	109 259	nfan	$⊢ Ⅎ z ((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)$
261		nfv	$⊢ Ⅎ z c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)$
262	260 261	nfan	$⊢ Ⅎ z (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin))$
263		simp-4l	$⊢ ((((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land z \in c) \to φ$
264	224 225	syl	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to c \subseteq ⋃_{j \in A} (\{j\} \times B)$
265	264	sselda	$⊢ ((((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land z \in c) \to z \in ⋃_{j \in A} (\{j\} \times B)$
266	263 265 49	syl2anc	$⊢ ((((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land z \in c) \to F \in [0, +∞]$
267	266	ex	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to (z \in c \to F \in [0, +∞])$
268	262 267	ralrimi	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \forall z \in c F \in [0, +∞]$
269	15 254 241 268	gsummptcl	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F \in [0, +∞]$
270	14 269	sselid	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F \in ℝ^{}$
271		nfv	$⊢ Ⅎ j ((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)$
272		nfcv	$⊢ \underline{Ⅎ} j c$
273	30	nfpw	$⊢ \underline{Ⅎ} j 𝒫 ⋃_{j \in A} (\{j\} \times B)$
274		nfcv	$⊢ \underline{Ⅎ} j Fin$
275	273 274	nfin	$⊢ \underline{Ⅎ} j (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)$
276	272 275	nfel	$⊢ Ⅎ j c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)$
277	271 276	nfan	$⊢ Ⅎ j (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin))$
278		simpll	$⊢ ((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \to φ$
279	79 236	syl	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to dom c \subseteq A$
280	279	sselda	$⊢ ((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \to j \in A$
281	278 280 161	syl2anc	$⊢ ((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \to \underset{k \in B}{\sum^{*}} C \in [0, +∞]$
282	281	adantllr	$⊢ (((φ \land s \in ℝ^{}) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \to \underset{k \in B}{\sum^{}} C \in [0, +∞]$
283	282	adantllr	$⊢ ((((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \to \underset{k \in B}{\sum^{*}} C \in [0, +∞]$
284	283	ex	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to (j \in dom c \to \underset{k \in B}{\sum^{*}} C \in [0, +∞])$
285	277 284	ralrimi	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \forall j \in dom c \underset{k \in B}{\sum^{*}} C \in [0, +∞]$
286	15 254 243 285	gsummptcl	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C \in [0, +∞]$
287	14 286	sselid	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C \in ℝ^{*}$
288		simplr	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F$
289	28 276	nfan	$⊢ Ⅎ j (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin))$
290		id	$⊢ c \subseteq ⋃_{j \in A} (\{j\} \times B) \to c \subseteq ⋃_{j \in A} (\{j\} \times B)$
291		xpss	$⊢ \{j\} \times B \subseteq V \times V$
292	291	rgenw	$⊢ \forall j \in A \{j\} \times B \subseteq V \times V$
293		iunss	$⊢ ⋃_{j \in A} (\{j\} \times B) \subseteq V \times V \leftrightarrow \forall j \in A \{j\} \times B \subseteq V \times V$
294	292 293	mpbir	$⊢ ⋃_{j \in A} (\{j\} \times B) \subseteq V \times V$
295	294	a1i	$⊢ c \subseteq ⋃_{j \in A} (\{j\} \times B) \to ⋃_{j \in A} (\{j\} \times B) \subseteq V \times V$
296	290 295	sstrd	$⊢ c \subseteq ⋃_{j \in A} (\{j\} \times B) \to c \subseteq V \times V$
297	79 296	syl	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to c \subseteq V \times V$
298		df-rel	$⊢ Rel c \leftrightarrow c \subseteq V \times V$
299	297 298	sylibr	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to Rel c$
300	1 289 15 2 299 19 17 50	gsummpt2d	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F = \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} (\underset{k \in c [\{j\}]}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}}, C)$
301		nfcv	$⊢ \underline{Ⅎ} j dom c$
302	237	a1i	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to dom c \in V$
303	278	adantr	$⊢ (((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \land k \in c [\{j\}]) \to φ$
304	280	adantr	$⊢ (((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \land k \in c [\{j\}]) \to j \in A$
305	79	adantr	$⊢ ((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \to c \subseteq ⋃_{j \in A} (\{j\} \times B)$
306		imass1	$⊢ c \subseteq ⋃_{j \in A} (\{j\} \times B) \to c [\{j\}] \subseteq ⋃_{j \in A} (\{j\} \times B) [\{j\}]$
307	305 306	syl	$⊢ ((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \to c [\{j\}] \subseteq ⋃_{j \in A} (\{j\} \times B) [\{j\}]$
308	3 4	iunsnima	$⊢ (φ \land j \in A) \to ⋃_{j \in A} (\{j\} \times B) [\{j\}] = B$
309	278 280 308	syl2anc	$⊢ ((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \to ⋃_{j \in A} (\{j\} \times B) [\{j\}] = B$
310	307 309	sseqtrd	$⊢ ((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \to c [\{j\}] \subseteq B$
311	310	sselda	$⊢ (((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \land k \in c [\{j\}]) \to k \in B$
312	303 304 311 5	syl12anc	$⊢ (((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \land k \in c [\{j\}]) \to C \in [0, +∞]$
313	312	ralrimiva	$⊢ ((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \to \forall k \in c [\{j\}] C \in [0, +∞]$
314		imaexg	$⊢ c \in V \to c [\{j\}] \in V$
315	23 314	ax-mp	$⊢ c [\{j\}] \in V$
316		nfcv	$⊢ \underline{Ⅎ} k c [\{j\}]$
317	316	esumcl	$⊢ (c [\{j\}] \in V \land \forall k \in c [\{j\}] C \in [0, +∞]) \to \underset{k \in c [\{j\}]}{\sum^{*}} C \in [0, +∞]$
318	315 317	mpan	$⊢ \forall k \in c [\{j\}] C \in [0, +∞] \to \underset{k \in c [\{j\}]}{\sum^{*}} C \in [0, +∞]$
319	313 318	syl	$⊢ ((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \to \underset{k \in c [\{j\}]}{\sum^{*}} C \in [0, +∞]$
320		nfv	$⊢ Ⅎ k ((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c)$
321	278 280 4	syl2anc	$⊢ ((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \to B \in W$
322	278	adantr	$⊢ (((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \land k \in B) \to φ$
323	280	adantr	$⊢ (((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \land k \in B) \to j \in A$
324		simpr	$⊢ (((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \land k \in B) \to k \in B$
325	322 323 324 5	syl12anc	$⊢ (((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \land k \in B) \to C \in [0, +∞]$
326	320 321 325 310	esummono	$⊢ ((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \to \underset{k \in c [\{j\}]}{\sum^{}} C \leq \underset{k \in B}{\sum^{}} C$
327	289 301 302 319 281 326	esumlef	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{j \in dom c}{\sum^{}} \underset{k \in c [\{j\}]}{\sum^{}} C \leq \underset{j \in dom c}{\sum^{}} \underset{k \in B}{\sum^{}} C$
328	19 242	syl	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to dom c \in Fin$
329	289 301 328 319	esumgsum	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{j \in dom c}{\sum^{}} \underset{k \in c [\{j\}]}{\sum^{}} C = \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in c [\{j\}]}{\sum^{}} C$
330	19	adantr	$⊢ ((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \to c \in Fin$
331		imafi2	$⊢ c \in Fin \to c [\{j\}] \in Fin$
332	330 331	syl	$⊢ ((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \to c [\{j\}] \in Fin$
333	320 316 332 312	esumgsum	$⊢ ((φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land j \in dom c) \to \underset{k \in c [\{j\}]}{\sum^{}} C = \underset{k \in c [\{j\}]}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} C$
334	289 333	mpteq2da	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to (j \in dom c ⟼ \underset{k \in c [\{j\}]}{\sum^{}} C) = (j \in dom c ⟼ \underset{k \in c [\{j\}]}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} C)$
335	334	oveq2d	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in c [\{j\}]}{\sum^{}} C = \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} (\underset{k \in c [\{j\}]}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}}, C)$
336	329 335	eqtrd	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{j \in dom c}{\sum^{}} \underset{k \in c [\{j\}]}{\sum^{}} C = \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} (\underset{k \in c [\{j\}]}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}}, C)$
337	289 301 328 281	esumgsum	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{j \in dom c}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C$
338	327 336 337	3brtr3d	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} (\underset{k \in c [\{j\}]}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}}, C) \leq \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C$
339	300 338	eqbrtrd	$⊢ (φ \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F \leq \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{*}} C$
340	339	adantlr	$⊢ ((φ \land s \in ℝ^{}) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F \leq \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C$
341	340	adantlr	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F \leq \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{*}} C$
342	253 270 287 288 341	xrltletrd	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to s < \underset{j \in dom c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C$
343	250 252 342	rspcedvd	$⊢ (((φ \land s \in ℝ^{}) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \exists t \in ran (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C) s < t$
344	343	adantllr	$⊢ ((((φ \land s \in ℝ^{}) \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <)) \land s < \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \to \exists t \in ran (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C) s < t$
345	218 221 222 344	syl21anc	$⊢ (((((φ \land (s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <))) \land u \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land s < u) \land c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin)) \land u = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \to \exists t \in ran (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{*}} C) s < t$
346	55 89	elrnmpti	$⊢ u \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \leftrightarrow \exists c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) u = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F$
347	346	biimpi	$⊢ u \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) \to \exists c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) u = \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F$
348	347	ad2antlr	$⊢ (((φ \land (s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <))) \land u \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land s < u) \to \exists c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) u = \underset{z \in c}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} F$
349	209 345 348	r19.29af	$⊢ (((φ \land (s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <))) \land u \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F)) \land s < u) \to \exists t \in ran (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C) s < t$
350	7 134	suplub	$⊢ φ \to ((s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <)) \to \exists t \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) s < t)$
351	350	imp	$⊢ (φ \land (s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <))) \to \exists t \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) s < t$
352		breq2	$⊢ t = u \to (s < t \leftrightarrow s < u)$
353	352	cbvrexvw	$⊢ \exists t \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) s < t \leftrightarrow \exists u \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) s < u$
354	351 353	sylib	$⊢ (φ \land (s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <))) \to \exists u \in ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) s < u$
355	349 354	r19.29a	$⊢ (φ \land (s \in ℝ^{} \land s < sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{} <))) \to \exists t \in ran (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{*}} C) s < t$
356	7 135 197 355	eqsupd	$⊢ φ \to sup (ran (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C) ℝ^{} <) = sup (ran (c \in (𝒫 ⋃_{j \in A} (\{j\} \times B) \cap Fin) ⟼ \underset{z \in c}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} F) ℝ^{*} <)$
357		nfcv	$⊢ \underline{Ⅎ} j A$
358		eqidd	$⊢ (φ \land a \in (𝒫 A \cap Fin)) \to \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C = \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C$
359	28 357 3 161 358	esumval	$⊢ φ \to \underset{j \in A}{\sum^{}} \underset{k \in B}{\sum^{}} C = sup (ran (a \in (𝒫 A \cap Fin) ⟼ \underset{j \in a}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} \underset{k \in B}{\sum^{}} C) ℝ^{*} <)$
360	356 359 182	3eqtr4d	$⊢ φ \to \underset{j \in A}{\sum^{}} \underset{k \in B}{\sum^{}} C = \underset{z \in ⋃_{j \in A} (\{j\} \times B)}{\sum^{*}} F$

Metamath Proof Explorer

Theorem esum2d

Proof