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