Theorem xrge0tsms 23997

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 13162	. . . . . . . . 9 ⊢ (0[,]+∞) ⊆ ℝ*
3		xrge0tsms.g	. . . . . . . . . . . 12 ⊢ 𝐺 = (ℝ*𝑠 ↾s (0[,]+∞))
4		xrsbas 20614	. . . . . . . . . . . 12 ⊢ ℝ* = (Base‘ℝ*𝑠)
5	3, 4	ressbas2 16949	. . . . . . . . . . 11 ⊢ ((0[,]+∞) ⊆ ℝ* → (0[,]+∞) = (Base‘𝐺))
6	2, 5	ax-mp 5	. . . . . . . . . 10 ⊢ (0[,]+∞) = (Base‘𝐺)
7		eqid 2738	. . . . . . . . . . . 12 ⊢ (ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞}))
8	7	xrge0subm 20639	. . . . . . . . . . 11 ⊢ (0[,]+∞) ∈ (SubMnd‘(ℝ*𝑠 ↾s (ℝ* ∖ {-∞})))
9		xrex 12727	. . . . . . . . . . . . . . 15 ⊢ ℝ* ∈ V
10	9	difexi 5252	. . . . . . . . . . . . . 14 ⊢ (ℝ* ∖ {-∞}) ∈ V
11		simpl 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥) → 𝑥 ∈ ℝ*)
12		ge0nemnf 12907	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥) → 𝑥 ≠ -∞)
13	11, 12	jca 512	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥) → (𝑥 ∈ ℝ* ∧ 𝑥 ≠ -∞))
14		elxrge0 13189	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (0[,]+∞) ↔ (𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥))
15		eldifsn 4720	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (ℝ* ∖ {-∞}) ↔ (𝑥 ∈ ℝ* ∧ 𝑥 ≠ -∞))
16	13, 14, 15	3imtr4i 292	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0[,]+∞) → 𝑥 ∈ (ℝ* ∖ {-∞}))
17	16	ssriv 3925	. . . . . . . . . . . . . 14 ⊢ (0[,]+∞) ⊆ (ℝ* ∖ {-∞})
18		ressabs 16959	. . . . . . . . . . . . . 14 ⊢ (((ℝ* ∖ {-∞}) ∈ V ∧ (0[,]+∞) ⊆ (ℝ* ∖ {-∞})) → ((ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ↾s (0[,]+∞)) = (ℝ*𝑠 ↾s (0[,]+∞)))
19	10, 17, 18	mp2an 689	. . . . . . . . . . . . 13 ⊢ ((ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ↾s (0[,]+∞)) = (ℝ*𝑠 ↾s (0[,]+∞))
20	3, 19	eqtr4i 2769	. . . . . . . . . . . 12 ⊢ 𝐺 = ((ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ↾s (0[,]+∞))
21	7	xrs10 20637	. . . . . . . . . . . 12 ⊢ 0 = (0g‘(ℝ*𝑠 ↾s (ℝ* ∖ {-∞})))
22	20, 21	subm0 18454	. . . . . . . . . . 11 ⊢ ((0[,]+∞) ∈ (SubMnd‘(ℝ*𝑠 ↾s (ℝ* ∖ {-∞}))) → 0 = (0g‘𝐺))
23	8, 22	ax-mp 5	. . . . . . . . . 10 ⊢ 0 = (0g‘𝐺)
24		xrge0cmn 20640	. . . . . . . . . . . 12 ⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ CMnd
25	3, 24	eqeltri 2835	. . . . . . . . . . 11 ⊢ 𝐺 ∈ CMnd
26	25	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐺 ∈ CMnd)
27		elinel2 4130	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) → 𝑠 ∈ Fin)
28	27	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑠 ∈ Fin)
29		xrge0tsms.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝐴⟶(0[,]+∞))
30		elfpw 9121	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑠 ⊆ 𝐴 ∧ 𝑠 ∈ Fin))
31	30	simplbi 498	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) → 𝑠 ⊆ 𝐴)
32		fssres 6640	. . . . . . . . . . 11 ⊢ ((𝐹:𝐴⟶(0[,]+∞) ∧ 𝑠 ⊆ 𝐴) → (𝐹 ↾ 𝑠):𝑠⟶(0[,]+∞))
33	29, 31, 32	syl2an 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑠):𝑠⟶(0[,]+∞))
34		c0ex 10969	. . . . . . . . . . . 12 ⊢ 0 ∈ V
35	34	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 0 ∈ V)
36	33, 28, 35	fdmfifsupp 9138	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑠) finSupp 0)
37	6, 23, 26, 28, 33, 36	gsumcl 19516	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑠)) ∈ (0[,]+∞))
38	2, 37	sselid 3919	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑠)) ∈ ℝ*)
39	38	fmpttd 6989	. . . . . . 7 ⊢ (𝜑 → (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))):(𝒫 𝐴 ∩ Fin)⟶ℝ*)
40	39	frnd 6608	. . . . . 6 ⊢ (𝜑 → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) ⊆ ℝ*)
41		supxrcl 13049	. . . . . 6 ⊢ (ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) ⊆ ℝ* → sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < ) ∈ ℝ*)
42	40, 41	syl 17	. . . . 5 ⊢ (𝜑 → sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < ) ∈ ℝ*)
43	1, 42	eqeltrid 2843	. . . 4 ⊢ (𝜑 → 𝑆 ∈ ℝ*)
44		0ss 4330	. . . . . . . 8 ⊢ ∅ ⊆ 𝐴
45		0fin 8954	. . . . . . . 8 ⊢ ∅ ∈ Fin
46		elfpw 9121	. . . . . . . 8 ⊢ (∅ ∈ (𝒫 𝐴 ∩ Fin) ↔ (∅ ⊆ 𝐴 ∧ ∅ ∈ Fin))
47	44, 45, 46	mpbir2an 708	. . . . . . 7 ⊢ ∅ ∈ (𝒫 𝐴 ∩ Fin)
48		0cn 10967	. . . . . . 7 ⊢ 0 ∈ ℂ
49		eqid 2738	. . . . . . . 8 ⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) = (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))
50		reseq2 5886	. . . . . . . . . . 11 ⊢ (𝑠 = ∅ → (𝐹 ↾ 𝑠) = (𝐹 ↾ ∅))
51		res0 5895	. . . . . . . . . . 11 ⊢ (𝐹 ↾ ∅) = ∅
52	50, 51	eqtrdi 2794	. . . . . . . . . 10 ⊢ (𝑠 = ∅ → (𝐹 ↾ 𝑠) = ∅)
53	52	oveq2d 7291	. . . . . . . . 9 ⊢ (𝑠 = ∅ → (𝐺 Σg (𝐹 ↾ 𝑠)) = (𝐺 Σg ∅))
54	23	gsum0 18368	. . . . . . . . 9 ⊢ (𝐺 Σg ∅) = 0
55	53, 54	eqtrdi 2794	. . . . . . . 8 ⊢ (𝑠 = ∅ → (𝐺 Σg (𝐹 ↾ 𝑠)) = 0)
56	49, 55	elrnmpt1s 5866	. . . . . . 7 ⊢ ((∅ ∈ (𝒫 𝐴 ∩ Fin) ∧ 0 ∈ ℂ) → 0 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))))
57	47, 48, 56	mp2an 689	. . . . . 6 ⊢ 0 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))
58		supxrub 13058	. . . . . 6 ⊢ ((ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) ⊆ ℝ* ∧ 0 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))) → 0 ≤ sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < ))
59	40, 57, 58	sylancl 586	. . . . 5 ⊢ (𝜑 → 0 ≤ sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < ))
60	59, 1	breqtrrdi 5116	. . . 4 ⊢ (𝜑 → 0 ≤ 𝑆)
61		elxrge0 13189	. . . 4 ⊢ (𝑆 ∈ (0[,]+∞) ↔ (𝑆 ∈ ℝ* ∧ 0 ≤ 𝑆))
62	43, 60, 61	sylanbrc 583	. . 3 ⊢ (𝜑 → 𝑆 ∈ (0[,]+∞))
63		letop 22357	. . . . . 6 ⊢ (ordTop‘ ≤ ) ∈ Top
64		ovex 7308	. . . . . 6 ⊢ (0[,]+∞) ∈ V
65		elrest 17138	. . . . . 6 ⊢ (((ordTop‘ ≤ ) ∈ Top ∧ (0[,]+∞) ∈ V) → (𝑢 ∈ ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ↔ ∃𝑣 ∈ (ordTop‘ ≤ )𝑢 = (𝑣 ∩ (0[,]+∞))))
66	63, 64, 65	mp2an 689	. . . . 5 ⊢ (𝑢 ∈ ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ↔ ∃𝑣 ∈ (ordTop‘ ≤ )𝑢 = (𝑣 ∩ (0[,]+∞)))
67		elinel1 4129	. . . . . . . 8 ⊢ (𝑆 ∈ (𝑣 ∩ (0[,]+∞)) → 𝑆 ∈ 𝑣)
68		reex 10962	. . . . . . . . . . . . . 14 ⊢ ℝ ∈ V
69		simplrl 774	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑣 ∈ (ordTop‘ ≤ ))
70		elrestr 17139	. . . . . . . . . . . . . 14 ⊢ (((ordTop‘ ≤ ) ∈ Top ∧ ℝ ∈ V ∧ 𝑣 ∈ (ordTop‘ ≤ )) → (𝑣 ∩ ℝ) ∈ ((ordTop‘ ≤ ) ↾t ℝ))
71	63, 68, 69, 70	mp3an12i 1464	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (𝑣 ∩ ℝ) ∈ ((ordTop‘ ≤ ) ↾t ℝ))
72		eqid 2738	. . . . . . . . . . . . . 14 ⊢ ((ordTop‘ ≤ ) ↾t ℝ) = ((ordTop‘ ≤ ) ↾t ℝ)
73	72	xrtgioo 23969	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) = ((ordTop‘ ≤ ) ↾t ℝ)
74	71, 73	eleqtrrdi 2850	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (𝑣 ∩ ℝ) ∈ (topGen‘ran (,)))
75		simplrr 775	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑆 ∈ 𝑣)
76		simpr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑆 ∈ ℝ)
77	75, 76	elind 4128	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑆 ∈ (𝑣 ∩ ℝ))
78		tg2 22115	. . . . . . . . . . . 12 ⊢ (((𝑣 ∩ ℝ) ∈ (topGen‘ran (,)) ∧ 𝑆 ∈ (𝑣 ∩ ℝ)) → ∃𝑢 ∈ ran (,)(𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)))
79	74, 77, 78	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → ∃𝑢 ∈ ran (,)(𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)))
80		ioof 13179	. . . . . . . . . . . . . 14 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
81		ffn 6600	. . . . . . . . . . . . . 14 ⊢ ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*))
82		ovelrn 7448	. . . . . . . . . . . . . 14 ⊢ ((,) Fn (ℝ* × ℝ*) → (𝑢 ∈ ran (,) ↔ ∃𝑟 ∈ ℝ* ∃𝑤 ∈ ℝ* 𝑢 = (𝑟(,)𝑤)))
83	80, 81, 82	mp2b 10	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ ran (,) ↔ ∃𝑟 ∈ ℝ* ∃𝑤 ∈ ℝ* 𝑢 = (𝑟(,)𝑤))
84		simprrr 779	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ))
85	84	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ))
86		inss1 4162	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∩ ℝ) ⊆ 𝑣
87	85, 86	sstrdi 3933	. . . . . . . . . . . . . . . . . . . . . 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 4130	. . . . . . . . . . . . . . . . . . . . . . . . . 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 9121	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ∈ Fin))
95	94	simplbi 498	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴)
96	89, 95	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ⊆ 𝐴)
97	93, 96	fssresd 6641	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑦):𝑦⟶(0[,]+∞))
98	34	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 0 ∈ V)
99	97, 91, 98	fdmfifsupp 9138	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑦) finSupp 0)
100	6, 23, 88, 91, 97, 99	gsumcl 19516	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (0[,]+∞))
101	2, 100	sselid 3919	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ ℝ*)
102		simprll 776	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑟 ∈ ℝ*)
103	102	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑟 ∈ ℝ*)
104		simprrr 779	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ⊆ 𝑦)
105	91, 104	ssfid 9042	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ∈ Fin)
106	104, 96	sstrd 3931	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ⊆ 𝐴)
107	93, 106	fssresd 6641	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑧):𝑧⟶(0[,]+∞))
108	107, 105, 98	fdmfifsupp 9138	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑧) finSupp 0)
109	6, 23, 88, 105, 107, 108	gsumcl 19516	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ (0[,]+∞))
110	2, 109	sselid 3919	. . . . . . . . . . . . . . . . . . . . . . . 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 23996	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑧)) ≤ (𝐺 Σg (𝐹 ↾ 𝑦)))
115	103, 110, 101, 111, 114	xrltletrd 12895	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑦)))
116	92, 43	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑆 ∈ ℝ*)
117		simprlr 777	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑤 ∈ ℝ*)
118	117	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑤 ∈ ℝ*)
119	92, 40	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) ⊆ ℝ*)
120		ovex 7308	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ V
121		reseq2 5886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑠 = 𝑦 → (𝐹 ↾ 𝑠) = (𝐹 ↾ 𝑦))
122	121	oveq2d 7291	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑠 = 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑠)) = (𝐺 Σg (𝐹 ↾ 𝑦)))
123	49, 122	elrnmpt1s 5866	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ V) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))))
124	89, 120, 123	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))))
125		supxrub 13058	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) ⊆ ℝ* ∧ (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ≤ sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < ))
126	119, 124, 125	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ≤ sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < ))
127	126, 1	breqtrrdi 5116	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ≤ 𝑆)
128		simprrl 778	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑆 ∈ (𝑟(,)𝑤))
129		eliooord 13138	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑆 ∈ (𝑟(,)𝑤) → (𝑟 < 𝑆 ∧ 𝑆 < 𝑤))
130	128, 129	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → (𝑟 < 𝑆 ∧ 𝑆 < 𝑤))
131	130	simprd 496	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑆 < 𝑤)
132	131	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑆 < 𝑤)
133	101, 116, 118, 127, 132	xrlelttrd 12894	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) < 𝑤)
134		elioo1 13119	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑟(,)𝑤) ↔ ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ ℝ* ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑦)) ∧ (𝐺 Σg (𝐹 ↾ 𝑦)) < 𝑤)))
135	103, 118, 134	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 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 3922	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣)
138	137, 100	elind 4128	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))
139	138	anassrs 468	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))
140	139	expr 457	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
141	140	ralrimiva 3103	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) → ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
142	130	simpld 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑟 < 𝑆)
143	142, 1	breqtrdi 5115	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < ))
144	40	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) ⊆ ℝ*)
145		supxrlub 13059	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) ⊆ ℝ* ∧ 𝑟 ∈ ℝ*) → (𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < ) ↔ ∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))𝑟 < 𝑤))
146	144, 102, 145	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → (𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < ) ↔ ∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))𝑟 < 𝑤))
147	143, 146	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))𝑟 < 𝑤)
148		ovex 7308	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ V
149	148	rgenw 3076	. . . . . . . . . . . . . . . . . . 19 ⊢ ∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝐺 Σg (𝐹 ↾ 𝑧)) ∈ V
150		reseq2 5886	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = 𝑧 → (𝐹 ↾ 𝑠) = (𝐹 ↾ 𝑧))
151	150	oveq2d 7291	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 = 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑠)) = (𝐺 Σg (𝐹 ↾ 𝑧)))
152	151	cbvmptv 5187	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) = (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑧)))
153		breq2 5078	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = (𝐺 Σg (𝐹 ↾ 𝑧)) → (𝑟 < 𝑤 ↔ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))))
154	152, 153	rexrnmptw 6971	. . . . . . . . . . . . . . . . . . 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 3204	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
158	157	expr 457	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ (𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)) → ((𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))
159		eleq2 2827	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = (𝑟(,)𝑤) → (𝑆 ∈ 𝑢 ↔ 𝑆 ∈ (𝑟(,)𝑤)))
160		sseq1 3946	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = (𝑟(,)𝑤) → (𝑢 ⊆ (𝑣 ∩ ℝ) ↔ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))
161	159, 160	anbi12d 631	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = (𝑟(,)𝑤) → ((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) ↔ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ))))
162	161	imbi1d 342	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (𝑟(,)𝑤) → (((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) ↔ ((𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))))
163	158, 162	syl5ibrcom 246	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ (𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)) → (𝑢 = (𝑟(,)𝑤) → ((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))))
164	163	rexlimdvva 3223	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (∃𝑟 ∈ ℝ* ∃𝑤 ∈ ℝ* 𝑢 = (𝑟(,)𝑤) → ((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))))
165	83, 164	syl5bi 241	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (𝑢 ∈ ran (,) → ((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))))
166	165	rexlimdv 3212	. . . . . . . . . . 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 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → 𝑆 = +∞)
170		simplrr 775	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → 𝑆 ∈ 𝑣)
171	169, 170	eqeltrrd 2840	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → +∞ ∈ 𝑣)
172		pnfnei 22371	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ 𝑣) → ∃𝑟 ∈ ℝ (𝑟(,]+∞) ⊆ 𝑣)
173	168, 171, 172	syl2anc 584	. . . . . . . . . . 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 6641	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑦):𝑦⟶(0[,]+∞))
182	34	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 0 ∈ V)
183	181, 177, 182	fdmfifsupp 9138	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑦) finSupp 0)
184	6, 23, 176, 177, 181, 183	gsumcl 19516	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (0[,]+∞))
185	2, 184	sselid 3919	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ ℝ*)
186		rexr 11021	. . . . . . . . . . . . . . . . . . . 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 9042	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑧 ∈ Fin)
191	189, 180	sstrd 3931	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑧 ⊆ 𝐴)
192	179, 191	fssresd 6641	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑧):𝑧⟶(0[,]+∞))
193	192, 190, 182	fdmfifsupp 9138	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑧) finSupp 0)
194	6, 23, 176, 190, 192, 193	gsumcl 19516	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ (0[,]+∞))
195	2, 194	sselid 3919	. . . . . . . . . . . . . . . . . 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 23996	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑧)) ≤ (𝐺 Σg (𝐹 ↾ 𝑦)))
200	188, 195, 185, 196, 199	xrltletrd 12895	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑦)))
201		pnfge 12866	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ ℝ* → (𝐺 Σg (𝐹 ↾ 𝑦)) ≤ +∞)
202	185, 201	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ≤ +∞)
203		pnfxr 11029	. . . . . . . . . . . . . . . . . 18 ⊢ +∞ ∈ ℝ*
204		elioc1 13121	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑟 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑟(,]+∞) ↔ ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ ℝ* ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑦)) ∧ (𝐺 Σg (𝐹 ↾ 𝑦)) ≤ +∞)))
205	188, 203, 204	sylancl 586	. . . . . . . . . . . . . . . . 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 3922	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣)
208	207, 184	elind 4128	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))
209	208	expr 457	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
210	209	ralrimiva 3103	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) → ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
211		ltpnf 12856	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ ℝ → 𝑟 < +∞)
212	211	ad2antrl 725	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 < +∞)
213		simplr 766	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑆 = +∞)
214	212, 213	breqtrrd 5102	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 < 𝑆)
215	214, 1	breqtrdi 5115	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < ))
216	40	ad3antrrr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) ⊆ ℝ*)
217	216, 187, 145	syl2anc 584	. . . . . . . . . . . . . 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 3204	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
221	173, 220	rexlimddv 3220	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
222		ge0nemnf 12907	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ ℝ* ∧ 0 ≤ 𝑆) → 𝑆 ≠ -∞)
223	43, 60, 222	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ≠ -∞)
224	43, 223	jca 512	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 ∈ ℝ* ∧ 𝑆 ≠ -∞))
225	224	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) → (𝑆 ∈ ℝ* ∧ 𝑆 ≠ -∞))
226		xrnemnf 12853	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ ℝ* ∧ 𝑆 ≠ -∞) ↔ (𝑆 ∈ ℝ ∨ 𝑆 = +∞))
227	225, 226	sylib 217	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) → (𝑆 ∈ ℝ ∨ 𝑆 = +∞))
228	167, 221, 227	mpjaodan 956	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
229	228	expr 457	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑣 ∈ (ordTop‘ ≤ )) → (𝑆 ∈ 𝑣 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))
230	67, 229	syl5 34	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ (ordTop‘ ≤ )) → (𝑆 ∈ (𝑣 ∩ (0[,]+∞)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))
231		eleq2 2827	. . . . . . . 8 ⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → (𝑆 ∈ 𝑢 ↔ 𝑆 ∈ (𝑣 ∩ (0[,]+∞))))
232		eleq2 2827	. . . . . . . . . 10 ⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢 ↔ (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
233	232	imbi2d 341	. . . . . . . . 9 ⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → ((𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢) ↔ (𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))
234	233	rexralbidv 3230	. . . . . . . 8 ⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → (∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢) ↔ ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))
235	231, 234	imbi12d 345	. . . . . . 7 ⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → ((𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)) ↔ (𝑆 ∈ (𝑣 ∩ (0[,]+∞)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))))
236	230, 235	syl5ibrcom 246	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ (ordTop‘ ≤ )) → (𝑢 = (𝑣 ∩ (0[,]+∞)) → (𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢))))
237	236	rexlimdva 3213	. . . . 5 ⊢ (𝜑 → (∃𝑣 ∈ (ordTop‘ ≤ )𝑢 = (𝑣 ∩ (0[,]+∞)) → (𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢))))
238	66, 237	syl5bi 241	. . . 4 ⊢ (𝜑 → (𝑢 ∈ ((ordTop‘ ≤ ) ↾t (0[,]+∞)) → (𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢))))
239	238	ralrimiv 3102	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ ((ordTop‘ ≤ ) ↾t (0[,]+∞))(𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)))
240		xrstset 20617	. . . . . . 7 ⊢ (ordTop‘ ≤ ) = (TopSet‘ℝ*𝑠)
241	3, 240	resstset 17075	. . . . . 6 ⊢ ((0[,]+∞) ∈ V → (ordTop‘ ≤ ) = (TopSet‘𝐺))
242	64, 241	ax-mp 5	. . . . 5 ⊢ (ordTop‘ ≤ ) = (TopSet‘𝐺)
243	6, 242	topnval 17145	. . . 4 ⊢ ((ordTop‘ ≤ ) ↾t (0[,]+∞)) = (TopOpen‘𝐺)
244		eqid 2738	. . . 4 ⊢ (𝒫 𝐴 ∩ Fin) = (𝒫 𝐴 ∩ Fin)
245	25	a1i 11	. . . 4 ⊢ (𝜑 → 𝐺 ∈ CMnd)
246		xrstps 22360	. . . . . . 7 ⊢ ℝ*𝑠 ∈ TopSp
247		resstps 22338	. . . . . . 7 ⊢ ((ℝ*𝑠 ∈ TopSp ∧ (0[,]+∞) ∈ V) → (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopSp)
248	246, 64, 247	mp2an 689	. . . . . 6 ⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopSp
249	3, 248	eqeltri 2835	. . . . 5 ⊢ 𝐺 ∈ TopSp
250	249	a1i 11	. . . 4 ⊢ (𝜑 → 𝐺 ∈ TopSp)
251	6, 243, 244, 245, 250, 112, 29	eltsms 23284	. . 3 ⊢ (𝜑 → (𝑆 ∈ (𝐺 tsums 𝐹) ↔ (𝑆 ∈ (0[,]+∞) ∧ ∀𝑢 ∈ ((ordTop‘ ≤ ) ↾t (0[,]+∞))(𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)))))
252	62, 239, 251	mpbir2and 710	. 2 ⊢ (𝜑 → 𝑆 ∈ (𝐺 tsums 𝐹))
253		letsr 18311	. . . . 5 ⊢ ≤ ∈ TosetRel
254		ordthaus 22535	. . . . 5 ⊢ ( ≤ ∈ TosetRel → (ordTop‘ ≤ ) ∈ Haus)
255	253, 254	mp1i 13	. . . 4 ⊢ (𝜑 → (ordTop‘ ≤ ) ∈ Haus)
256		resthaus 22519	. . . 4 ⊢ (((ordTop‘ ≤ ) ∈ Haus ∧ (0[,]+∞) ∈ V) → ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈ Haus)
257	255, 64, 256	sylancl 586	. . 3 ⊢ (𝜑 → ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈ Haus)
258	6, 245, 250, 112, 29, 243, 257	haustsms2 23288	. 2 ⊢ (𝜑 → (𝑆 ∈ (𝐺 tsums 𝐹) → (𝐺 tsums 𝐹) = {𝑆}))
259	252, 258	mpd 15	1 ⊢ (𝜑 → (𝐺 tsums 𝐹) = {𝑆})

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3065  Vcvv 3432   ∖ cdif 3884   ∩ cin 3886   ⊆ wss 3887  ∅c0 4256  𝒫 cpw 4533  {csn 4561   class class class wbr 5074   ↦ cmpt 5157   × cxp 5587  ran crn 5590   ↾ cres 5591   Fn wfn 6428  ⟶wf 6429  ‘cfv 6433  (class class class)co 7275  Fincfn 8733  supcsup 9199  ℂcc 10869  ℝcr 10870  0cc0 10871  +∞cpnf 11006  -∞cmnf 11007  ℝ^*cxr 11008   < clt 11009   ≤ cle 11010  (,)cioo 13079  (,]cioc 13080  [,]cicc 13082  Basecbs 16912   ↾_s cress 16941  TopSetcts 16968   ↾_t crest 17131  topGenctg 17148  0_gc0g 17150   Σ_g cgsu 17151  ordTopcordt 17210  ℝ^*_𝑠cxrs 17211   TosetRel ctsr 18283  SubMndcsubmnd 18429  CMndccmn 19386  Topctop 22042  TopSpctps 22081  Hauscha 22459   tsums ctsu 23277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948  ax-pre-sup 10949

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-iin 4927  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-of 7533  df-om 7713  df-1st 7831  df-2nd 7832  df-supp 7978  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-er 8498  df-map 8617  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-fsupp 9129  df-fi 9170  df-sup 9201  df-inf 9202  df-oi 9269  df-card 9697  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-4 12038  df-5 12039  df-6 12040  df-7 12041  df-8 12042  df-9 12043  df-n0 12234  df-z 12320  df-dec 12438  df-uz 12583  df-q 12689  df-xadd 12849  df-ioo 13083  df-ioc 13084  df-ico 13085  df-icc 13086  df-fz 13240  df-fzo 13383  df-seq 13722  df-hash 14045  df-struct 16848  df-sets 16865  df-slot 16883  df-ndx 16895  df-base 16913  df-ress 16942  df-plusg 16975  df-mulr 16976  df-tset 16981  df-ple 16982  df-ds 16984  df-rest 17133  df-topn 17134  df-0g 17152  df-gsum 17153  df-topgen 17154  df-ordt 17212  df-xrs 17213  df-mre 17295  df-mrc 17296  df-acs 17298  df-ps 18284  df-tsr 18285  df-mgm 18326  df-sgrp 18375  df-mnd 18386  df-submnd 18431  df-cntz 18923  df-cmn 19388  df-fbas 20594  df-fg 20595  df-top 22043  df-topon 22060  df-topsp 22082  df-bases 22096  df-ntr 22171  df-nei 22249  df-cn 22378  df-haus 22466  df-fil 22997  df-fm 23089  df-flim 23090  df-flf 23091  df-tsms 23278

This theorem is referenced by:  xrge0tsms2  23998  sge0tsms  43918