xrge0tsms - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > xrge0tsms		Structured version Visualization version GIF version

Theorem xrge0tsms 24571

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.)

**Hypotheses**
Ref	Expression
xrge0tsms.g	⊢ 𝐺 = (ℝ^*_𝑠 ↾_s (0[,]+∞))
xrge0tsms.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
xrge0tsms.f	⊢ (𝜑 → 𝐹:𝐴⟶(0[,]+∞))
xrge0tsms.s	⊢ 𝑆 = sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))), ℝ^*, < )

**Assertion**
Ref	Expression
xrge0tsms	⊢ (𝜑 → (𝐺 tsums 𝐹) = {𝑆})

Distinct variable groups: 𝐴,𝑠 𝐹,𝑠 𝜑,𝑠 𝐺,𝑠 Allowed substitution hints: 𝑆(𝑠) 𝑉(𝑠)

Proof of Theorem xrge0tsms Dummy variables 𝑟 𝑢 𝑣 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xrge0tsms.s	. . . . 5 ⊢ 𝑆 = sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))), ℝ^*, < )
2		iccssxr 13412	. . . . . . . . 9 ⊢ (0[,]+∞) ⊆ ℝ^*
3		xrge0tsms.g	. . . . . . . . . . . 12 ⊢ 𝐺 = (ℝ^*_𝑠 ↾_s (0[,]+∞))
4		xrsbas 21162	. . . . . . . . . . . 12 ⊢ ℝ^* = (Base‘ℝ^*_𝑠)
5	3, 4	ressbas2 17187	. . . . . . . . . . 11 ⊢ ((0[,]+∞) ⊆ ℝ^* → (0[,]+∞) = (Base‘𝐺))
6	2, 5	ax-mp 5	. . . . . . . . . 10 ⊢ (0[,]+∞) = (Base‘𝐺)
7		eqid 2731	. . . . . . . . . . . 12 ⊢ (ℝ^_𝑠 ↾_s (ℝ^ ∖ {-∞})) = (ℝ^_𝑠 ↾_s (ℝ^ ∖ {-∞}))
8	7	xrge0subm 21187	. . . . . . . . . . 11 ⊢ (0[,]+∞) ∈ (SubMnd‘(ℝ^_𝑠 ↾_s (ℝ^ ∖ {-∞})))
9		xrex 12976	. . . . . . . . . . . . . . 15 ⊢ ℝ^* ∈ V
10	9	difexi 5329	. . . . . . . . . . . . . 14 ⊢ (ℝ^* ∖ {-∞}) ∈ V
11		simpl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 0 ≤ 𝑥) → 𝑥 ∈ ℝ^*)
12		ge0nemnf 13157	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ^* ∧ 0 ≤ 𝑥) → 𝑥 ≠ -∞)
13	11, 12	jca 511	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ^* ∧ 0 ≤ 𝑥) → (𝑥 ∈ ℝ^* ∧ 𝑥 ≠ -∞))
14		elxrge0 13439	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (0[,]+∞) ↔ (𝑥 ∈ ℝ^* ∧ 0 ≤ 𝑥))
15		eldifsn 4791	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (ℝ^* ∖ {-∞}) ↔ (𝑥 ∈ ℝ^* ∧ 𝑥 ≠ -∞))
16	13, 14, 15	3imtr4i 291	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0[,]+∞) → 𝑥 ∈ (ℝ^* ∖ {-∞}))
17	16	ssriv 3987	. . . . . . . . . . . . . 14 ⊢ (0[,]+∞) ⊆ (ℝ^* ∖ {-∞})
18		ressabs 17199	. . . . . . . . . . . . . 14 ⊢ (((ℝ^* ∖ {-∞}) ∈ V ∧ (0[,]+∞) ⊆ (ℝ^* ∖ {-∞})) → ((ℝ^_𝑠 ↾_s (ℝ^ ∖ {-∞})) ↾_s (0[,]+∞)) = (ℝ^*_𝑠 ↾_s (0[,]+∞)))
19	10, 17, 18	mp2an 689	. . . . . . . . . . . . 13 ⊢ ((ℝ^_𝑠 ↾_s (ℝ^ ∖ {-∞})) ↾_s (0[,]+∞)) = (ℝ^*_𝑠 ↾_s (0[,]+∞))
20	3, 19	eqtr4i 2762	. . . . . . . . . . . 12 ⊢ 𝐺 = ((ℝ^_𝑠 ↾_s (ℝ^ ∖ {-∞})) ↾_s (0[,]+∞))
21	7	xrs10 21185	. . . . . . . . . . . 12 ⊢ 0 = (0_g‘(ℝ^_𝑠 ↾_s (ℝ^ ∖ {-∞})))
22	20, 21	subm0 18733	. . . . . . . . . . 11 ⊢ ((0[,]+∞) ∈ (SubMnd‘(ℝ^_𝑠 ↾_s (ℝ^ ∖ {-∞}))) → 0 = (0_g‘𝐺))
23	8, 22	ax-mp 5	. . . . . . . . . 10 ⊢ 0 = (0_g‘𝐺)
24		xrge0cmn 21188	. . . . . . . . . . . 12 ⊢ (ℝ^*_𝑠 ↾_s (0[,]+∞)) ∈ CMnd
25	3, 24	eqeltri 2828	. . . . . . . . . . 11 ⊢ 𝐺 ∈ CMnd
26	25	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐺 ∈ CMnd)
27		elinel2 4197	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) → 𝑠 ∈ Fin)
28	27	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑠 ∈ Fin)
29		xrge0tsms.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝐴⟶(0[,]+∞))
30		elfpw 9357	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑠 ⊆ 𝐴 ∧ 𝑠 ∈ Fin))
31	30	simplbi 497	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) → 𝑠 ⊆ 𝐴)
32		fssres 6758	. . . . . . . . . . 11 ⊢ ((𝐹:𝐴⟶(0[,]+∞) ∧ 𝑠 ⊆ 𝐴) → (𝐹 ↾ 𝑠):𝑠⟶(0[,]+∞))
33	29, 31, 32	syl2an 595	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑠):𝑠⟶(0[,]+∞))
34		c0ex 11213	. . . . . . . . . . . 12 ⊢ 0 ∈ V
35	34	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 0 ∈ V)
36	33, 28, 35	fdmfifsupp 9376	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑠) finSupp 0)
37	6, 23, 26, 28, 33, 36	gsumcl 19825	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σ_g (𝐹 ↾ 𝑠)) ∈ (0[,]+∞))
38	2, 37	sselid 3981	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σ_g (𝐹 ↾ 𝑠)) ∈ ℝ^*)
39	38	fmpttd 7117	. . . . . . 7 ⊢ (𝜑 → (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))):(𝒫 𝐴 ∩ Fin)⟶ℝ^*)
40	39	frnd 6726	. . . . . 6 ⊢ (𝜑 → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))) ⊆ ℝ^*)
41		supxrcl 13299	. . . . . 6 ⊢ (ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))) ⊆ ℝ^* → sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))), ℝ^, < ) ∈ ℝ^)
42	40, 41	syl 17	. . . . 5 ⊢ (𝜑 → sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))), ℝ^, < ) ∈ ℝ^)
43	1, 42	eqeltrid 2836	. . . 4 ⊢ (𝜑 → 𝑆 ∈ ℝ^*)
44		0ss 4397	. . . . . . . 8 ⊢ ∅ ⊆ 𝐴
45		0fin 9174	. . . . . . . 8 ⊢ ∅ ∈ Fin
46		elfpw 9357	. . . . . . . 8 ⊢ (∅ ∈ (𝒫 𝐴 ∩ Fin) ↔ (∅ ⊆ 𝐴 ∧ ∅ ∈ Fin))
47	44, 45, 46	mpbir2an 708	. . . . . . 7 ⊢ ∅ ∈ (𝒫 𝐴 ∩ Fin)
48		0cn 11211	. . . . . . 7 ⊢ 0 ∈ ℂ
49		eqid 2731	. . . . . . . 8 ⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))) = (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠)))
50		reseq2 5977	. . . . . . . . . . 11 ⊢ (𝑠 = ∅ → (𝐹 ↾ 𝑠) = (𝐹 ↾ ∅))
51		res0 5986	. . . . . . . . . . 11 ⊢ (𝐹 ↾ ∅) = ∅
52	50, 51	eqtrdi 2787	. . . . . . . . . 10 ⊢ (𝑠 = ∅ → (𝐹 ↾ 𝑠) = ∅)
53	52	oveq2d 7428	. . . . . . . . 9 ⊢ (𝑠 = ∅ → (𝐺 Σ_g (𝐹 ↾ 𝑠)) = (𝐺 Σ_g ∅))
54	23	gsum0 18610	. . . . . . . . 9 ⊢ (𝐺 Σ_g ∅) = 0
55	53, 54	eqtrdi 2787	. . . . . . . 8 ⊢ (𝑠 = ∅ → (𝐺 Σ_g (𝐹 ↾ 𝑠)) = 0)
56	49, 55	elrnmpt1s 5957	. . . . . . 7 ⊢ ((∅ ∈ (𝒫 𝐴 ∩ Fin) ∧ 0 ∈ ℂ) → 0 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))))
57	47, 48, 56	mp2an 689	. . . . . 6 ⊢ 0 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠)))
58		supxrub 13308	. . . . . 6 ⊢ ((ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))) ⊆ ℝ^* ∧ 0 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠)))) → 0 ≤ sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))), ℝ^*, < ))
59	40, 57, 58	sylancl 585	. . . . 5 ⊢ (𝜑 → 0 ≤ sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))), ℝ^*, < ))
60	59, 1	breqtrrdi 5191	. . . 4 ⊢ (𝜑 → 0 ≤ 𝑆)
61		elxrge0 13439	. . . 4 ⊢ (𝑆 ∈ (0[,]+∞) ↔ (𝑆 ∈ ℝ^* ∧ 0 ≤ 𝑆))
62	43, 60, 61	sylanbrc 582	. . 3 ⊢ (𝜑 → 𝑆 ∈ (0[,]+∞))
63		letop 22931	. . . . . 6 ⊢ (ordTop‘ ≤ ) ∈ Top
64		ovex 7445	. . . . . 6 ⊢ (0[,]+∞) ∈ V
65		elrest 17378	. . . . . 6 ⊢ (((ordTop‘ ≤ ) ∈ Top ∧ (0[,]+∞) ∈ V) → (𝑢 ∈ ((ordTop‘ ≤ ) ↾_t (0[,]+∞)) ↔ ∃𝑣 ∈ (ordTop‘ ≤ )𝑢 = (𝑣 ∩ (0[,]+∞))))
66	63, 64, 65	mp2an 689	. . . . 5 ⊢ (𝑢 ∈ ((ordTop‘ ≤ ) ↾_t (0[,]+∞)) ↔ ∃𝑣 ∈ (ordTop‘ ≤ )𝑢 = (𝑣 ∩ (0[,]+∞)))
67		elinel1 4196	. . . . . . . 8 ⊢ (𝑆 ∈ (𝑣 ∩ (0[,]+∞)) → 𝑆 ∈ 𝑣)
68		reex 11204	. . . . . . . . . . . . . 14 ⊢ ℝ ∈ V
69		simplrl 774	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑣 ∈ (ordTop‘ ≤ ))
70		elrestr 17379	. . . . . . . . . . . . . 14 ⊢ (((ordTop‘ ≤ ) ∈ Top ∧ ℝ ∈ V ∧ 𝑣 ∈ (ordTop‘ ≤ )) → (𝑣 ∩ ℝ) ∈ ((ordTop‘ ≤ ) ↾_t ℝ))
71	63, 68, 69, 70	mp3an12i 1464	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (𝑣 ∩ ℝ) ∈ ((ordTop‘ ≤ ) ↾_t ℝ))
72		eqid 2731	. . . . . . . . . . . . . 14 ⊢ ((ordTop‘ ≤ ) ↾_t ℝ) = ((ordTop‘ ≤ ) ↾_t ℝ)
73	72	xrtgioo 24543	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) = ((ordTop‘ ≤ ) ↾_t ℝ)
74	71, 73	eleqtrrdi 2843	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (𝑣 ∩ ℝ) ∈ (topGen‘ran (,)))
75		simplrr 775	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑆 ∈ 𝑣)
76		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑆 ∈ ℝ)
77	75, 76	elind 4195	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑆 ∈ (𝑣 ∩ ℝ))
78		tg2 22689	. . . . . . . . . . . 12 ⊢ (((𝑣 ∩ ℝ) ∈ (topGen‘ran (,)) ∧ 𝑆 ∈ (𝑣 ∩ ℝ)) → ∃𝑢 ∈ ran (,)(𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)))
79	74, 77, 78	syl2anc 583	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → ∃𝑢 ∈ ran (,)(𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)))
80		ioof 13429	. . . . . . . . . . . . . 14 ⊢ (,):(ℝ^* × ℝ^*)⟶𝒫 ℝ
81		ffn 6718	. . . . . . . . . . . . . 14 ⊢ ((,):(ℝ^* × ℝ^)⟶𝒫 ℝ → (,) Fn (ℝ^ × ℝ^*))
82		ovelrn 7586	. . . . . . . . . . . . . 14 ⊢ ((,) Fn (ℝ^* × ℝ^) → (𝑢 ∈ ran (,) ↔ ∃𝑟 ∈ ℝ^ ∃𝑤 ∈ ℝ^* 𝑢 = (𝑟(,)𝑤)))
83	80, 81, 82	mp2b 10	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ ran (,) ↔ ∃𝑟 ∈ ℝ^* ∃𝑤 ∈ ℝ^* 𝑢 = (𝑟(,)𝑤))
84		simprrr 779	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ))
85	84	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ))
86		inss1 4229	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∩ ℝ) ⊆ 𝑣
87	85, 86	sstrdi 3995	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝑟(,)𝑤) ⊆ 𝑣)
88	25	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝐺 ∈ CMnd)
89		simprrl 778	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
90		elinel2 4197	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin)
91	89, 90	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ∈ Fin)
92		simp-4l 780	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝜑)
93	92, 29	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝐹:𝐴⟶(0[,]+∞))
94		elfpw 9357	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ∈ Fin))
95	94	simplbi 497	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴)
96	89, 95	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ⊆ 𝐴)
97	93, 96	fssresd 6759	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑦):𝑦⟶(0[,]+∞))
98	34	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 0 ∈ V)
99	97, 91, 98	fdmfifsupp 9376	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑦) finSupp 0)
100	6, 23, 88, 91, 97, 99	gsumcl 19825	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (0[,]+∞))
101	2, 100	sselid 3981	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ ℝ^)
102		simprll 776	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑟 ∈ ℝ^)
103	102	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑟 ∈ ℝ^)
104		simprrr 779	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ⊆ 𝑦)
105	91, 104	ssfid 9270	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ∈ Fin)
106	104, 96	sstrd 3993	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ⊆ 𝐴)
107	93, 106	fssresd 6759	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑧):𝑧⟶(0[,]+∞))
108	107, 105, 98	fdmfifsupp 9376	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑧) finSupp 0)
109	6, 23, 88, 105, 107, 108	gsumcl 19825	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ (0[,]+∞))
110	2, 109	sselid 3981	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ ℝ^)
111		simprlr 777	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))
112		xrge0tsms.a	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
113	92, 112	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝐴 ∈ 𝑉)
114	3, 113, 93, 89, 104	xrge0gsumle 24570	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ≤ (𝐺 Σ_g (𝐹 ↾ 𝑦)))
115	103, 110, 101, 111, 114	xrltletrd 13145	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑦)))
116	92, 43	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑆 ∈ ℝ^)
117		simprlr 777	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑤 ∈ ℝ^)
118	117	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑤 ∈ ℝ^)
119	92, 40	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))) ⊆ ℝ^)
120		ovex 7445	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ V
121		reseq2 5977	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑠 = 𝑦 → (𝐹 ↾ 𝑠) = (𝐹 ↾ 𝑦))
122	121	oveq2d 7428	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑠 = 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑠)) = (𝐺 Σ_g (𝐹 ↾ 𝑦)))
123	49, 122	elrnmpt1s 5957	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ V) → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))))
124	89, 120, 123	sylancl 585	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))))
125		supxrub 13308	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))) ⊆ ℝ^* ∧ (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠)))) → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ≤ sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))), ℝ^*, < ))
126	119, 124, 125	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ≤ sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))), ℝ^, < ))
127	126, 1	breqtrrdi 5191	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ≤ 𝑆)
128		simprrl 778	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑆 ∈ (𝑟(,)𝑤))
129		eliooord 13388	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑆 ∈ (𝑟(,)𝑤) → (𝑟 < 𝑆 ∧ 𝑆 < 𝑤))
130	128, 129	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → (𝑟 < 𝑆 ∧ 𝑆 < 𝑤))
131	130	simprd 495	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑆 < 𝑤)
132	131	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑆 < 𝑤)
133	101, 116, 118, 127, 132	xrlelttrd 13144	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σ_g (𝐹 ↾ 𝑦)) < 𝑤)
134		elioo1 13369	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^) → ((𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑟(,)𝑤) ↔ ((𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ ℝ^ ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∧ (𝐺 Σ_g (𝐹 ↾ 𝑦)) < 𝑤)))
135	103, 118, 134	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → ((𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑟(,)𝑤) ↔ ((𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ ℝ^ ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∧ (𝐺 Σ_g (𝐹 ↾ 𝑦)) < 𝑤)))
136	101, 115, 133, 135	mpbir3and 1341	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑟(,)𝑤))
137	87, 136	sseldd 3984	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ 𝑣)
138	137, 100	elind 4195	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))
139	138	anassrs 467	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))
140	139	expr 456	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
141	140	ralrimiva 3145	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) → ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
142	130	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑟 < 𝑆)
143	142, 1	breqtrdi 5190	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))), ℝ^, < ))
144	40	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))) ⊆ ℝ^)
145		supxrlub 13309	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))) ⊆ ℝ^* ∧ 𝑟 ∈ ℝ^) → (𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))), ℝ^, < ) ↔ ∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠)))𝑟 < 𝑤))
146	144, 102, 145	syl2anc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → (𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))), ℝ^, < ) ↔ ∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠)))𝑟 < 𝑤))
147	143, 146	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠)))𝑟 < 𝑤)
148		ovex 7445	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ V
149	148	rgenw 3064	. . . . . . . . . . . . . . . . . . 19 ⊢ ∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ V
150		reseq2 5977	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = 𝑧 → (𝐹 ↾ 𝑠) = (𝐹 ↾ 𝑧))
151	150	oveq2d 7428	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 = 𝑧 → (𝐺 Σ_g (𝐹 ↾ 𝑠)) = (𝐺 Σ_g (𝐹 ↾ 𝑧)))
152	151	cbvmptv 5262	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))) = (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑧)))
153		breq2 5153	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = (𝐺 Σ_g (𝐹 ↾ 𝑧)) → (𝑟 < 𝑤 ↔ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))))
154	152, 153	rexrnmptw 7097	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ V → (∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠)))𝑟 < 𝑤 ↔ ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧))))
155	149, 154	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠)))𝑟 < 𝑤 ↔ ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))
156	147, 155	sylib 217	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))
157	141, 156	reximddv 3170	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
158	157	expr 456	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ (𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*)) → ((𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))
159		eleq2 2821	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = (𝑟(,)𝑤) → (𝑆 ∈ 𝑢 ↔ 𝑆 ∈ (𝑟(,)𝑤)))
160		sseq1 4008	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = (𝑟(,)𝑤) → (𝑢 ⊆ (𝑣 ∩ ℝ) ↔ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))
161	159, 160	anbi12d 630	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = (𝑟(,)𝑤) → ((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) ↔ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ))))
162	161	imbi1d 340	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (𝑟(,)𝑤) → (((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) ↔ ((𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))))
163	158, 162	syl5ibrcom 246	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ (𝑟 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^*)) → (𝑢 = (𝑟(,)𝑤) → ((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))))
164	163	rexlimdvva 3210	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (∃𝑟 ∈ ℝ^* ∃𝑤 ∈ ℝ^* 𝑢 = (𝑟(,)𝑤) → ((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))))
165	83, 164	biimtrid 241	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (𝑢 ∈ ran (,) → ((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))))
166	165	rexlimdv 3152	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (∃𝑢 ∈ ran (,)(𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))
167	79, 166	mpd 15	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
168		simplrl 774	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → 𝑣 ∈ (ordTop‘ ≤ ))
169		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → 𝑆 = +∞)
170		simplrr 775	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → 𝑆 ∈ 𝑣)
171	169, 170	eqeltrrd 2833	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → +∞ ∈ 𝑣)
172		pnfnei 22945	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ 𝑣) → ∃𝑟 ∈ ℝ (𝑟(,]+∞) ⊆ 𝑣)
173	168, 171, 172	syl2anc 583	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → ∃𝑟 ∈ ℝ (𝑟(,]+∞) ⊆ 𝑣)
174		simprr 770	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → (𝑟(,]+∞) ⊆ 𝑣)
175	174	ad2antrr 723	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝑟(,]+∞) ⊆ 𝑣)
176	25	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝐺 ∈ CMnd)
177	90	ad2antrl 725	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑦 ∈ Fin)
178		simp-5l 782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝜑)
179	178, 29	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝐹:𝐴⟶(0[,]+∞))
180	95	ad2antrl 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑦 ⊆ 𝐴)
181	179, 180	fssresd 6759	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑦):𝑦⟶(0[,]+∞))
182	34	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 0 ∈ V)
183	181, 177, 182	fdmfifsupp 9376	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑦) finSupp 0)
184	6, 23, 176, 177, 181, 183	gsumcl 19825	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (0[,]+∞))
185	2, 184	sselid 3981	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ ℝ^*)
186		rexr 11265	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑟 ∈ ℝ → 𝑟 ∈ ℝ^*)
187	186	ad2antrl 725	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 ∈ ℝ^*)
188	187	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑟 ∈ ℝ^*)
189		simprr 770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑧 ⊆ 𝑦)
190	177, 189	ssfid 9270	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑧 ∈ Fin)
191	189, 180	sstrd 3993	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑧 ⊆ 𝐴)
192	179, 191	fssresd 6759	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑧):𝑧⟶(0[,]+∞))
193	192, 190, 182	fdmfifsupp 9376	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑧) finSupp 0)
194	6, 23, 176, 190, 192, 193	gsumcl 19825	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ (0[,]+∞))
195	2, 194	sselid 3981	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ∈ ℝ^*)
196		simplrr 775	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))
197	178, 112	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝐴 ∈ 𝑉)
198		simprl 768	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
199	3, 197, 179, 198, 189	xrge0gsumle 24570	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σ_g (𝐹 ↾ 𝑧)) ≤ (𝐺 Σ_g (𝐹 ↾ 𝑦)))
200	188, 195, 185, 196, 199	xrltletrd 13145	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑦)))
201		pnfge 13115	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ ℝ^* → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ≤ +∞)
202	185, 201	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ≤ +∞)
203		pnfxr 11273	. . . . . . . . . . . . . . . . . 18 ⊢ +∞ ∈ ℝ^*
204		elioc1 13371	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑟 ∈ ℝ^* ∧ +∞ ∈ ℝ^) → ((𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑟(,]+∞) ↔ ((𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ ℝ^ ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∧ (𝐺 Σ_g (𝐹 ↾ 𝑦)) ≤ +∞)))
205	188, 203, 204	sylancl 585	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → ((𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑟(,]+∞) ↔ ((𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ ℝ^* ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∧ (𝐺 Σ_g (𝐹 ↾ 𝑦)) ≤ +∞)))
206	185, 200, 202, 205	mpbir3and 1341	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑟(,]+∞))
207	175, 206	sseldd 3984	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ 𝑣)
208	207, 184	elind 4195	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))
209	208	expr 456	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
210	209	ralrimiva 3145	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))) → ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
211		ltpnf 13105	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ ℝ → 𝑟 < +∞)
212	211	ad2antrl 725	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 < +∞)
213		simplr 766	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑆 = +∞)
214	212, 213	breqtrrd 5177	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 < 𝑆)
215	214, 1	breqtrdi 5190	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))), ℝ^*, < ))
216	40	ad3antrrr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))) ⊆ ℝ^*)
217	216, 187, 145	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → (𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠))), ℝ^*, < ) ↔ ∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠)))𝑟 < 𝑤))
218	215, 217	mpbid 231	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → ∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σ_g (𝐹 ↾ 𝑠)))𝑟 < 𝑤)
219	218, 155	sylib 217	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)𝑟 < (𝐺 Σ_g (𝐹 ↾ 𝑧)))
220	210, 219	reximddv 3170	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
221	173, 220	rexlimddv 3160	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
222		ge0nemnf 13157	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ ℝ^* ∧ 0 ≤ 𝑆) → 𝑆 ≠ -∞)
223	43, 60, 222	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ≠ -∞)
224	43, 223	jca 511	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 ∈ ℝ^* ∧ 𝑆 ≠ -∞))
225	224	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) → (𝑆 ∈ ℝ^* ∧ 𝑆 ≠ -∞))
226		xrnemnf 13102	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ ℝ^* ∧ 𝑆 ≠ -∞) ↔ (𝑆 ∈ ℝ ∨ 𝑆 = +∞))
227	225, 226	sylib 217	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) → (𝑆 ∈ ℝ ∨ 𝑆 = +∞))
228	167, 221, 227	mpjaodan 956	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
229	228	expr 456	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑣 ∈ (ordTop‘ ≤ )) → (𝑆 ∈ 𝑣 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))
230	67, 229	syl5 34	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ (ordTop‘ ≤ )) → (𝑆 ∈ (𝑣 ∩ (0[,]+∞)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))
231		eleq2 2821	. . . . . . . 8 ⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → (𝑆 ∈ 𝑢 ↔ 𝑆 ∈ (𝑣 ∩ (0[,]+∞))))
232		eleq2 2821	. . . . . . . . . 10 ⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → ((𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ 𝑢 ↔ (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
233	232	imbi2d 339	. . . . . . . . 9 ⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → ((𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ 𝑢) ↔ (𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))
234	233	rexralbidv 3219	. . . . . . . 8 ⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → (∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ 𝑢) ↔ ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))
235	231, 234	imbi12d 343	. . . . . . 7 ⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → ((𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ 𝑢)) ↔ (𝑆 ∈ (𝑣 ∩ (0[,]+∞)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))))
236	230, 235	syl5ibrcom 246	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ (ordTop‘ ≤ )) → (𝑢 = (𝑣 ∩ (0[,]+∞)) → (𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ 𝑢))))
237	236	rexlimdva 3154	. . . . 5 ⊢ (𝜑 → (∃𝑣 ∈ (ordTop‘ ≤ )𝑢 = (𝑣 ∩ (0[,]+∞)) → (𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ 𝑢))))
238	66, 237	biimtrid 241	. . . 4 ⊢ (𝜑 → (𝑢 ∈ ((ordTop‘ ≤ ) ↾_t (0[,]+∞)) → (𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ 𝑢))))
239	238	ralrimiv 3144	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ ((ordTop‘ ≤ ) ↾_t (0[,]+∞))(𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ 𝑢)))
240		xrstset 21165	. . . . . . 7 ⊢ (ordTop‘ ≤ ) = (TopSet‘ℝ^*_𝑠)
241	3, 240	resstset 17315	. . . . . 6 ⊢ ((0[,]+∞) ∈ V → (ordTop‘ ≤ ) = (TopSet‘𝐺))
242	64, 241	ax-mp 5	. . . . 5 ⊢ (ordTop‘ ≤ ) = (TopSet‘𝐺)
243	6, 242	topnval 17385	. . . 4 ⊢ ((ordTop‘ ≤ ) ↾_t (0[,]+∞)) = (TopOpen‘𝐺)
244		eqid 2731	. . . 4 ⊢ (𝒫 𝐴 ∩ Fin) = (𝒫 𝐴 ∩ Fin)
245	25	a1i 11	. . . 4 ⊢ (𝜑 → 𝐺 ∈ CMnd)
246		xrstps 22934	. . . . . . 7 ⊢ ℝ^*_𝑠 ∈ TopSp
247		resstps 22912	. . . . . . 7 ⊢ ((ℝ^_𝑠 ∈ TopSp ∧ (0[,]+∞) ∈ V) → (ℝ^_𝑠 ↾_s (0[,]+∞)) ∈ TopSp)
248	246, 64, 247	mp2an 689	. . . . . 6 ⊢ (ℝ^*_𝑠 ↾_s (0[,]+∞)) ∈ TopSp
249	3, 248	eqeltri 2828	. . . . 5 ⊢ 𝐺 ∈ TopSp
250	249	a1i 11	. . . 4 ⊢ (𝜑 → 𝐺 ∈ TopSp)
251	6, 243, 244, 245, 250, 112, 29	eltsms 23858	. . 3 ⊢ (𝜑 → (𝑆 ∈ (𝐺 tsums 𝐹) ↔ (𝑆 ∈ (0[,]+∞) ∧ ∀𝑢 ∈ ((ordTop‘ ≤ ) ↾_t (0[,]+∞))(𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σ_g (𝐹 ↾ 𝑦)) ∈ 𝑢)))))
252	62, 239, 251	mpbir2and 710	. 2 ⊢ (𝜑 → 𝑆 ∈ (𝐺 tsums 𝐹))
253		letsr 18551	. . . . 5 ⊢ ≤ ∈ TosetRel
254		ordthaus 23109	. . . . 5 ⊢ ( ≤ ∈ TosetRel → (ordTop‘ ≤ ) ∈ Haus)
255	253, 254	mp1i 13	. . . 4 ⊢ (𝜑 → (ordTop‘ ≤ ) ∈ Haus)
256		resthaus 23093	. . . 4 ⊢ (((ordTop‘ ≤ ) ∈ Haus ∧ (0[,]+∞) ∈ V) → ((ordTop‘ ≤ ) ↾_t (0[,]+∞)) ∈ Haus)
257	255, 64, 256	sylancl 585	. . 3 ⊢ (𝜑 → ((ordTop‘ ≤ ) ↾_t (0[,]+∞)) ∈ Haus)
258	6, 245, 250, 112, 29, 243, 257	haustsms2 23862	. 2 ⊢ (𝜑 → (𝑆 ∈ (𝐺 tsums 𝐹) → (𝐺 tsums 𝐹) = {𝑆}))
259	252, 258	mpd 15	1 ⊢ (𝜑 → (𝐺 tsums 𝐹) = {𝑆})

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 844 ∧ w3a 1086 = wceq 1540 ∈ wcel 2105 ≠ wne 2939 ∀wral 3060 ∃wrex 3069 Vcvv 3473 ∖ cdif 3946 ∩ cin 3948 ⊆ wss 3949 ∅c0 4323 𝒫 cpw 4603 {csn 4629 class class class wbr 5149 ↦ cmpt 5232 × cxp 5675 ran crn 5678 ↾ cres 5679 Fn wfn 6539 ⟶wf 6540 ‘cfv 6544 (class class class)co 7412 Fincfn 8942 supcsup 9438 ℂcc 11111 ℝcr 11112 0cc0 11113 +∞cpnf 11250 -∞cmnf 11251 ℝ^*cxr 11252 < clt 11253 ≤ cle 11254 (,)cioo 13329 (,]cioc 13330 [,]cicc 13332 Basecbs 17149 ↾_s cress 17178 TopSetcts 17208 ↾_t crest 17371 topGenctg 17388 0_gc0g 17390 Σ_g cgsu 17391 ordTopcordt 17450 ℝ^*_𝑠cxrs 17451 TosetRel ctsr 18523 SubMndcsubmnd 18705 CMndccmn 19690 Topctop 22616 TopSpctps 22655 Hauscha 23033 tsums ctsu 23851

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7728 ax-cnex 11169 ax-resscn 11170 ax-1cn 11171 ax-icn 11172 ax-addcl 11173 ax-addrcl 11174 ax-mulcl 11175 ax-mulrcl 11176 ax-mulcom 11177 ax-addass 11178 ax-mulass 11179 ax-distr 11180 ax-i2m1 11181 ax-1ne0 11182 ax-1rid 11183 ax-rnegex 11184 ax-rrecex 11185 ax-cnre 11186 ax-pre-lttri 11187 ax-pre-lttrn 11188 ax-pre-ltadd 11189 ax-pre-mulgt0 11190 ax-pre-sup 11191

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-tp 4634 df-op 4636 df-uni 4910 df-int 4952 df-iun 5000 df-iin 5001 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-se 5633 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-isom 6553 df-riota 7368 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7673 df-om 7859 df-1st 7978 df-2nd 7979 df-supp 8150 df-frecs 8269 df-wrecs 8300 df-recs 8374 df-rdg 8413 df-1o 8469 df-er 8706 df-map 8825 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-fsupp 9365 df-fi 9409 df-sup 9440 df-inf 9441 df-oi 9508 df-card 9937 df-pnf 11255 df-mnf 11256 df-xr 11257 df-ltxr 11258 df-le 11259 df-sub 11451 df-neg 11452 df-div 11877 df-nn 12218 df-2 12280 df-3 12281 df-4 12282 df-5 12283 df-6 12284 df-7 12285 df-8 12286 df-9 12287 df-n0 12478 df-z 12564 df-dec 12683 df-uz 12828 df-q 12938 df-xadd 13098 df-ioo 13333 df-ioc 13334 df-ico 13335 df-icc 13336 df-fz 13490 df-fzo 13633 df-seq 13972 df-hash 14296 df-struct 17085 df-sets 17102 df-slot 17120 df-ndx 17132 df-base 17150 df-ress 17179 df-plusg 17215 df-mulr 17216 df-tset 17221 df-ple 17222 df-ds 17224 df-rest 17373 df-topn 17374 df-0g 17392 df-gsum 17393 df-topgen 17394 df-ordt 17452 df-xrs 17453 df-mre 17535 df-mrc 17536 df-acs 17538 df-ps 18524 df-tsr 18525 df-mgm 18566 df-sgrp 18645 df-mnd 18661 df-submnd 18707 df-cntz 19223 df-cmn 19692 df-fbas 21142 df-fg 21143 df-top 22617 df-topon 22634 df-topsp 22656 df-bases 22670 df-ntr 22745 df-nei 22823 df-cn 22952 df-haus 23040 df-fil 23571 df-fm 23663 df-flim 23664 df-flf 23665 df-tsms 23852

This theorem is referenced by: xrge0tsms2 24572 sge0tsms 45396

W3C validator