xrge0tsmsd

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) (Revised by Thierry Arnoux, 30-Jan-2017)

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

Proof

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

Metamath Proof Explorer

Theorem xrge0tsmsd

Proof