Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  xrge0tsmsd Structured version   Visualization version   GIF version

Theorem xrge0tsmsd 29570
Description: Any finite or infinite sum in the nonnegative extended reals is uniquely convergent to the supremum of all finite sums. (Contributed by Mario Carneiro, 13-Sep-2015.) (Revised by Thierry Arnoux, 30-Jan-2017.)
Hypotheses
Ref Expression
xrge0tsmsd.g 𝐺 = (ℝ*𝑠s (0[,]+∞))
xrge0tsmsd.a (𝜑𝐴𝑉)
xrge0tsmsd.f (𝜑𝐹:𝐴⟶(0[,]+∞))
xrge0tsmsd.s (𝜑𝑆 = sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))), ℝ*, < ))
Assertion
Ref Expression
xrge0tsmsd (𝜑 → (𝐺 tsums 𝐹) = {𝑆})
Distinct variable groups:   𝐴,𝑠   𝐹,𝑠   𝜑,𝑠   𝐺,𝑠
Allowed substitution hints:   𝑆(𝑠)   𝑉(𝑠)

Proof of Theorem xrge0tsmsd
Dummy variables 𝑟 𝑢 𝑣 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xrge0tsmsd.s . . . . 5 (𝜑𝑆 = sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))), ℝ*, < ))
2 iccssxr 12198 . . . . . . . . 9 (0[,]+∞) ⊆ ℝ*
3 xrge0tsmsd.g . . . . . . . . . . . 12 𝐺 = (ℝ*𝑠s (0[,]+∞))
4 xrsbas 19681 . . . . . . . . . . . 12 * = (Base‘ℝ*𝑠)
53, 4ressbas2 15852 . . . . . . . . . . 11 ((0[,]+∞) ⊆ ℝ* → (0[,]+∞) = (Base‘𝐺))
62, 5ax-mp 5 . . . . . . . . . 10 (0[,]+∞) = (Base‘𝐺)
7 eqid 2621 . . . . . . . . . 10 (0g𝐺) = (0g𝐺)
8 xrge0cmn 19707 . . . . . . . . . . . 12 (ℝ*𝑠s (0[,]+∞)) ∈ CMnd
93, 8eqeltri 2694 . . . . . . . . . . 11 𝐺 ∈ CMnd
109a1i 11 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐺 ∈ CMnd)
11 simpr 477 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑠 ∈ (𝒫 𝐴 ∩ Fin))
12 xrge0tsmsd.f . . . . . . . . . . 11 (𝜑𝐹:𝐴⟶(0[,]+∞))
13 elfpw 8212 . . . . . . . . . . . 12 (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑠𝐴𝑠 ∈ Fin))
1413simplbi 476 . . . . . . . . . . 11 (𝑠 ∈ (𝒫 𝐴 ∩ Fin) → 𝑠𝐴)
15 fssres 6027 . . . . . . . . . . 11 ((𝐹:𝐴⟶(0[,]+∞) ∧ 𝑠𝐴) → (𝐹𝑠):𝑠⟶(0[,]+∞))
1612, 14, 15syl2an 494 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹𝑠):𝑠⟶(0[,]+∞))
17 elinel2 3778 . . . . . . . . . . . 12 (𝑠 ∈ (𝒫 𝐴 ∩ Fin) → 𝑠 ∈ Fin)
1817adantl 482 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑠 ∈ Fin)
19 fvex 6158 . . . . . . . . . . . 12 (0g𝐺) ∈ V
2019a1i 11 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (0g𝐺) ∈ V)
2116, 18, 20fdmfifsupp 8229 . . . . . . . . . 10 ((𝜑𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹𝑠) finSupp (0g𝐺))
226, 7, 10, 11, 16, 21gsumcl 18237 . . . . . . . . 9 ((𝜑𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹𝑠)) ∈ (0[,]+∞))
232, 22sseldi 3581 . . . . . . . 8 ((𝜑𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹𝑠)) ∈ ℝ*)
24 eqid 2621 . . . . . . . 8 (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))) = (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠)))
2523, 24fmptd 6340 . . . . . . 7 (𝜑 → (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))):(𝒫 𝐴 ∩ Fin)⟶ℝ*)
26 frn 6010 . . . . . . 7 ((𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))):(𝒫 𝐴 ∩ Fin)⟶ℝ* → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))) ⊆ ℝ*)
2725, 26syl 17 . . . . . 6 (𝜑 → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))) ⊆ ℝ*)
28 supxrcl 12088 . . . . . 6 (ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))) ⊆ ℝ* → sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))), ℝ*, < ) ∈ ℝ*)
2927, 28syl 17 . . . . 5 (𝜑 → sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))), ℝ*, < ) ∈ ℝ*)
301, 29eqeltrd 2698 . . . 4 (𝜑𝑆 ∈ ℝ*)
31 0ss 3944 . . . . . . . 8 ∅ ⊆ 𝐴
32 0fin 8132 . . . . . . . 8 ∅ ∈ Fin
33 elfpw 8212 . . . . . . . 8 (∅ ∈ (𝒫 𝐴 ∩ Fin) ↔ (∅ ⊆ 𝐴 ∧ ∅ ∈ Fin))
3431, 32, 33mpbir2an 954 . . . . . . 7 ∅ ∈ (𝒫 𝐴 ∩ Fin)
35 0cn 9976 . . . . . . 7 0 ∈ ℂ
36 reseq2 5351 . . . . . . . . . . 11 (𝑠 = ∅ → (𝐹𝑠) = (𝐹 ↾ ∅))
37 res0 5360 . . . . . . . . . . 11 (𝐹 ↾ ∅) = ∅
3836, 37syl6eq 2671 . . . . . . . . . 10 (𝑠 = ∅ → (𝐹𝑠) = ∅)
3938oveq2d 6620 . . . . . . . . 9 (𝑠 = ∅ → (𝐺 Σg (𝐹𝑠)) = (𝐺 Σg ∅))
40 eqid 2621 . . . . . . . . . . . 12 (ℝ*𝑠s (ℝ* ∖ {-∞})) = (ℝ*𝑠s (ℝ* ∖ {-∞}))
4140xrge0subm 19706 . . . . . . . . . . 11 (0[,]+∞) ∈ (SubMnd‘(ℝ*𝑠s (ℝ* ∖ {-∞})))
42 xrex 11773 . . . . . . . . . . . . . . 15 * ∈ V
43 difexg 4768 . . . . . . . . . . . . . . 15 (ℝ* ∈ V → (ℝ* ∖ {-∞}) ∈ V)
4442, 43ax-mp 5 . . . . . . . . . . . . . 14 (ℝ* ∖ {-∞}) ∈ V
45 simpl 473 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥) → 𝑥 ∈ ℝ*)
46 ge0nemnf 11947 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥) → 𝑥 ≠ -∞)
4745, 46jca 554 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥) → (𝑥 ∈ ℝ*𝑥 ≠ -∞))
48 elxrge0 12223 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (0[,]+∞) ↔ (𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥))
49 eldifsn 4287 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (ℝ* ∖ {-∞}) ↔ (𝑥 ∈ ℝ*𝑥 ≠ -∞))
5047, 48, 493imtr4i 281 . . . . . . . . . . . . . . 15 (𝑥 ∈ (0[,]+∞) → 𝑥 ∈ (ℝ* ∖ {-∞}))
5150ssriv 3587 . . . . . . . . . . . . . 14 (0[,]+∞) ⊆ (ℝ* ∖ {-∞})
52 ressabs 15860 . . . . . . . . . . . . . 14 (((ℝ* ∖ {-∞}) ∈ V ∧ (0[,]+∞) ⊆ (ℝ* ∖ {-∞})) → ((ℝ*𝑠s (ℝ* ∖ {-∞})) ↾s (0[,]+∞)) = (ℝ*𝑠s (0[,]+∞)))
5344, 51, 52mp2an 707 . . . . . . . . . . . . 13 ((ℝ*𝑠s (ℝ* ∖ {-∞})) ↾s (0[,]+∞)) = (ℝ*𝑠s (0[,]+∞))
543, 53eqtr4i 2646 . . . . . . . . . . . 12 𝐺 = ((ℝ*𝑠s (ℝ* ∖ {-∞})) ↾s (0[,]+∞))
5540xrs10 19704 . . . . . . . . . . . 12 0 = (0g‘(ℝ*𝑠s (ℝ* ∖ {-∞})))
5654, 55subm0 17277 . . . . . . . . . . 11 ((0[,]+∞) ∈ (SubMnd‘(ℝ*𝑠s (ℝ* ∖ {-∞}))) → 0 = (0g𝐺))
5741, 56ax-mp 5 . . . . . . . . . 10 0 = (0g𝐺)
5857gsum0 17199 . . . . . . . . 9 (𝐺 Σg ∅) = 0
5939, 58syl6eq 2671 . . . . . . . 8 (𝑠 = ∅ → (𝐺 Σg (𝐹𝑠)) = 0)
6024, 59elrnmpt1s 5333 . . . . . . 7 ((∅ ∈ (𝒫 𝐴 ∩ Fin) ∧ 0 ∈ ℂ) → 0 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))))
6134, 35, 60mp2an 707 . . . . . 6 0 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠)))
62 supxrub 12097 . . . . . 6 ((ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))) ⊆ ℝ* ∧ 0 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠)))) → 0 ≤ sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))), ℝ*, < ))
6327, 61, 62sylancl 693 . . . . 5 (𝜑 → 0 ≤ sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))), ℝ*, < ))
6463, 1breqtrrd 4641 . . . 4 (𝜑 → 0 ≤ 𝑆)
65 elxrge0 12223 . . . 4 (𝑆 ∈ (0[,]+∞) ↔ (𝑆 ∈ ℝ* ∧ 0 ≤ 𝑆))
6630, 64, 65sylanbrc 697 . . 3 (𝜑𝑆 ∈ (0[,]+∞))
67 letop 20920 . . . . . 6 (ordTop‘ ≤ ) ∈ Top
68 ovex 6632 . . . . . 6 (0[,]+∞) ∈ V
69 elrest 16009 . . . . . 6 (((ordTop‘ ≤ ) ∈ Top ∧ (0[,]+∞) ∈ V) → (𝑢 ∈ ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ↔ ∃𝑣 ∈ (ordTop‘ ≤ )𝑢 = (𝑣 ∩ (0[,]+∞))))
7067, 68, 69mp2an 707 . . . . 5 (𝑢 ∈ ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ↔ ∃𝑣 ∈ (ordTop‘ ≤ )𝑢 = (𝑣 ∩ (0[,]+∞)))
71 elinel1 3777 . . . . . . . 8 (𝑆 ∈ (𝑣 ∩ (0[,]+∞)) → 𝑆𝑣)
72 simplrl 799 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑣 ∈ (ordTop‘ ≤ ))
73 reex 9971 . . . . . . . . . . . . . . 15 ℝ ∈ V
74 elrestr 16010 . . . . . . . . . . . . . . 15 (((ordTop‘ ≤ ) ∈ Top ∧ ℝ ∈ V ∧ 𝑣 ∈ (ordTop‘ ≤ )) → (𝑣 ∩ ℝ) ∈ ((ordTop‘ ≤ ) ↾t ℝ))
7567, 73, 74mp3an12 1411 . . . . . . . . . . . . . 14 (𝑣 ∈ (ordTop‘ ≤ ) → (𝑣 ∩ ℝ) ∈ ((ordTop‘ ≤ ) ↾t ℝ))
7672, 75syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) → (𝑣 ∩ ℝ) ∈ ((ordTop‘ ≤ ) ↾t ℝ))
77 eqid 2621 . . . . . . . . . . . . . 14 ((ordTop‘ ≤ ) ↾t ℝ) = ((ordTop‘ ≤ ) ↾t ℝ)
7877xrtgioo 22517 . . . . . . . . . . . . 13 (topGen‘ran (,)) = ((ordTop‘ ≤ ) ↾t ℝ)
7976, 78syl6eleqr 2709 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) → (𝑣 ∩ ℝ) ∈ (topGen‘ran (,)))
80 simplrr 800 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑆𝑣)
81 simpr 477 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑆 ∈ ℝ)
8280, 81elind 3776 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑆 ∈ (𝑣 ∩ ℝ))
83 tg2 20680 . . . . . . . . . . . 12 (((𝑣 ∩ ℝ) ∈ (topGen‘ran (,)) ∧ 𝑆 ∈ (𝑣 ∩ ℝ)) → ∃𝑢 ∈ ran (,)(𝑆𝑢𝑢 ⊆ (𝑣 ∩ ℝ)))
8479, 82, 83syl2anc 692 . . . . . . . . . . 11 (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) → ∃𝑢 ∈ ran (,)(𝑆𝑢𝑢 ⊆ (𝑣 ∩ ℝ)))
85 ioof 12213 . . . . . . . . . . . . . 14 (,):(ℝ* × ℝ*)⟶𝒫 ℝ
86 ffn 6002 . . . . . . . . . . . . . 14 ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*))
87 ovelrn 6763 . . . . . . . . . . . . . 14 ((,) Fn (ℝ* × ℝ*) → (𝑢 ∈ ran (,) ↔ ∃𝑟 ∈ ℝ*𝑤 ∈ ℝ* 𝑢 = (𝑟(,)𝑤)))
8885, 86, 87mp2b 10 . . . . . . . . . . . . 13 (𝑢 ∈ ran (,) ↔ ∃𝑟 ∈ ℝ*𝑤 ∈ ℝ* 𝑢 = (𝑟(,)𝑤))
89 simprrr 804 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ))
9089adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ))
91 inss1 3811 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 ∩ ℝ) ⊆ 𝑣
9290, 91syl6ss 3595 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → (𝑟(,)𝑤) ⊆ 𝑣)
939a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → 𝐺 ∈ CMnd)
94 simprrl 803 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
95 elinel2 3778 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin)
9694, 95syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → 𝑦 ∈ Fin)
97 simp-4l 805 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → 𝜑)
9897, 12syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → 𝐹:𝐴⟶(0[,]+∞))
99 elfpw 8212 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑦𝐴𝑦 ∈ Fin))
10099simplbi 476 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦𝐴)
10194, 100syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → 𝑦𝐴)
10298, 101fssresd 6028 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → (𝐹𝑦):𝑦⟶(0[,]+∞))
103 ffun 6005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐹:𝐴⟶(0[,]+∞) → Fun 𝐹)
10412, 103syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → Fun 𝐹)
105104ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) → Fun 𝐹)
106105ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → Fun 𝐹)
107 c0ex 9978 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ∈ V
108107a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → 0 ∈ V)
109106, 96, 108resfifsupp 8247 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → (𝐹𝑦) finSupp 0)
1106, 57, 93, 96, 102, 109gsumcl 18237 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → (𝐺 Σg (𝐹𝑦)) ∈ (0[,]+∞))
1112, 110sseldi 3581 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → (𝐺 Σg (𝐹𝑦)) ∈ ℝ*)
112 simprll 801 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑟 ∈ ℝ*)
113112adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → 𝑟 ∈ ℝ*)
114 simprll 801 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → 𝑧 ∈ (𝒫 𝐴 ∩ Fin))
115 simprrr 804 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → 𝑧𝑦)
116115, 101sstrd 3593 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → 𝑧𝐴)
11798, 116fssresd 6028 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → (𝐹𝑧):𝑧⟶(0[,]+∞))
118 ssfi 8124 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 ∈ Fin ∧ 𝑧𝑦) → 𝑧 ∈ Fin)
11996, 115, 118syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → 𝑧 ∈ Fin)
12019a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → (0g𝐺) ∈ V)
121117, 119, 120fdmfifsupp 8229 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → (𝐹𝑧) finSupp (0g𝐺))
1226, 7, 93, 114, 117, 121gsumcl 18237 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → (𝐺 Σg (𝐹𝑧)) ∈ (0[,]+∞))
1232, 122sseldi 3581 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → (𝐺 Σg (𝐹𝑧)) ∈ ℝ*)
124 simprlr 802 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → 𝑟 < (𝐺 Σg (𝐹𝑧)))
125 xrge0tsmsd.a . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐴𝑉)
12697, 125syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → 𝐴𝑉)
1273, 126, 98, 94, 115xrge0gsumle 22544 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → (𝐺 Σg (𝐹𝑧)) ≤ (𝐺 Σg (𝐹𝑦)))
128113, 123, 111, 124, 127xrltletrd 11936 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → 𝑟 < (𝐺 Σg (𝐹𝑦)))
12997, 30syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → 𝑆 ∈ ℝ*)
130 simprlr 802 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑤 ∈ ℝ*)
131130adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → 𝑤 ∈ ℝ*)
13297, 27syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))) ⊆ ℝ*)
133 ovex 6632 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐺 Σg (𝐹𝑦)) ∈ V
134 reseq2 5351 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑠 = 𝑦 → (𝐹𝑠) = (𝐹𝑦))
135134oveq2d 6620 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑠 = 𝑦 → (𝐺 Σg (𝐹𝑠)) = (𝐺 Σg (𝐹𝑦)))
13624, 135elrnmpt1s 5333 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ (𝐺 Σg (𝐹𝑦)) ∈ V) → (𝐺 Σg (𝐹𝑦)) ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))))
13794, 133, 136sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → (𝐺 Σg (𝐹𝑦)) ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))))
138 supxrub 12097 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))) ⊆ ℝ* ∧ (𝐺 Σg (𝐹𝑦)) ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠)))) → (𝐺 Σg (𝐹𝑦)) ≤ sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))), ℝ*, < ))
139132, 137, 138syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → (𝐺 Σg (𝐹𝑦)) ≤ sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))), ℝ*, < ))
14097, 1syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → 𝑆 = sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))), ℝ*, < ))
141139, 140breqtrrd 4641 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → (𝐺 Σg (𝐹𝑦)) ≤ 𝑆)
142 simprrl 803 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑆 ∈ (𝑟(,)𝑤))
143 eliooord 12175 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑆 ∈ (𝑟(,)𝑤) → (𝑟 < 𝑆𝑆 < 𝑤))
144142, 143syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → (𝑟 < 𝑆𝑆 < 𝑤))
145144simprd 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑆 < 𝑤)
146145adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → 𝑆 < 𝑤)
147111, 129, 131, 141, 146xrlelttrd 11935 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → (𝐺 Σg (𝐹𝑦)) < 𝑤)
148 elioo1 12157 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) → ((𝐺 Σg (𝐹𝑦)) ∈ (𝑟(,)𝑤) ↔ ((𝐺 Σg (𝐹𝑦)) ∈ ℝ*𝑟 < (𝐺 Σg (𝐹𝑦)) ∧ (𝐺 Σg (𝐹𝑦)) < 𝑤)))
149113, 131, 148syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → ((𝐺 Σg (𝐹𝑦)) ∈ (𝑟(,)𝑤) ↔ ((𝐺 Σg (𝐹𝑦)) ∈ ℝ*𝑟 < (𝐺 Σg (𝐹𝑦)) ∧ (𝐺 Σg (𝐹𝑦)) < 𝑤)))
150111, 128, 147, 149mpbir3and 1243 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → (𝐺 Σg (𝐹𝑦)) ∈ (𝑟(,)𝑤))
15192, 150sseldd 3584 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → (𝐺 Σg (𝐹𝑦)) ∈ 𝑣)
152151, 110elind 3776 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦))) → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))
153152anassrs 679 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))
154153expr 642 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
155154ralrimiva 2960 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) → ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
156144simpld 475 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑟 < 𝑆)
1571ad3antrrr 765 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑆 = sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))), ℝ*, < ))
158156, 157breqtrd 4639 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))), ℝ*, < ))
15927ad3antrrr 765 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))) ⊆ ℝ*)
160 supxrlub 12098 . . . . . . . . . . . . . . . . . . . 20 ((ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))) ⊆ ℝ*𝑟 ∈ ℝ*) → (𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))), ℝ*, < ) ↔ ∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠)))𝑟 < 𝑤))
161159, 112, 160syl2anc 692 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → (𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))), ℝ*, < ) ↔ ∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠)))𝑟 < 𝑤))
162158, 161mpbid 222 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠)))𝑟 < 𝑤)
163 ovex 6632 . . . . . . . . . . . . . . . . . . . 20 (𝐺 Σg (𝐹𝑧)) ∈ V
164163rgenw 2919 . . . . . . . . . . . . . . . . . . 19 𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝐺 Σg (𝐹𝑧)) ∈ V
165 reseq2 5351 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = 𝑧 → (𝐹𝑠) = (𝐹𝑧))
166165oveq2d 6620 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = 𝑧 → (𝐺 Σg (𝐹𝑠)) = (𝐺 Σg (𝐹𝑧)))
167166cbvmptv 4710 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))) = (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑧)))
168 breq2 4617 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = (𝐺 Σg (𝐹𝑧)) → (𝑟 < 𝑤𝑟 < (𝐺 Σg (𝐹𝑧))))
169167, 168rexrnmpt 6325 . . . . . . . . . . . . . . . . . . 19 (∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝐺 Σg (𝐹𝑧)) ∈ V → (∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠)))𝑟 < 𝑤 ↔ ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)𝑟 < (𝐺 Σg (𝐹𝑧))))
170164, 169ax-mp 5 . . . . . . . . . . . . . . . . . 18 (∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠)))𝑟 < 𝑤 ↔ ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)𝑟 < (𝐺 Σg (𝐹𝑧)))
171162, 170sylib 208 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)𝑟 < (𝐺 Σg (𝐹𝑧)))
172155, 171reximddv 3012 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ*𝑤 ∈ ℝ*) ∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
173172expr 642 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ (𝑟 ∈ ℝ*𝑤 ∈ ℝ*)) → ((𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))
174 eleq2 2687 . . . . . . . . . . . . . . . . 17 (𝑢 = (𝑟(,)𝑤) → (𝑆𝑢𝑆 ∈ (𝑟(,)𝑤)))
175 sseq1 3605 . . . . . . . . . . . . . . . . 17 (𝑢 = (𝑟(,)𝑤) → (𝑢 ⊆ (𝑣 ∩ ℝ) ↔ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))
176174, 175anbi12d 746 . . . . . . . . . . . . . . . 16 (𝑢 = (𝑟(,)𝑤) → ((𝑆𝑢𝑢 ⊆ (𝑣 ∩ ℝ)) ↔ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ))))
177176imbi1d 331 . . . . . . . . . . . . . . 15 (𝑢 = (𝑟(,)𝑤) → (((𝑆𝑢𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) ↔ ((𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))))
178173, 177syl5ibrcom 237 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) ∧ (𝑟 ∈ ℝ*𝑤 ∈ ℝ*)) → (𝑢 = (𝑟(,)𝑤) → ((𝑆𝑢𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))))
179178rexlimdvva 3031 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) → (∃𝑟 ∈ ℝ*𝑤 ∈ ℝ* 𝑢 = (𝑟(,)𝑤) → ((𝑆𝑢𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))))
18088, 179syl5bi 232 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) → (𝑢 ∈ ran (,) → ((𝑆𝑢𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))))
181180rexlimdv 3023 . . . . . . . . . . 11 (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) → (∃𝑢 ∈ ran (,)(𝑆𝑢𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))
18284, 181mpd 15 . . . . . . . . . 10 (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 ∈ ℝ) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
183 simplrl 799 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) → 𝑣 ∈ (ordTop‘ ≤ ))
184 simpr 477 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) → 𝑆 = +∞)
185 simplrr 800 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) → 𝑆𝑣)
186184, 185eqeltrrd 2699 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) → +∞ ∈ 𝑣)
187 pnfnei 20934 . . . . . . . . . . . 12 ((𝑣 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ 𝑣) → ∃𝑟 ∈ ℝ (𝑟(,]+∞) ⊆ 𝑣)
188183, 186, 187syl2anc 692 . . . . . . . . . . 11 (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) → ∃𝑟 ∈ ℝ (𝑟(,]+∞) ⊆ 𝑣)
189 simprr 795 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → (𝑟(,]+∞) ⊆ 𝑣)
190189ad2antrr 761 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → (𝑟(,]+∞) ⊆ 𝑣)
1919a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → 𝐺 ∈ CMnd)
192 simprl 793 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → 𝑦 ∈ (𝒫 𝐴 ∩ Fin))
193 simp-5l 807 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → 𝜑)
194193, 12syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → 𝐹:𝐴⟶(0[,]+∞))
195100ad2antrl 763 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → 𝑦𝐴)
196194, 195fssresd 6028 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → (𝐹𝑦):𝑦⟶(0[,]+∞))
19795ad2antrl 763 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → 𝑦 ∈ Fin)
19819a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → (0g𝐺) ∈ V)
199196, 197, 198fdmfifsupp 8229 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → (𝐹𝑦) finSupp (0g𝐺))
2006, 7, 191, 192, 196, 199gsumcl 18237 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → (𝐺 Σg (𝐹𝑦)) ∈ (0[,]+∞))
2012, 200sseldi 3581 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → (𝐺 Σg (𝐹𝑦)) ∈ ℝ*)
202 rexr 10029 . . . . . . . . . . . . . . . . . . . 20 (𝑟 ∈ ℝ → 𝑟 ∈ ℝ*)
203202ad2antrl 763 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 ∈ ℝ*)
204203ad2antrr 761 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → 𝑟 ∈ ℝ*)
205 simplrl 799 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → 𝑧 ∈ (𝒫 𝐴 ∩ Fin))
206 simprr 795 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → 𝑧𝑦)
207206, 195sstrd 3593 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → 𝑧𝐴)
208194, 207fssresd 6028 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → (𝐹𝑧):𝑧⟶(0[,]+∞))
209197, 206, 118syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → 𝑧 ∈ Fin)
210208, 209, 198fdmfifsupp 8229 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → (𝐹𝑧) finSupp (0g𝐺))
2116, 7, 191, 205, 208, 210gsumcl 18237 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → (𝐺 Σg (𝐹𝑧)) ∈ (0[,]+∞))
2122, 211sseldi 3581 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → (𝐺 Σg (𝐹𝑧)) ∈ ℝ*)
213 simplrr 800 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → 𝑟 < (𝐺 Σg (𝐹𝑧)))
214193, 125syl 17 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → 𝐴𝑉)
2153, 214, 194, 192, 206xrge0gsumle 22544 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → (𝐺 Σg (𝐹𝑧)) ≤ (𝐺 Σg (𝐹𝑦)))
216204, 212, 201, 213, 215xrltletrd 11936 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → 𝑟 < (𝐺 Σg (𝐹𝑦)))
217 pnfge 11908 . . . . . . . . . . . . . . . . . 18 ((𝐺 Σg (𝐹𝑦)) ∈ ℝ* → (𝐺 Σg (𝐹𝑦)) ≤ +∞)
218201, 217syl 17 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → (𝐺 Σg (𝐹𝑦)) ≤ +∞)
219 pnfxr 10036 . . . . . . . . . . . . . . . . . 18 +∞ ∈ ℝ*
220 elioc1 12159 . . . . . . . . . . . . . . . . . 18 ((𝑟 ∈ ℝ* ∧ +∞ ∈ ℝ*) → ((𝐺 Σg (𝐹𝑦)) ∈ (𝑟(,]+∞) ↔ ((𝐺 Σg (𝐹𝑦)) ∈ ℝ*𝑟 < (𝐺 Σg (𝐹𝑦)) ∧ (𝐺 Σg (𝐹𝑦)) ≤ +∞)))
221204, 219, 220sylancl 693 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → ((𝐺 Σg (𝐹𝑦)) ∈ (𝑟(,]+∞) ↔ ((𝐺 Σg (𝐹𝑦)) ∈ ℝ*𝑟 < (𝐺 Σg (𝐹𝑦)) ∧ (𝐺 Σg (𝐹𝑦)) ≤ +∞)))
222201, 216, 218, 221mpbir3and 1243 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → (𝐺 Σg (𝐹𝑦)) ∈ (𝑟(,]+∞))
223190, 222sseldd 3584 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → (𝐺 Σg (𝐹𝑦)) ∈ 𝑣)
224223, 200elind 3776 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧𝑦)) → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))
225224expr 642 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
226225ralrimiva 2960 . . . . . . . . . . . 12 (((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹𝑧)))) → ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
227 ltpnf 11898 . . . . . . . . . . . . . . . . 17 (𝑟 ∈ ℝ → 𝑟 < +∞)
228227ad2antrl 763 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 < +∞)
229 simplr 791 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑆 = +∞)
230228, 229breqtrrd 4641 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 < 𝑆)
2311ad3antrrr 765 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑆 = sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))), ℝ*, < ))
232230, 231breqtrd 4639 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))), ℝ*, < ))
23327ad3antrrr 765 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))) ⊆ ℝ*)
234233, 203, 160syl2anc 692 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → (𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠))), ℝ*, < ) ↔ ∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠)))𝑟 < 𝑤))
235232, 234mpbid 222 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → ∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹𝑠)))𝑟 < 𝑤)
236235, 170sylib 208 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)𝑟 < (𝐺 Σg (𝐹𝑧)))
237226, 236reximddv 3012 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
238188, 237rexlimddv 3028 . . . . . . . . . 10 (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) ∧ 𝑆 = +∞) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
239 ge0nemnf 11947 . . . . . . . . . . . . . 14 ((𝑆 ∈ ℝ* ∧ 0 ≤ 𝑆) → 𝑆 ≠ -∞)
24030, 64, 239syl2anc 692 . . . . . . . . . . . . 13 (𝜑𝑆 ≠ -∞)
24130, 240jca 554 . . . . . . . . . . . 12 (𝜑 → (𝑆 ∈ ℝ*𝑆 ≠ -∞))
242241adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) → (𝑆 ∈ ℝ*𝑆 ≠ -∞))
243 xrnemnf 11895 . . . . . . . . . . 11 ((𝑆 ∈ ℝ*𝑆 ≠ -∞) ↔ (𝑆 ∈ ℝ ∨ 𝑆 = +∞))
244242, 243sylib 208 . . . . . . . . . 10 ((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) → (𝑆 ∈ ℝ ∨ 𝑆 = +∞))
245182, 238, 244mpjaodan 826 . . . . . . . . 9 ((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆𝑣)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
246245expr 642 . . . . . . . 8 ((𝜑𝑣 ∈ (ordTop‘ ≤ )) → (𝑆𝑣 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))
24771, 246syl5 34 . . . . . . 7 ((𝜑𝑣 ∈ (ordTop‘ ≤ )) → (𝑆 ∈ (𝑣 ∩ (0[,]+∞)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))
248 eleq2 2687 . . . . . . . 8 (𝑢 = (𝑣 ∩ (0[,]+∞)) → (𝑆𝑢𝑆 ∈ (𝑣 ∩ (0[,]+∞))))
249 eleq2 2687 . . . . . . . . . 10 (𝑢 = (𝑣 ∩ (0[,]+∞)) → ((𝐺 Σg (𝐹𝑦)) ∈ 𝑢 ↔ (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))
250249imbi2d 330 . . . . . . . . 9 (𝑢 = (𝑣 ∩ (0[,]+∞)) → ((𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ 𝑢) ↔ (𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))
251250rexralbidv 3051 . . . . . . . 8 (𝑢 = (𝑣 ∩ (0[,]+∞)) → (∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ 𝑢) ↔ ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))
252248, 251imbi12d 334 . . . . . . 7 (𝑢 = (𝑣 ∩ (0[,]+∞)) → ((𝑆𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ 𝑢)) ↔ (𝑆 ∈ (𝑣 ∩ (0[,]+∞)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))))
253247, 252syl5ibrcom 237 . . . . . 6 ((𝜑𝑣 ∈ (ordTop‘ ≤ )) → (𝑢 = (𝑣 ∩ (0[,]+∞)) → (𝑆𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ 𝑢))))
254253rexlimdva 3024 . . . . 5 (𝜑 → (∃𝑣 ∈ (ordTop‘ ≤ )𝑢 = (𝑣 ∩ (0[,]+∞)) → (𝑆𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ 𝑢))))
25570, 254syl5bi 232 . . . 4 (𝜑 → (𝑢 ∈ ((ordTop‘ ≤ ) ↾t (0[,]+∞)) → (𝑆𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ 𝑢))))
256255ralrimiv 2959 . . 3 (𝜑 → ∀𝑢 ∈ ((ordTop‘ ≤ ) ↾t (0[,]+∞))(𝑆𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ 𝑢)))
257 xrstset 19684 . . . . . . 7 (ordTop‘ ≤ ) = (TopSet‘ℝ*𝑠)
2583, 257resstset 15967 . . . . . 6 ((0[,]+∞) ∈ V → (ordTop‘ ≤ ) = (TopSet‘𝐺))
25968, 258ax-mp 5 . . . . 5 (ordTop‘ ≤ ) = (TopSet‘𝐺)
2606, 259topnval 16016 . . . 4 ((ordTop‘ ≤ ) ↾t (0[,]+∞)) = (TopOpen‘𝐺)
261 eqid 2621 . . . 4 (𝒫 𝐴 ∩ Fin) = (𝒫 𝐴 ∩ Fin)
2629a1i 11 . . . 4 (𝜑𝐺 ∈ CMnd)
263 xrstps 20923 . . . . . . 7 *𝑠 ∈ TopSp
264 resstps 20901 . . . . . . 7 ((ℝ*𝑠 ∈ TopSp ∧ (0[,]+∞) ∈ V) → (ℝ*𝑠s (0[,]+∞)) ∈ TopSp)
265263, 68, 264mp2an 707 . . . . . 6 (ℝ*𝑠s (0[,]+∞)) ∈ TopSp
2663, 265eqeltri 2694 . . . . 5 𝐺 ∈ TopSp
267266a1i 11 . . . 4 (𝜑𝐺 ∈ TopSp)
2686, 260, 261, 262, 267, 125, 12eltsms 21846 . . 3 (𝜑 → (𝑆 ∈ (𝐺 tsums 𝐹) ↔ (𝑆 ∈ (0[,]+∞) ∧ ∀𝑢 ∈ ((ordTop‘ ≤ ) ↾t (0[,]+∞))(𝑆𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧𝑦 → (𝐺 Σg (𝐹𝑦)) ∈ 𝑢)))))
26966, 256, 268mpbir2and 956 . 2 (𝜑𝑆 ∈ (𝐺 tsums 𝐹))
270 letsr 17148 . . . . 5 ≤ ∈ TosetRel
271 ordthaus 21098 . . . . 5 ( ≤ ∈ TosetRel → (ordTop‘ ≤ ) ∈ Haus)
272270, 271mp1i 13 . . . 4 (𝜑 → (ordTop‘ ≤ ) ∈ Haus)
273 resthaus 21082 . . . 4 (((ordTop‘ ≤ ) ∈ Haus ∧ (0[,]+∞) ∈ V) → ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈ Haus)
274272, 68, 273sylancl 693 . . 3 (𝜑 → ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈ Haus)
2756, 262, 267, 125, 12, 260, 274haustsms2 21850 . 2 (𝜑 → (𝑆 ∈ (𝐺 tsums 𝐹) → (𝐺 tsums 𝐹) = {𝑆}))
276269, 275mpd 15 1 (𝜑 → (𝐺 tsums 𝐹) = {𝑆})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908  Vcvv 3186  cdif 3552  cin 3554  wss 3555  c0 3891  𝒫 cpw 4130  {csn 4148   class class class wbr 4613  cmpt 4673   × cxp 5072  ran crn 5075  cres 5076  Fun wfun 5841   Fn wfn 5842  wf 5843  cfv 5847  (class class class)co 6604  Fincfn 7899  supcsup 8290  cc 9878  cr 9879  0cc0 9880  +∞cpnf 10015  -∞cmnf 10016  *cxr 10017   < clt 10018  cle 10019  (,)cioo 12117  (,]cioc 12118  [,]cicc 12120  Basecbs 15781  s cress 15782  TopSetcts 15868  t crest 16002  topGenctg 16019  0gc0g 16021   Σg cgsu 16022  ordTopcordt 16080  *𝑠cxrs 16081   TosetRel ctsr 17120  SubMndcsubmnd 17255  CMndccmn 18114  Topctop 20617  TopSpctps 20619  Hauscha 21022   tsums ctsu 21839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957  ax-pre-sup 9958
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-iin 4488  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-of 6850  df-om 7013  df-1st 7113  df-2nd 7114  df-supp 7241  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-map 7804  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-fsupp 8220  df-fi 8261  df-sup 8292  df-inf 8293  df-oi 8359  df-card 8709  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-div 10629  df-nn 10965  df-2 11023  df-3 11024  df-4 11025  df-5 11026  df-6 11027  df-7 11028  df-8 11029  df-9 11030  df-n0 11237  df-z 11322  df-dec 11438  df-uz 11632  df-q 11733  df-xadd 11891  df-ioo 12121  df-ioc 12122  df-ico 12123  df-icc 12124  df-fz 12269  df-fzo 12407  df-seq 12742  df-hash 13058  df-struct 15783  df-ndx 15784  df-slot 15785  df-base 15786  df-sets 15787  df-ress 15788  df-plusg 15875  df-mulr 15876  df-tset 15881  df-ple 15882  df-ds 15885  df-rest 16004  df-topn 16005  df-0g 16023  df-gsum 16024  df-topgen 16025  df-ordt 16082  df-xrs 16083  df-mre 16167  df-mrc 16168  df-acs 16170  df-ps 17121  df-tsr 17122  df-mgm 17163  df-sgrp 17205  df-mnd 17216  df-submnd 17257  df-cntz 17671  df-cmn 18116  df-fbas 19662  df-fg 19663  df-top 20621  df-bases 20622  df-topon 20623  df-topsp 20624  df-ntr 20734  df-nei 20812  df-cn 20941  df-haus 21029  df-fil 21560  df-fm 21652  df-flim 21653  df-flf 21654  df-tsms 21840
This theorem is referenced by:  esumval  29889  esumel  29890  esumsnf  29907
  Copyright terms: Public domain W3C validator