xrge0tsms

Description: Any finite or infinite sum in the nonnegative extended reals is uniquely convergent to the supremum of all finite sums. (Contributed by Mario Carneiro, 13-Sep-2015) (Proof shortened by AV, 26-Jul-2019)

	Ref	Expression
Hypotheses	xrge0tsms.g	$⊢ G = ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]$
	xrge0tsms.a	$⊢ φ \to A \in V$
	xrge0tsms.f	$⊢ φ \to F : A ⟶ [0, +∞]$
	xrge0tsms.s	$⊢ S = sup (ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) ℝ^{*} <)$
Assertion	xrge0tsms	$⊢ φ \to G tsums F = \{S\}$

Proof

Step	Hyp	Ref	Expression
1		xrge0tsms.g	$⊢ G = ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]$
2		xrge0tsms.a	$⊢ φ \to A \in V$
3		xrge0tsms.f	$⊢ φ \to F : A ⟶ [0, +∞]$
4		xrge0tsms.s	$⊢ S = sup (ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) ℝ^{*} <)$
5		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
6		xrsbas	$⊢ ℝ^{} = {Base}_{ℝ_{𝑠}^{}}$
7	1 6	ressbas2	$⊢ [0, +∞] \subseteq ℝ^{*} \to [0, +∞] = {Base}_{G}$
8	5 7	ax-mp	$⊢ [0, +∞] = {Base}_{G}$
9		eqid	$⊢ ℝ_{𝑠}^{} ↾_{𝑠} (ℝ^{} ∖ \{−∞\}) = ℝ_{𝑠}^{} ↾_{𝑠} (ℝ^{} ∖ \{−∞\})$
10	9	xrge0subm	$⊢ [0, +∞] \in SubMnd (ℝ_{𝑠}^{} ↾_{𝑠} (ℝ^{} ∖ \{−∞\}))$
11		xrex	$⊢ ℝ^{*} \in V$
12	11	difexi	$⊢ ℝ^{*} ∖ \{−∞\} \in V$
13		simpl	$⊢ (x \in ℝ^{} \land 0 \leq x) \to x \in ℝ^{}$
14		ge0nemnf	$⊢ (x \in ℝ^{*} \land 0 \leq x) \to x \neq −∞$
15	13 14	jca	$⊢ (x \in ℝ^{} \land 0 \leq x) \to (x \in ℝ^{} \land x \neq −∞)$
16		elxrge0	$⊢ x \in [0, +∞] \leftrightarrow (x \in ℝ^{*} \land 0 \leq x)$
17		eldifsn	$⊢ x \in (ℝ^{} ∖ \{−∞\}) \leftrightarrow (x \in ℝ^{} \land x \neq −∞)$
18	15 16 17	3imtr4i	$⊢ x \in [0, +∞] \to x \in (ℝ^{*} ∖ \{−∞\})$
19	18	ssriv	$⊢ [0, +∞] \subseteq ℝ^{*} ∖ \{−∞\}$
20		ressabs	$⊢ (ℝ^{} ∖ \{−∞\} \in V \land [0, +∞] \subseteq ℝ^{} ∖ \{−∞\}) \to (ℝ_{𝑠}^{} ↾_{𝑠} (ℝ^{} ∖ \{−∞\})) ↾_{𝑠} [0, +∞] = ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]$
21	12 19 20	mp2an	$⊢ (ℝ_{𝑠}^{} ↾_{𝑠} (ℝ^{} ∖ \{−∞\})) ↾_{𝑠} [0, +∞] = ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]$
22	1 21	eqtr4i	$⊢ G = (ℝ_{𝑠}^{} ↾_{𝑠} (ℝ^{} ∖ \{−∞\})) ↾_{𝑠} [0, +∞]$
23	9	xrs10	$⊢ 0 = 0_{(ℝ_{𝑠}^{} ↾_{𝑠} (ℝ^{} ∖ \{−∞\}))}$
24	22 23	subm0	$⊢ [0, +∞] \in SubMnd (ℝ_{𝑠}^{} ↾_{𝑠} (ℝ^{} ∖ \{−∞\})) \to 0 = 0_{G}$
25	10 24	ax-mp	$⊢ 0 = 0_{G}$
26		xrge0cmn	$⊢ ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in CMnd$
27	1 26	eqeltri	$⊢ G \in CMnd$
28	27	a1i	$⊢ (φ \land s \in (𝒫 A \cap Fin)) \to G \in CMnd$
29		elinel2	$⊢ s \in (𝒫 A \cap Fin) \to s \in Fin$
30	29	adantl	$⊢ (φ \land s \in (𝒫 A \cap Fin)) \to s \in Fin$
31		elfpw	$⊢ s \in (𝒫 A \cap Fin) \leftrightarrow (s \subseteq A \land s \in Fin)$
32	31	simplbi	$⊢ s \in (𝒫 A \cap Fin) \to s \subseteq A$
33		fssres	$⊢ (F : A ⟶ [0, +∞] \land s \subseteq A) \to ({F ↾}_{s}) : s ⟶ [0, +∞]$
34	3 32 33	syl2an	$⊢ (φ \land s \in (𝒫 A \cap Fin)) \to ({F ↾}_{s}) : s ⟶ [0, +∞]$
35		c0ex	$⊢ 0 \in V$
36	35	a1i	$⊢ (φ \land s \in (𝒫 A \cap Fin)) \to 0 \in V$
37	34 30 36	fdmfifsupp	$⊢ (φ \land s \in (𝒫 A \cap Fin)) \to {finSupp}_{0} (({F ↾}_{s}))$
38	8 25 28 30 34 37	gsumcl	$⊢ (φ \land s \in (𝒫 A \cap Fin)) \to \sum_{G} ({F ↾}_{s}) \in [0, +∞]$
39	5 38	sseldi	$⊢ (φ \land s \in (𝒫 A \cap Fin)) \to \sum_{G} ({F ↾}_{s}) \in ℝ^{*}$
40	39	fmpttd	$⊢ φ \to (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) : 𝒫 A \cap Fin ⟶ ℝ^{*}$
41	40	frnd	$⊢ φ \to ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) \subseteq ℝ^{*}$
42		supxrcl	$⊢ ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) \subseteq ℝ^{} \to sup (ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) ℝ^{} <) \in ℝ^{*}$
43	41 42	syl	$⊢ φ \to sup (ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) ℝ^{} <) \in ℝ^{}$
44	4 43	eqeltrid	$⊢ φ \to S \in ℝ^{*}$
45		0ss	$⊢ \emptyset \subseteq A$
46		0fin	$⊢ \emptyset \in Fin$
47		elfpw	$⊢ \emptyset \in (𝒫 A \cap Fin) \leftrightarrow (\emptyset \subseteq A \land \emptyset \in Fin)$
48	45 46 47	mpbir2an	$⊢ \emptyset \in (𝒫 A \cap Fin)$
49		0cn	$⊢ 0 \in ℂ$
50		eqid	$⊢ (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) = (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s}))$
51		reseq2	$⊢ s = \emptyset \to {F ↾}_{s} = {F ↾}_{\emptyset}$
52		res0	$⊢ {F ↾}_{\emptyset} = \emptyset$
53	51 52	eqtrdi	$⊢ s = \emptyset \to {F ↾}_{s} = \emptyset$
54	53	oveq2d	$⊢ s = \emptyset \to \sum_{G} ({F ↾}_{s}) = \sum_{G} \emptyset$
55	25	gsum0	$⊢ \sum_{G} \emptyset = 0$
56	54 55	eqtrdi	$⊢ s = \emptyset \to \sum_{G} ({F ↾}_{s}) = 0$
57	50 56	elrnmpt1s	$⊢ (\emptyset \in (𝒫 A \cap Fin) \land 0 \in ℂ) \to 0 \in ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s}))$
58	48 49 57	mp2an	$⊢ 0 \in ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s}))$
59		supxrub	$⊢ (ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) \subseteq ℝ^{} \land 0 \in ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s}))) \to 0 \leq sup (ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) ℝ^{} <)$
60	41 58 59	sylancl	$⊢ φ \to 0 \leq sup (ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) ℝ^{*} <)$
61	60 4	breqtrrdi	$⊢ φ \to 0 \leq S$
62		elxrge0	$⊢ S \in [0, +∞] \leftrightarrow (S \in ℝ^{*} \land 0 \leq S)$
63	44 61 62	sylanbrc	$⊢ φ \to S \in [0, +∞]$
64		letop	$⊢ ordTop (\leq) \in Top$
65		ovex	$⊢ [0, +∞] \in V$
66		elrest	$⊢ (ordTop (\leq) \in Top \land [0, +∞] \in V) \to (u \in (ordTop (\leq) ↾_{𝑡} [0, +∞]) \leftrightarrow \exists v \in ordTop (\leq) u = v \cap [0, +∞])$
67	64 65 66	mp2an	$⊢ u \in (ordTop (\leq) ↾_{𝑡} [0, +∞]) \leftrightarrow \exists v \in ordTop (\leq) u = v \cap [0, +∞]$
68		elinel1	$⊢ S \in (v \cap [0, +∞]) \to S \in v$
69		reex	$⊢ ℝ \in V$
70		simplrl	$⊢ ((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \to v \in ordTop (\leq)$
71		elrestr	$⊢ (ordTop (\leq) \in Top \land ℝ \in V \land v \in ordTop (\leq)) \to v \cap ℝ \in (ordTop (\leq) ↾_{𝑡} ℝ)$
72	64 69 70 71	mp3an12i	$⊢ ((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \to v \cap ℝ \in (ordTop (\leq) ↾_{𝑡} ℝ)$
73		eqid	$⊢ ordTop (\leq) ↾_{𝑡} ℝ = ordTop (\leq) ↾_{𝑡} ℝ$
74	73	xrtgioo	$⊢ topGen (ran (.)) = ordTop (\leq) ↾_{𝑡} ℝ$
75	72 74	eleqtrrdi	$⊢ ((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \to v \cap ℝ \in topGen (ran (.))$
76		simplrr	$⊢ ((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \to S \in v$
77		simpr	$⊢ ((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \to S \in ℝ$
78	76 77	elind	$⊢ ((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \to S \in (v \cap ℝ)$
79		tg2	$⊢ (v \cap ℝ \in topGen (ran (.)) \land S \in (v \cap ℝ)) \to \exists u \in ran (.) (S \in u \land u \subseteq v \cap ℝ)$
80	75 78 79	syl2anc	$⊢ ((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \to \exists u \in ran (.) (S \in u \land u \subseteq v \cap ℝ)$
81		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
82		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
83		ovelrn	$⊢ (.) Fn (ℝ^{} \times ℝ^{}) \to (u \in ran (.) \leftrightarrow \exists r \in ℝ^{} \exists w \in ℝ^{} u = (r, w))$
84	81 82 83	mp2b	$⊢ u \in ran (.) \leftrightarrow \exists r \in ℝ^{} \exists w \in ℝ^{} u = (r, w)$
85		simprrr	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \to (r, w) \subseteq v \cap ℝ$
86	85	adantr	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to (r, w) \subseteq v \cap ℝ$
87		inss1	$⊢ v \cap ℝ \subseteq v$
88	86 87	sstrdi	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to (r, w) \subseteq v$
89	27	a1i	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to G \in CMnd$
90		simprrl	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to y \in (𝒫 A \cap Fin)$
91		elinel2	$⊢ y \in (𝒫 A \cap Fin) \to y \in Fin$
92	90 91	syl	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to y \in Fin$
93		simp-4l	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to φ$
94	93 3	syl	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to F : A ⟶ [0, +∞]$
95		elfpw	$⊢ y \in (𝒫 A \cap Fin) \leftrightarrow (y \subseteq A \land y \in Fin)$
96	95	simplbi	$⊢ y \in (𝒫 A \cap Fin) \to y \subseteq A$
97	90 96	syl	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to y \subseteq A$
98	94 97	fssresd	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to ({F ↾}_{y}) : y ⟶ [0, +∞]$
99	35	a1i	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to 0 \in V$
100	98 92 99	fdmfifsupp	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to {finSupp}_{0} (({F ↾}_{y}))$
101	8 25 89 92 98 100	gsumcl	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to \sum_{G} ({F ↾}_{y}) \in [0, +∞]$
102	5 101	sseldi	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to \sum_{G} ({F ↾}_{y}) \in ℝ^{*}$
103		simprll	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \to r \in ℝ^{*}$
104	103	adantr	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to r \in ℝ^{*}$
105		simprrr	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to z \subseteq y$
106	92 105	ssfid	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to z \in Fin$
107	105 97	sstrd	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to z \subseteq A$
108	94 107	fssresd	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to ({F ↾}_{z}) : z ⟶ [0, +∞]$
109	108 106 99	fdmfifsupp	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to {finSupp}_{0} (({F ↾}_{z}))$
110	8 25 89 106 108 109	gsumcl	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to \sum_{G} ({F ↾}_{z}) \in [0, +∞]$
111	5 110	sseldi	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to \sum_{G} ({F ↾}_{z}) \in ℝ^{*}$
112		simprlr	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to r < \sum_{G} ({F ↾}_{z})$
113	93 2	syl	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to A \in V$
114	1 113 94 90 105	xrge0gsumle	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to \sum_{G} ({F ↾}_{z}) \leq \sum_{G} ({F ↾}_{y})$
115	104 111 102 112 114	xrltletrd	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to r < \sum_{G} ({F ↾}_{y})$
116	93 44	syl	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to S \in ℝ^{*}$
117		simprlr	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \to w \in ℝ^{*}$
118	117	adantr	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to w \in ℝ^{*}$
119	93 41	syl	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) \subseteq ℝ^{*}$
120		ovex	$⊢ \sum_{G} ({F ↾}_{y}) \in V$
121		reseq2	$⊢ s = y \to {F ↾}_{s} = {F ↾}_{y}$
122	121	oveq2d	$⊢ s = y \to \sum_{G} ({F ↾}_{s}) = \sum_{G} ({F ↾}_{y})$
123	50 122	elrnmpt1s	$⊢ (y \in (𝒫 A \cap Fin) \land \sum_{G} ({F ↾}_{y}) \in V) \to \sum_{G} ({F ↾}_{y}) \in ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s}))$
124	90 120 123	sylancl	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to \sum_{G} ({F ↾}_{y}) \in ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s}))$
125		supxrub	$⊢ (ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) \subseteq ℝ^{} \land \sum_{G} ({F ↾}_{y}) \in ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s}))) \to \sum_{G} ({F ↾}_{y}) \leq sup (ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) ℝ^{} <)$
126	119 124 125	syl2anc	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to \sum_{G} ({F ↾}_{y}) \leq sup (ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) ℝ^{*} <)$
127	126 4	breqtrrdi	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to \sum_{G} ({F ↾}_{y}) \leq S$
128		simprrl	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \to S \in (r, w)$
129		eliooord	$⊢ S \in (r, w) \to (r < S \land S < w)$
130	128 129	syl	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \to (r < S \land S < w)$
131	130	simprd	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \to S < w$
132	131	adantr	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to S < w$
133	102 116 118 127 132	xrlelttrd	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to \sum_{G} ({F ↾}_{y}) < w$
134		elioo1	$⊢ (r \in ℝ^{} \land w \in ℝ^{}) \to (\sum_{G} ({F ↾}_{y}) \in (r, w) \leftrightarrow (\sum_{G} ({F ↾}_{y}) \in ℝ^{*} \land r < \sum_{G} ({F ↾}_{y}) \land \sum_{G} ({F ↾}_{y}) < w))$
135	104 118 134	syl2anc	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to (\sum_{G} ({F ↾}_{y}) \in (r, w) \leftrightarrow (\sum_{G} ({F ↾}_{y}) \in ℝ^{*} \land r < \sum_{G} ({F ↾}_{y}) \land \sum_{G} ({F ↾}_{y}) < w))$
136	102 115 133 135	mpbir3and	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to \sum_{G} ({F ↾}_{y}) \in (r, w)$
137	88 136	sseldd	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to \sum_{G} ({F ↾}_{y}) \in v$
138	137 101	elind	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land ((z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z})) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y))) \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞])$
139	138	anassrs	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞])$
140	139	expr	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land y \in (𝒫 A \cap Fin)) \to (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞]))$
141	140	ralrimiva	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \to \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞]))$
142	130	simpld	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \to r < S$
143	142 4	breqtrdi	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \to r < sup (ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) ℝ^{*} <)$
144	41	ad3antrrr	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \to ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) \subseteq ℝ^{*}$
145		supxrlub	$⊢ (ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) \subseteq ℝ^{} \land r \in ℝ^{}) \to (r < sup (ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) ℝ^{*} <) \leftrightarrow \exists w \in ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) r < w)$
146	144 103 145	syl2anc	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \to (r < sup (ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) ℝ^{*} <) \leftrightarrow \exists w \in ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) r < w)$
147	143 146	mpbid	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \to \exists w \in ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) r < w$
148		ovex	$⊢ \sum_{G} ({F ↾}_{z}) \in V$
149	148	rgenw	$⊢ \forall z \in (𝒫 A \cap Fin) \sum_{G} ({F ↾}_{z}) \in V$
150		reseq2	$⊢ s = z \to {F ↾}_{s} = {F ↾}_{z}$
151	150	oveq2d	$⊢ s = z \to \sum_{G} ({F ↾}_{s}) = \sum_{G} ({F ↾}_{z})$
152	151	cbvmptv	$⊢ (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) = (z \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{z}))$
153		breq2	$⊢ w = \sum_{G} ({F ↾}_{z}) \to (r < w \leftrightarrow r < \sum_{G} ({F ↾}_{z}))$
154	152 153	rexrnmptw	$⊢ \forall z \in (𝒫 A \cap Fin) \sum_{G} ({F ↾}_{z}) \in V \to (\exists w \in ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) r < w \leftrightarrow \exists z \in (𝒫 A \cap Fin) r < \sum_{G} ({F ↾}_{z}))$
155	149 154	ax-mp	$⊢ \exists w \in ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) r < w \leftrightarrow \exists z \in (𝒫 A \cap Fin) r < \sum_{G} ({F ↾}_{z})$
156	147 155	sylib	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \to \exists z \in (𝒫 A \cap Fin) r < \sum_{G} ({F ↾}_{z})$
157	141 156	reximddv	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land ((r \in ℝ^{} \land w \in ℝ^{}) \land (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))) \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞]))$
158	157	expr	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land (r \in ℝ^{} \land w \in ℝ^{})) \to ((S \in (r, w) \land (r, w) \subseteq v \cap ℝ) \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞])))$
159		eleq2	$⊢ u = (r, w) \to (S \in u \leftrightarrow S \in (r, w))$
160		sseq1	$⊢ u = (r, w) \to (u \subseteq v \cap ℝ \leftrightarrow (r, w) \subseteq v \cap ℝ)$
161	159 160	anbi12d	$⊢ u = (r, w) \to ((S \in u \land u \subseteq v \cap ℝ) \leftrightarrow (S \in (r, w) \land (r, w) \subseteq v \cap ℝ))$
162	161	imbi1d	$⊢ u = (r, w) \to (((S \in u \land u \subseteq v \cap ℝ) \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞]))) \leftrightarrow ((S \in (r, w) \land (r, w) \subseteq v \cap ℝ) \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞]))))$
163	158 162	syl5ibrcom	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \land (r \in ℝ^{} \land w \in ℝ^{})) \to (u = (r, w) \to ((S \in u \land u \subseteq v \cap ℝ) \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞]))))$
164	163	rexlimdvva	$⊢ ((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \to (\exists r \in ℝ^{} \exists w \in ℝ^{} u = (r, w) \to ((S \in u \land u \subseteq v \cap ℝ) \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞]))))$
165	84 164	syl5bi	$⊢ ((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \to (u \in ran (.) \to ((S \in u \land u \subseteq v \cap ℝ) \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞]))))$
166	165	rexlimdv	$⊢ ((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \to (\exists u \in ran (.) (S \in u \land u \subseteq v \cap ℝ) \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞])))$
167	80 166	mpd	$⊢ ((φ \land (v \in ordTop (\leq) \land S \in v)) \land S \in ℝ) \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞]))$
168		simplrl	$⊢ ((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \to v \in ordTop (\leq)$
169		simpr	$⊢ ((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \to S = +∞$
170		simplrr	$⊢ ((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \to S \in v$
171	169 170	eqeltrrd	$⊢ ((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \to +∞ \in v$
172		pnfnei	$⊢ (v \in ordTop (\leq) \land +∞ \in v) \to \exists r \in ℝ (r, +∞] \subseteq v$
173	168 171 172	syl2anc	$⊢ ((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \to \exists r \in ℝ (r, +∞] \subseteq v$
174		simprr	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \to (r, +∞] \subseteq v$
175	174	ad2antrr	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to (r, +∞] \subseteq v$
176	27	a1i	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to G \in CMnd$
177	91	ad2antrl	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to y \in Fin$
178		simp-5l	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to φ$
179	178 3	syl	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to F : A ⟶ [0, +∞]$
180	96	ad2antrl	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to y \subseteq A$
181	179 180	fssresd	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to ({F ↾}_{y}) : y ⟶ [0, +∞]$
182	35	a1i	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to 0 \in V$
183	181 177 182	fdmfifsupp	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to {finSupp}_{0} (({F ↾}_{y}))$
184	8 25 176 177 181 183	gsumcl	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to \sum_{G} ({F ↾}_{y}) \in [0, +∞]$
185	5 184	sseldi	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to \sum_{G} ({F ↾}_{y}) \in ℝ^{*}$
186		rexr	$⊢ r \in ℝ \to r \in ℝ^{*}$
187	186	ad2antrl	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \to r \in ℝ^{*}$
188	187	ad2antrr	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to r \in ℝ^{*}$
189		simprr	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to z \subseteq y$
190	177 189	ssfid	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to z \in Fin$
191	189 180	sstrd	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to z \subseteq A$
192	179 191	fssresd	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to ({F ↾}_{z}) : z ⟶ [0, +∞]$
193	192 190 182	fdmfifsupp	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to {finSupp}_{0} (({F ↾}_{z}))$
194	8 25 176 190 192 193	gsumcl	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to \sum_{G} ({F ↾}_{z}) \in [0, +∞]$
195	5 194	sseldi	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to \sum_{G} ({F ↾}_{z}) \in ℝ^{*}$
196		simplrr	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to r < \sum_{G} ({F ↾}_{z})$
197	178 2	syl	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to A \in V$
198		simprl	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to y \in (𝒫 A \cap Fin)$
199	1 197 179 198 189	xrge0gsumle	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to \sum_{G} ({F ↾}_{z}) \leq \sum_{G} ({F ↾}_{y})$
200	188 195 185 196 199	xrltletrd	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to r < \sum_{G} ({F ↾}_{y})$
201		pnfge	$⊢ \sum_{G} ({F ↾}_{y}) \in ℝ^{*} \to \sum_{G} ({F ↾}_{y}) \leq +∞$
202	185 201	syl	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to \sum_{G} ({F ↾}_{y}) \leq +∞$
203		pnfxr	$⊢ +∞ \in ℝ^{*}$
204		elioc1	$⊢ (r \in ℝ^{} \land +∞ \in ℝ^{}) \to (\sum_{G} ({F ↾}_{y}) \in (r, +∞] \leftrightarrow (\sum_{G} ({F ↾}_{y}) \in ℝ^{*} \land r < \sum_{G} ({F ↾}_{y}) \land \sum_{G} ({F ↾}_{y}) \leq +∞))$
205	188 203 204	sylancl	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to (\sum_{G} ({F ↾}_{y}) \in (r, +∞] \leftrightarrow (\sum_{G} ({F ↾}_{y}) \in ℝ^{*} \land r < \sum_{G} ({F ↾}_{y}) \land \sum_{G} ({F ↾}_{y}) \leq +∞))$
206	185 200 202 205	mpbir3and	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to \sum_{G} ({F ↾}_{y}) \in (r, +∞]$
207	175 206	sseldd	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to \sum_{G} ({F ↾}_{y}) \in v$
208	207 184	elind	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land (y \in (𝒫 A \cap Fin) \land z \subseteq y)) \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞])$
209	208	expr	$⊢ (((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \land y \in (𝒫 A \cap Fin)) \to (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞]))$
210	209	ralrimiva	$⊢ ((((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \land (z \in (𝒫 A \cap Fin) \land r < \sum_{G} ({F ↾}_{z}))) \to \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞]))$
211		ltpnf	$⊢ r \in ℝ \to r < +∞$
212	211	ad2antrl	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \to r < +∞$
213		simplr	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \to S = +∞$
214	212 213	breqtrrd	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \to r < S$
215	214 4	breqtrdi	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \to r < sup (ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) ℝ^{*} <)$
216	41	ad3antrrr	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \to ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) \subseteq ℝ^{*}$
217	216 187 145	syl2anc	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \to (r < sup (ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) ℝ^{*} <) \leftrightarrow \exists w \in ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) r < w)$
218	215 217	mpbid	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \to \exists w \in ran (s \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{s})) r < w$
219	218 155	sylib	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \to \exists z \in (𝒫 A \cap Fin) r < \sum_{G} ({F ↾}_{z})$
220	210 219	reximddv	$⊢ (((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \land (r \in ℝ \land (r, +∞] \subseteq v)) \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞]))$
221	173 220	rexlimddv	$⊢ ((φ \land (v \in ordTop (\leq) \land S \in v)) \land S = +∞) \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞]))$
222		ge0nemnf	$⊢ (S \in ℝ^{*} \land 0 \leq S) \to S \neq −∞$
223	44 61 222	syl2anc	$⊢ φ \to S \neq −∞$
224	44 223	jca	$⊢ φ \to (S \in ℝ^{*} \land S \neq −∞)$
225	224	adantr	$⊢ (φ \land (v \in ordTop (\leq) \land S \in v)) \to (S \in ℝ^{*} \land S \neq −∞)$
226		xrnemnf	$⊢ (S \in ℝ^{*} \land S \neq −∞) \leftrightarrow (S \in ℝ \lor S = +∞)$
227	225 226	sylib	$⊢ (φ \land (v \in ordTop (\leq) \land S \in v)) \to (S \in ℝ \lor S = +∞)$
228	167 221 227	mpjaodan	$⊢ (φ \land (v \in ordTop (\leq) \land S \in v)) \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞]))$
229	228	expr	$⊢ (φ \land v \in ordTop (\leq)) \to (S \in v \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞])))$
230	68 229	syl5	$⊢ (φ \land v \in ordTop (\leq)) \to (S \in (v \cap [0, +∞]) \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞])))$
231		eleq2	$⊢ u = v \cap [0, +∞] \to (S \in u \leftrightarrow S \in (v \cap [0, +∞]))$
232		eleq2	$⊢ u = v \cap [0, +∞] \to (\sum_{G} ({F ↾}_{y}) \in u \leftrightarrow \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞]))$
233	232	imbi2d	$⊢ u = v \cap [0, +∞] \to ((z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u) \leftrightarrow (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞])))$
234	233	rexralbidv	$⊢ u = v \cap [0, +∞] \to (\exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u) \leftrightarrow \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞])))$
235	231 234	imbi12d	$⊢ u = v \cap [0, +∞] \to ((S \in u \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u)) \leftrightarrow (S \in (v \cap [0, +∞]) \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in (v \cap [0, +∞]))))$
236	230 235	syl5ibrcom	$⊢ (φ \land v \in ordTop (\leq)) \to (u = v \cap [0, +∞] \to (S \in u \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u)))$
237	236	rexlimdva	$⊢ φ \to (\exists v \in ordTop (\leq) u = v \cap [0, +∞] \to (S \in u \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u)))$
238	67 237	syl5bi	$⊢ φ \to (u \in (ordTop (\leq) ↾_{𝑡} [0, +∞]) \to (S \in u \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u)))$
239	238	ralrimiv	$⊢ φ \to \forall u \in (ordTop (\leq) ↾_{𝑡} [0, +∞]) (S \in u \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u))$
240		xrstset	$⊢ ordTop (\leq) = TopSet (ℝ_{𝑠}^{*})$
241	1 240	resstset	$⊢ [0, +∞] \in V \to ordTop (\leq) = TopSet (G)$
242	65 241	ax-mp	$⊢ ordTop (\leq) = TopSet (G)$
243	8 242	topnval	$⊢ ordTop (\leq) ↾_{𝑡} [0, +∞] = TopOpen (G)$
244		eqid	$⊢ 𝒫 A \cap Fin = 𝒫 A \cap Fin$
245	27	a1i	$⊢ φ \to G \in CMnd$
246		xrstps	$⊢ ℝ_{𝑠}^{*} \in TopSp$
247		resstps	$⊢ (ℝ_{𝑠}^{} \in TopSp \land [0, +∞] \in V) \to ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞] \in TopSp$
248	246 65 247	mp2an	$⊢ ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in TopSp$
249	1 248	eqeltri	$⊢ G \in TopSp$
250	249	a1i	$⊢ φ \to G \in TopSp$
251	8 243 244 245 250 2 3	eltsms	$⊢ φ \to (S \in (G tsums F) \leftrightarrow (S \in [0, +∞] \land \forall u \in (ordTop (\leq) ↾_{𝑡} [0, +∞]) (S \in u \to \exists z \in (𝒫 A \cap Fin) \forall y \in (𝒫 A \cap Fin) (z \subseteq y \to \sum_{G} ({F ↾}_{y}) \in u))))$
252	63 239 251	mpbir2and	$⊢ φ \to S \in (G tsums F)$
253		letsr	$⊢ \leq \in TosetRel$
254		ordthaus	$⊢ \leq \in TosetRel \to ordTop (\leq) \in Haus$
255	253 254	mp1i	$⊢ φ \to ordTop (\leq) \in Haus$
256		resthaus	$⊢ (ordTop (\leq) \in Haus \land [0, +∞] \in V) \to ordTop (\leq) ↾_{𝑡} [0, +∞] \in Haus$
257	255 65 256	sylancl	$⊢ φ \to ordTop (\leq) ↾_{𝑡} [0, +∞] \in Haus$
258	8 245 250 2 3 243 257	haustsms2	$⊢ φ \to (S \in (G tsums F) \to G tsums F = \{S\})$
259	252 258	mpd	$⊢ φ \to G tsums F = \{S\}$

Metamath Proof Explorer

Theorem xrge0tsms

Proof