Theorem xrge0tsms 24723

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 13391	. . . . . . . . 9 ⊢ (0[,]+∞) ⊆ ℝ*
3		xrge0tsms.g	. . . . . . . . . . . 12 ⊢ 𝐺 = (ℝ*𝑠 ↾s (0[,]+∞))
4		xrsbas 21295	. . . . . . . . . . . 12 ⊢ ℝ* = (Base‘ℝ*𝑠)
5	3, 4	ressbas2 17208	. . . . . . . . . . 11 ⊢ ((0[,]+∞) ⊆ ℝ* → (0[,]+∞) = (Base‘𝐺))
6	2, 5	ax-mp 5	. . . . . . . . . 10 ⊢ (0[,]+∞) = (Base‘𝐺)
7		eqid 2729	. . . . . . . . . . . 12 ⊢ (ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞}))
8	7	xrge0subm 21324	. . . . . . . . . . 11 ⊢ (0[,]+∞) ∈ (SubMnd‘(ℝ*𝑠 ↾s (ℝ* ∖ {-∞})))
9		xrex 12946	. . . . . . . . . . . . . . 15 ⊢ ℝ* ∈ V
10	9	difexi 5285	. . . . . . . . . . . . . 14 ⊢ (ℝ* ∖ {-∞}) ∈ V
11		simpl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥) → 𝑥 ∈ ℝ*)
12		ge0nemnf 13133	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥) → 𝑥 ≠ -∞)
13	11, 12	jca 511	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥) → (𝑥 ∈ ℝ* ∧ 𝑥 ≠ -∞))
14		elxrge0 13418	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (0[,]+∞) ↔ (𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥))
15		eldifsn 4750	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (ℝ* ∖ {-∞}) ↔ (𝑥 ∈ ℝ* ∧ 𝑥 ≠ -∞))
16	13, 14, 15	3imtr4i 292	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0[,]+∞) → 𝑥 ∈ (ℝ* ∖ {-∞}))
17	16	ssriv 3950	. . . . . . . . . . . . . 14 ⊢ (0[,]+∞) ⊆ (ℝ* ∖ {-∞})
18		ressabs 17218	. . . . . . . . . . . . . 14 ⊢ (((ℝ* ∖ {-∞}) ∈ V ∧ (0[,]+∞) ⊆ (ℝ* ∖ {-∞})) → ((ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ↾s (0[,]+∞)) = (ℝ*𝑠 ↾s (0[,]+∞)))
19	10, 17, 18	mp2an 692	. . . . . . . . . . . . 13 ⊢ ((ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ↾s (0[,]+∞)) = (ℝ*𝑠 ↾s (0[,]+∞))
20	3, 19	eqtr4i 2755	. . . . . . . . . . . 12 ⊢ 𝐺 = ((ℝ*𝑠 ↾s (ℝ* ∖ {-∞})) ↾s (0[,]+∞))
21	7	xrs10 21322	. . . . . . . . . . . 12 ⊢ 0 = (0g‘(ℝ*𝑠 ↾s (ℝ* ∖ {-∞})))
22	20, 21	subm0 18742	. . . . . . . . . . 11 ⊢ ((0[,]+∞) ∈ (SubMnd‘(ℝ*𝑠 ↾s (ℝ* ∖ {-∞}))) → 0 = (0g‘𝐺))
23	8, 22	ax-mp 5	. . . . . . . . . 10 ⊢ 0 = (0g‘𝐺)
24		xrge0cmn 21325	. . . . . . . . . . . 12 ⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ CMnd
25	3, 24	eqeltri 2824	. . . . . . . . . . 11 ⊢ 𝐺 ∈ CMnd
26	25	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐺 ∈ CMnd)
27		elinel2 4165	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) → 𝑠 ∈ Fin)
28	27	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑠 ∈ Fin)
29		xrge0tsms.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝐴⟶(0[,]+∞))
30		elfpw 9305	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑠 ⊆ 𝐴 ∧ 𝑠 ∈ Fin))
31	30	simplbi 497	. . . . . . . . . . 11 ⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) → 𝑠 ⊆ 𝐴)
32		fssres 6726	. . . . . . . . . . 11 ⊢ ((𝐹:𝐴⟶(0[,]+∞) ∧ 𝑠 ⊆ 𝐴) → (𝐹 ↾ 𝑠):𝑠⟶(0[,]+∞))
33	29, 31, 32	syl2an 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑠):𝑠⟶(0[,]+∞))
34		c0ex 11168	. . . . . . . . . . . 12 ⊢ 0 ∈ V
35	34	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 0 ∈ V)
36	33, 28, 35	fdmfifsupp 9326	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑠) finSupp 0)
37	6, 23, 26, 28, 33, 36	gsumcl 19845	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑠)) ∈ (0[,]+∞))
38	2, 37	sselid 3944	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑠)) ∈ ℝ*)
39	38	fmpttd 7087	. . . . . . 7 ⊢ (𝜑 → (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))):(𝒫 𝐴 ∩ Fin)⟶ℝ*)
40	39	frnd 6696	. . . . . 6 ⊢ (𝜑 → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) ⊆ ℝ*)
41		supxrcl 13275	. . . . . 6 ⊢ (ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) ⊆ ℝ* → sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < ) ∈ ℝ*)
42	40, 41	syl 17	. . . . 5 ⊢ (𝜑 → sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < ) ∈ ℝ*)
43	1, 42	eqeltrid 2832	. . . 4 ⊢ (𝜑 → 𝑆 ∈ ℝ*)
44		0ss 4363	. . . . . . . 8 ⊢ ∅ ⊆ 𝐴
45		0fi 9013	. . . . . . . 8 ⊢ ∅ ∈ Fin
46		elfpw 9305	. . . . . . . 8 ⊢ (∅ ∈ (𝒫 𝐴 ∩ Fin) ↔ (∅ ⊆ 𝐴 ∧ ∅ ∈ Fin))
47	44, 45, 46	mpbir2an 711	. . . . . . 7 ⊢ ∅ ∈ (𝒫 𝐴 ∩ Fin)
48		0cn 11166	. . . . . . 7 ⊢ 0 ∈ ℂ
49		eqid 2729	. . . . . . . 8 ⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) = (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))
50		reseq2 5945	. . . . . . . . . . 11 ⊢ (𝑠 = ∅ → (𝐹 ↾ 𝑠) = (𝐹 ↾ ∅))
51		res0 5954	. . . . . . . . . . 11 ⊢ (𝐹 ↾ ∅) = ∅
52	50, 51	eqtrdi 2780	. . . . . . . . . 10 ⊢ (𝑠 = ∅ → (𝐹 ↾ 𝑠) = ∅)
53	52	oveq2d 7403	. . . . . . . . 9 ⊢ (𝑠 = ∅ → (𝐺 Σg (𝐹 ↾ 𝑠)) = (𝐺 Σg ∅))
54	23	gsum0 18611	. . . . . . . . 9 ⊢ (𝐺 Σg ∅) = 0
55	53, 54	eqtrdi 2780	. . . . . . . 8 ⊢ (𝑠 = ∅ → (𝐺 Σg (𝐹 ↾ 𝑠)) = 0)
56	49, 55	elrnmpt1s 5923	. . . . . . 7 ⊢ ((∅ ∈ (𝒫 𝐴 ∩ Fin) ∧ 0 ∈ ℂ) → 0 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))))
57	47, 48, 56	mp2an 692	. . . . . 6 ⊢ 0 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))
58		supxrub 13284	. . . . . 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 5149	. . . 4 ⊢ (𝜑 → 0 ≤ 𝑆)
61		elxrge0 13418	. . . 4 ⊢ (𝑆 ∈ (0[,]+∞) ↔ (𝑆 ∈ ℝ* ∧ 0 ≤ 𝑆))
62	43, 60, 61	sylanbrc 583	. . 3 ⊢ (𝜑 → 𝑆 ∈ (0[,]+∞))
63		letop 23093	. . . . . 6 ⊢ (ordTop‘ ≤ ) ∈ Top
64		ovex 7420	. . . . . 6 ⊢ (0[,]+∞) ∈ V
65		elrest 17390	. . . . . 6 ⊢ (((ordTop‘ ≤ ) ∈ Top ∧ (0[,]+∞) ∈ V) → (𝑢 ∈ ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ↔ ∃𝑣 ∈ (ordTop‘ ≤ )𝑢 = (𝑣 ∩ (0[,]+∞))))
66	63, 64, 65	mp2an 692	. . . . 5 ⊢ (𝑢 ∈ ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ↔ ∃𝑣 ∈ (ordTop‘ ≤ )𝑢 = (𝑣 ∩ (0[,]+∞)))
67		elinel1 4164	. . . . . . . 8 ⊢ (𝑆 ∈ (𝑣 ∩ (0[,]+∞)) → 𝑆 ∈ 𝑣)
68		reex 11159	. . . . . . . . . . . . . 14 ⊢ ℝ ∈ V
69		simplrl 776	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑣 ∈ (ordTop‘ ≤ ))
70		elrestr 17391	. . . . . . . . . . . . . 14 ⊢ (((ordTop‘ ≤ ) ∈ Top ∧ ℝ ∈ V ∧ 𝑣 ∈ (ordTop‘ ≤ )) → (𝑣 ∩ ℝ) ∈ ((ordTop‘ ≤ ) ↾t ℝ))
71	63, 68, 69, 70	mp3an12i 1467	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (𝑣 ∩ ℝ) ∈ ((ordTop‘ ≤ ) ↾t ℝ))
72		eqid 2729	. . . . . . . . . . . . . 14 ⊢ ((ordTop‘ ≤ ) ↾t ℝ) = ((ordTop‘ ≤ ) ↾t ℝ)
73	72	xrtgioo 24695	. . . . . . . . . . . . 13 ⊢ (topGen‘ran (,)) = ((ordTop‘ ≤ ) ↾t ℝ)
74	71, 73	eleqtrrdi 2839	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (𝑣 ∩ ℝ) ∈ (topGen‘ran (,)))
75		simplrr 777	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑆 ∈ 𝑣)
76		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑆 ∈ ℝ)
77	75, 76	elind 4163	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑆 ∈ (𝑣 ∩ ℝ))
78		tg2 22852	. . . . . . . . . . . 12 ⊢ (((𝑣 ∩ ℝ) ∈ (topGen‘ran (,)) ∧ 𝑆 ∈ (𝑣 ∩ ℝ)) → ∃𝑢 ∈ ran (,)(𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)))
79	74, 77, 78	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → ∃𝑢 ∈ ran (,)(𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)))
80		ioof 13408	. . . . . . . . . . . . . 14 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
81		ffn 6688	. . . . . . . . . . . . . 14 ⊢ ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*))
82		ovelrn 7565	. . . . . . . . . . . . . 14 ⊢ ((,) Fn (ℝ* × ℝ*) → (𝑢 ∈ ran (,) ↔ ∃𝑟 ∈ ℝ* ∃𝑤 ∈ ℝ* 𝑢 = (𝑟(,)𝑤)))
83	80, 81, 82	mp2b 10	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ ran (,) ↔ ∃𝑟 ∈ ℝ* ∃𝑤 ∈ ℝ* 𝑢 = (𝑟(,)𝑤))
84		simprrr 781	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ))
85	84	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ))
86		inss1 4200	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 ∩ ℝ) ⊆ 𝑣
87	85, 86	sstrdi 3959	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝑟(,)𝑤) ⊆ 𝑣)
88	25	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝐺 ∈ CMnd)
89		simprrl 780	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
90		elinel2 4165	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin)
91	89, 90	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ∈ Fin)
92		simp-4l 782	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝜑)
93	92, 29	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝐹:𝐴⟶(0[,]+∞))
94		elfpw 9305	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ∈ Fin))
95	94	simplbi 497	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴)
96	89, 95	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ⊆ 𝐴)
97	93, 96	fssresd 6727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑦):𝑦⟶(0[,]+∞))
98	34	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 0 ∈ V)
99	97, 91, 98	fdmfifsupp 9326	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑦) finSupp 0)
100	6, 23, 88, 91, 97, 99	gsumcl 19845	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (0[,]+∞))
101	2, 100	sselid 3944	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ ℝ*)
102		simprll 778	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑟 ∈ ℝ*)
103	102	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑟 ∈ ℝ*)
104		simprrr 781	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ⊆ 𝑦)
105	91, 104	ssfid 9212	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ∈ Fin)
106	104, 96	sstrd 3957	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ⊆ 𝐴)
107	93, 106	fssresd 6727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑧):𝑧⟶(0[,]+∞))
108	107, 105, 98	fdmfifsupp 9326	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑧) finSupp 0)
109	6, 23, 88, 105, 107, 108	gsumcl 19845	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ (0[,]+∞))
110	2, 109	sselid 3944	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ ℝ*)
111		simprlr 779	. . . . . . . . . . . . . . . . . . . . . . . 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 24722	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑧)) ≤ (𝐺 Σg (𝐹 ↾ 𝑦)))
115	103, 110, 101, 111, 114	xrltletrd 13121	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑦)))
116	92, 43	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑆 ∈ ℝ*)
117		simprlr 779	. . . . . . . . . . . . . . . . . . . . . . . . 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 7420	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ V
121		reseq2 5945	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑠 = 𝑦 → (𝐹 ↾ 𝑠) = (𝐹 ↾ 𝑦))
122	121	oveq2d 7403	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑠 = 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑠)) = (𝐺 Σg (𝐹 ↾ 𝑦)))
123	49, 122	elrnmpt1s 5923	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 13284	. . . . . . . . . . . . . . . . . . . . . . . . . 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 5149	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ≤ 𝑆)
128		simprrl 780	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑆 ∈ (𝑟(,)𝑤))
129		eliooord 13366	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 13120	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) < 𝑤)
134		elioo1 13346	. . . . . . . . . . . . . . . . . . . . . . . 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 1343	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑟(,)𝑤))
137	87, 136	sseldd 3947	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣)
138	137, 100	elind 4163	. . . . . . . . . . . . . . . . . . . 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 3125	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) → ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
142	130	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑟 < 𝑆)
143	142, 1	breqtrdi 5148	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < ))
144	40	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) ⊆ ℝ*)
145		supxrlub 13285	. . . . . . . . . . . . . . . . . . . 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 232	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))𝑟 < 𝑤)
148		ovex 7420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ V
149	148	rgenw 3048	. . . . . . . . . . . . . . . . . . 19 ⊢ ∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝐺 Σg (𝐹 ↾ 𝑧)) ∈ V
150		reseq2 5945	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑠 = 𝑧 → (𝐹 ↾ 𝑠) = (𝐹 ↾ 𝑧))
151	150	oveq2d 7403	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 = 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑠)) = (𝐺 Σg (𝐹 ↾ 𝑧)))
152	151	cbvmptv 5211	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) = (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑧)))
153		breq2 5111	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = (𝐺 Σg (𝐹 ↾ 𝑧)) → (𝑟 < 𝑤 ↔ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))))
154	152, 153	rexrnmptw 7067	. . . . . . . . . . . . . . . . . . 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 218	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))
157	141, 156	reximddv 3149	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
158	157	expr 456	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ (𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)) → ((𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))
159		eleq2 2817	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = (𝑟(,)𝑤) → (𝑆 ∈ 𝑢 ↔ 𝑆 ∈ (𝑟(,)𝑤)))
160		sseq1 3972	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = (𝑟(,)𝑤) → (𝑢 ⊆ (𝑣 ∩ ℝ) ↔ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))
161	159, 160	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = (𝑟(,)𝑤) → ((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) ↔ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ))))
162	161	imbi1d 341	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = (𝑟(,)𝑤) → (((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) ↔ ((𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))))
163	158, 162	syl5ibrcom 247	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ (𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)) → (𝑢 = (𝑟(,)𝑤) → ((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))))
164	163	rexlimdvva 3194	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (∃𝑟 ∈ ℝ* ∃𝑤 ∈ ℝ* 𝑢 = (𝑟(,)𝑤) → ((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))))
165	83, 164	biimtrid 242	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (𝑢 ∈ ran (,) → ((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))))
166	165	rexlimdv 3132	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (∃𝑢 ∈ ran (,)(𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))
167	79, 166	mpd 15	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
168		simplrl 776	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → 𝑣 ∈ (ordTop‘ ≤ ))
169		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → 𝑆 = +∞)
170		simplrr 777	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → 𝑆 ∈ 𝑣)
171	169, 170	eqeltrrd 2829	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → +∞ ∈ 𝑣)
172		pnfnei 23107	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ 𝑣) → ∃𝑟 ∈ ℝ (𝑟(,]+∞) ⊆ 𝑣)
173	168, 171, 172	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → ∃𝑟 ∈ ℝ (𝑟(,]+∞) ⊆ 𝑣)
174		simprr 772	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → (𝑟(,]+∞) ⊆ 𝑣)
175	174	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝑟(,]+∞) ⊆ 𝑣)
176	25	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝐺 ∈ CMnd)
177	90	ad2antrl 728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑦 ∈ Fin)
178		simp-5l 784	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝜑)
179	178, 29	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝐹:𝐴⟶(0[,]+∞))
180	95	ad2antrl 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑦 ⊆ 𝐴)
181	179, 180	fssresd 6727	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑦):𝑦⟶(0[,]+∞))
182	34	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 0 ∈ V)
183	181, 177, 182	fdmfifsupp 9326	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑦) finSupp 0)
184	6, 23, 176, 177, 181, 183	gsumcl 19845	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (0[,]+∞))
185	2, 184	sselid 3944	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ ℝ*)
186		rexr 11220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑟 ∈ ℝ → 𝑟 ∈ ℝ*)
187	186	ad2antrl 728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 ∈ ℝ*)
188	187	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑟 ∈ ℝ*)
189		simprr 772	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑧 ⊆ 𝑦)
190	177, 189	ssfid 9212	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑧 ∈ Fin)
191	189, 180	sstrd 3957	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑧 ⊆ 𝐴)
192	179, 191	fssresd 6727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑧):𝑧⟶(0[,]+∞))
193	192, 190, 182	fdmfifsupp 9326	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑧) finSupp 0)
194	6, 23, 176, 190, 192, 193	gsumcl 19845	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ (0[,]+∞))
195	2, 194	sselid 3944	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ ℝ*)
196		simplrr 777	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))
197	178, 112	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝐴 ∈ 𝑉)
198		simprl 770	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
199	3, 197, 179, 198, 189	xrge0gsumle 24722	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑧)) ≤ (𝐺 Σg (𝐹 ↾ 𝑦)))
200	188, 195, 185, 196, 199	xrltletrd 13121	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑦)))
201		pnfge 13090	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ ℝ* → (𝐺 Σg (𝐹 ↾ 𝑦)) ≤ +∞)
202	185, 201	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ≤ +∞)
203		pnfxr 11228	. . . . . . . . . . . . . . . . . 18 ⊢ +∞ ∈ ℝ*
204		elioc1 13348	. . . . . . . . . . . . . . . . . 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 1343	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑟(,]+∞))
207	175, 206	sseldd 3947	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣)
208	207, 184	elind 4163	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))
209	208	expr 456	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
210	209	ralrimiva 3125	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) → ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
211		ltpnf 13080	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 ∈ ℝ → 𝑟 < +∞)
212	211	ad2antrl 728	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 < +∞)
213		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑆 = +∞)
214	212, 213	breqtrrd 5135	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 < 𝑆)
215	214, 1	breqtrdi 5148	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < ))
216	40	ad3antrrr 730	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) ⊆ ℝ*)
217	216, 187, 145	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → (𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < ) ↔ ∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))𝑟 < 𝑤))
218	215, 217	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → ∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))𝑟 < 𝑤)
219	218, 155	sylib 218	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))
220	210, 219	reximddv 3149	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
221	173, 220	rexlimddv 3140	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
222		ge0nemnf 13133	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ ℝ* ∧ 0 ≤ 𝑆) → 𝑆 ≠ -∞)
223	43, 60, 222	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ≠ -∞)
224	43, 223	jca 511	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 ∈ ℝ* ∧ 𝑆 ≠ -∞))
225	224	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) → (𝑆 ∈ ℝ* ∧ 𝑆 ≠ -∞))
226		xrnemnf 13077	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ ℝ* ∧ 𝑆 ≠ -∞) ↔ (𝑆 ∈ ℝ ∨ 𝑆 = +∞))
227	225, 226	sylib 218	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) → (𝑆 ∈ ℝ ∨ 𝑆 = +∞))
228	167, 221, 227	mpjaodan 960	. . . . . . . . 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 2817	. . . . . . . 8 ⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → (𝑆 ∈ 𝑢 ↔ 𝑆 ∈ (𝑣 ∩ (0[,]+∞))))
232		eleq2 2817	. . . . . . . . . 10 ⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢 ↔ (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
233	232	imbi2d 340	. . . . . . . . 9 ⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → ((𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢) ↔ (𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))
234	233	rexralbidv 3203	. . . . . . . 8 ⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → (∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢) ↔ ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))
235	231, 234	imbi12d 344	. . . . . . 7 ⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → ((𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)) ↔ (𝑆 ∈ (𝑣 ∩ (0[,]+∞)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))))
236	230, 235	syl5ibrcom 247	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ (ordTop‘ ≤ )) → (𝑢 = (𝑣 ∩ (0[,]+∞)) → (𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢))))
237	236	rexlimdva 3134	. . . . 5 ⊢ (𝜑 → (∃𝑣 ∈ (ordTop‘ ≤ )𝑢 = (𝑣 ∩ (0[,]+∞)) → (𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢))))
238	66, 237	biimtrid 242	. . . 4 ⊢ (𝜑 → (𝑢 ∈ ((ordTop‘ ≤ ) ↾t (0[,]+∞)) → (𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢))))
239	238	ralrimiv 3124	. . 3 ⊢ (𝜑 → ∀𝑢 ∈ ((ordTop‘ ≤ ) ↾t (0[,]+∞))(𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)))
240		xrstset 21298	. . . . . . 7 ⊢ (ordTop‘ ≤ ) = (TopSet‘ℝ*𝑠)
241	3, 240	resstset 17328	. . . . . 6 ⊢ ((0[,]+∞) ∈ V → (ordTop‘ ≤ ) = (TopSet‘𝐺))
242	64, 241	ax-mp 5	. . . . 5 ⊢ (ordTop‘ ≤ ) = (TopSet‘𝐺)
243	6, 242	topnval 17397	. . . 4 ⊢ ((ordTop‘ ≤ ) ↾t (0[,]+∞)) = (TopOpen‘𝐺)
244		eqid 2729	. . . 4 ⊢ (𝒫 𝐴 ∩ Fin) = (𝒫 𝐴 ∩ Fin)
245	25	a1i 11	. . . 4 ⊢ (𝜑 → 𝐺 ∈ CMnd)
246		xrstps 23096	. . . . . . 7 ⊢ ℝ*𝑠 ∈ TopSp
247		resstps 23074	. . . . . . 7 ⊢ ((ℝ*𝑠 ∈ TopSp ∧ (0[,]+∞) ∈ V) → (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopSp)
248	246, 64, 247	mp2an 692	. . . . . 6 ⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopSp
249	3, 248	eqeltri 2824	. . . . 5 ⊢ 𝐺 ∈ TopSp
250	249	a1i 11	. . . 4 ⊢ (𝜑 → 𝐺 ∈ TopSp)
251	6, 243, 244, 245, 250, 112, 29	eltsms 24020	. . 3 ⊢ (𝜑 → (𝑆 ∈ (𝐺 tsums 𝐹) ↔ (𝑆 ∈ (0[,]+∞) ∧ ∀𝑢 ∈ ((ordTop‘ ≤ ) ↾t (0[,]+∞))(𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)))))
252	62, 239, 251	mpbir2and 713	. 2 ⊢ (𝜑 → 𝑆 ∈ (𝐺 tsums 𝐹))
253		letsr 18552	. . . . 5 ⊢ ≤ ∈ TosetRel
254		ordthaus 23271	. . . . 5 ⊢ ( ≤ ∈ TosetRel → (ordTop‘ ≤ ) ∈ Haus)
255	253, 254	mp1i 13	. . . 4 ⊢ (𝜑 → (ordTop‘ ≤ ) ∈ Haus)
256		resthaus 23255	. . . 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 24024	. 2 ⊢ (𝜑 → (𝑆 ∈ (𝐺 tsums 𝐹) → (𝐺 tsums 𝐹) = {𝑆}))
259	252, 258	mpd 15	1 ⊢ (𝜑 → (𝐺 tsums 𝐹) = {𝑆})

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  Vcvv 3447   ∖ cdif 3911   ∩ cin 3913   ⊆ wss 3914  ∅c0 4296  𝒫 cpw 4563  {csn 4589   class class class wbr 5107   ↦ cmpt 5188   × cxp 5636  ran crn 5639   ↾ cres 5640   Fn wfn 6506  ⟶wf 6507  ‘cfv 6511  (class class class)co 7387  Fincfn 8918  supcsup 9391  ℂcc 11066  ℝcr 11067  0cc0 11068  +∞cpnf 11205  -∞cmnf 11206  ℝ^*cxr 11207   < clt 11208   ≤ cle 11209  (,)cioo 13306  (,]cioc 13307  [,]cicc 13309  Basecbs 17179   ↾_s cress 17200  TopSetcts 17226   ↾_t crest 17383  topGenctg 17400  0_gc0g 17402   Σ_g cgsu 17403  ordTopcordt 17462  ℝ^*_𝑠cxrs 17463   TosetRel ctsr 18524  SubMndcsubmnd 18709  CMndccmn 19710  Topctop 22780  TopSpctps 22819  Hauscha 23195   tsums ctsu 24013

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145  ax-pre-sup 11146

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-tp 4594  df-op 4596  df-uni 4872  df-int 4911  df-iun 4957  df-iin 4958  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-se 5592  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-isom 6520  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-of 7653  df-om 7843  df-1st 7968  df-2nd 7969  df-supp 8140  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-1o 8434  df-2o 8435  df-er 8671  df-map 8801  df-en 8919  df-dom 8920  df-sdom 8921  df-fin 8922  df-fsupp 9313  df-fi 9362  df-sup 9393  df-inf 9394  df-oi 9463  df-card 9892  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-div 11836  df-nn 12187  df-2 12249  df-3 12250  df-4 12251  df-5 12252  df-6 12253  df-7 12254  df-8 12255  df-9 12256  df-n0 12443  df-z 12530  df-dec 12650  df-uz 12794  df-q 12908  df-xadd 13073  df-ioo 13310  df-ioc 13311  df-ico 13312  df-icc 13313  df-fz 13469  df-fzo 13616  df-seq 13967  df-hash 14296  df-struct 17117  df-sets 17134  df-slot 17152  df-ndx 17164  df-base 17180  df-ress 17201  df-plusg 17233  df-mulr 17234  df-tset 17239  df-ple 17240  df-ds 17242  df-rest 17385  df-topn 17386  df-0g 17404  df-gsum 17405  df-topgen 17406  df-ordt 17464  df-xrs 17465  df-mre 17547  df-mrc 17548  df-acs 17550  df-ps 18525  df-tsr 18526  df-mgm 18567  df-sgrp 18646  df-mnd 18662  df-submnd 18711  df-cntz 19249  df-cmn 19712  df-fbas 21261  df-fg 21262  df-top 22781  df-topon 22798  df-topsp 22820  df-bases 22833  df-ntr 22907  df-nei 22985  df-cn 23114  df-haus 23202  df-fil 23733  df-fm 23825  df-flim 23826  df-flf 23827  df-tsms 24014

This theorem is referenced by:  xrge0tsms2  24724  sge0tsms  46378