| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | xrge0tsms.s | . . . . 5
⊢ 𝑆 = sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, <
) | 
| 2 |  | iccssxr 13471 | . . . . . . . . 9
⊢
(0[,]+∞) ⊆ ℝ* | 
| 3 |  | xrge0tsms.g | . . . . . . . . . . . 12
⊢ 𝐺 =
(ℝ*𝑠 ↾s
(0[,]+∞)) | 
| 4 |  | xrsbas 21397 | . . . . . . . . . . . 12
⊢
ℝ* =
(Base‘ℝ*𝑠) | 
| 5 | 3, 4 | ressbas2 17284 | . . . . . . . . . . 11
⊢
((0[,]+∞) ⊆ ℝ* → (0[,]+∞) =
(Base‘𝐺)) | 
| 6 | 2, 5 | ax-mp 5 | . . . . . . . . . 10
⊢
(0[,]+∞) = (Base‘𝐺) | 
| 7 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) =
(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) | 
| 8 | 7 | xrge0subm 21426 | . . . . . . . . . . 11
⊢
(0[,]+∞) ∈
(SubMnd‘(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞}))) | 
| 9 |  | xrex 13030 | . . . . . . . . . . . . . . 15
⊢
ℝ* ∈ V | 
| 10 | 9 | difexi 5329 | . . . . . . . . . . . . . 14
⊢
(ℝ* ∖ {-∞}) ∈ V | 
| 11 |  | simpl 482 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ*
∧ 0 ≤ 𝑥) →
𝑥 ∈
ℝ*) | 
| 12 |  | ge0nemnf 13216 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ*
∧ 0 ≤ 𝑥) →
𝑥 ≠
-∞) | 
| 13 | 11, 12 | jca 511 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ*
∧ 0 ≤ 𝑥) →
(𝑥 ∈
ℝ* ∧ 𝑥
≠ -∞)) | 
| 14 |  | elxrge0 13498 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (0[,]+∞) ↔
(𝑥 ∈
ℝ* ∧ 0 ≤ 𝑥)) | 
| 15 |  | eldifsn 4785 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (ℝ*
∖ {-∞}) ↔ (𝑥 ∈ ℝ* ∧ 𝑥 ≠
-∞)) | 
| 16 | 13, 14, 15 | 3imtr4i 292 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0[,]+∞) →
𝑥 ∈
(ℝ* ∖ {-∞})) | 
| 17 | 16 | ssriv 3986 | . . . . . . . . . . . . . 14
⊢
(0[,]+∞) ⊆ (ℝ* ∖
{-∞}) | 
| 18 |  | ressabs 17295 | . . . . . . . . . . . . . 14
⊢
(((ℝ* ∖ {-∞}) ∈ V ∧ (0[,]+∞)
⊆ (ℝ* ∖ {-∞})) →
((ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ↾s (0[,]+∞)) =
(ℝ*𝑠 ↾s
(0[,]+∞))) | 
| 19 | 10, 17, 18 | mp2an 692 | . . . . . . . . . . . . 13
⊢
((ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ↾s (0[,]+∞)) =
(ℝ*𝑠 ↾s
(0[,]+∞)) | 
| 20 | 3, 19 | eqtr4i 2767 | . . . . . . . . . . . 12
⊢ 𝐺 =
((ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ↾s
(0[,]+∞)) | 
| 21 | 7 | xrs10 21424 | . . . . . . . . . . . 12
⊢ 0 =
(0g‘(ℝ*𝑠
↾s (ℝ* ∖ {-∞}))) | 
| 22 | 20, 21 | subm0 18829 | . . . . . . . . . . 11
⊢
((0[,]+∞) ∈
(SubMnd‘(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞}))) → 0 =
(0g‘𝐺)) | 
| 23 | 8, 22 | ax-mp 5 | . . . . . . . . . 10
⊢ 0 =
(0g‘𝐺) | 
| 24 |  | xrge0cmn 21427 | . . . . . . . . . . . 12
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ CMnd | 
| 25 | 3, 24 | eqeltri 2836 | . . . . . . . . . . 11
⊢ 𝐺 ∈ CMnd | 
| 26 | 25 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐺 ∈ CMnd) | 
| 27 |  | elinel2 4201 | . . . . . . . . . . 11
⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) → 𝑠 ∈ Fin) | 
| 28 | 27 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑠 ∈ Fin) | 
| 29 |  | xrge0tsms.f | . . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐴⟶(0[,]+∞)) | 
| 30 |  | elfpw 9395 | . . . . . . . . . . . 12
⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑠 ⊆ 𝐴 ∧ 𝑠 ∈ Fin)) | 
| 31 | 30 | simplbi 497 | . . . . . . . . . . 11
⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) → 𝑠 ⊆ 𝐴) | 
| 32 |  | fssres 6773 | . . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶(0[,]+∞) ∧ 𝑠 ⊆ 𝐴) → (𝐹 ↾ 𝑠):𝑠⟶(0[,]+∞)) | 
| 33 | 29, 31, 32 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑠):𝑠⟶(0[,]+∞)) | 
| 34 |  | c0ex 11256 | . . . . . . . . . . . 12
⊢ 0 ∈
V | 
| 35 | 34 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 0 ∈
V) | 
| 36 | 33, 28, 35 | fdmfifsupp 9416 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑠) finSupp 0) | 
| 37 | 6, 23, 26, 28, 33, 36 | gsumcl 19934 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑠)) ∈ (0[,]+∞)) | 
| 38 | 2, 37 | sselid 3980 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑠)) ∈
ℝ*) | 
| 39 | 38 | fmpttd 7134 | . . . . . . 7
⊢ (𝜑 → (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))):(𝒫 𝐴 ∩
Fin)⟶ℝ*) | 
| 40 | 39 | frnd 6743 | . . . . . 6
⊢ (𝜑 → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) ⊆
ℝ*) | 
| 41 |  | supxrcl 13358 | . . . . . 6
⊢ (ran
(𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) ⊆ ℝ*
→ sup(ran (𝑠 ∈
(𝒫 𝐴 ∩ Fin)
↦ (𝐺
Σg (𝐹 ↾ 𝑠))), ℝ*, < ) ∈
ℝ*) | 
| 42 | 40, 41 | syl 17 | . . . . 5
⊢ (𝜑 → sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))), ℝ*, < )
∈ ℝ*) | 
| 43 | 1, 42 | eqeltrid 2844 | . . . 4
⊢ (𝜑 → 𝑆 ∈
ℝ*) | 
| 44 |  | 0ss 4399 | . . . . . . . 8
⊢ ∅
⊆ 𝐴 | 
| 45 |  | 0fi 9083 | . . . . . . . 8
⊢ ∅
∈ Fin | 
| 46 |  | elfpw 9395 | . . . . . . . 8
⊢ (∅
∈ (𝒫 𝐴 ∩
Fin) ↔ (∅ ⊆ 𝐴 ∧ ∅ ∈ Fin)) | 
| 47 | 44, 45, 46 | mpbir2an 711 | . . . . . . 7
⊢ ∅
∈ (𝒫 𝐴 ∩
Fin) | 
| 48 |  | 0cn 11254 | . . . . . . 7
⊢ 0 ∈
ℂ | 
| 49 |  | eqid 2736 | . . . . . . . 8
⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) = (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) | 
| 50 |  | reseq2 5991 | . . . . . . . . . . 11
⊢ (𝑠 = ∅ → (𝐹 ↾ 𝑠) = (𝐹 ↾ ∅)) | 
| 51 |  | res0 6000 | . . . . . . . . . . 11
⊢ (𝐹 ↾ ∅) =
∅ | 
| 52 | 50, 51 | eqtrdi 2792 | . . . . . . . . . 10
⊢ (𝑠 = ∅ → (𝐹 ↾ 𝑠) = ∅) | 
| 53 | 52 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑠 = ∅ → (𝐺 Σg
(𝐹 ↾ 𝑠)) = (𝐺 Σg
∅)) | 
| 54 | 23 | gsum0 18698 | . . . . . . . . 9
⊢ (𝐺 Σg
∅) = 0 | 
| 55 | 53, 54 | eqtrdi 2792 | . . . . . . . 8
⊢ (𝑠 = ∅ → (𝐺 Σg
(𝐹 ↾ 𝑠)) = 0) | 
| 56 | 49, 55 | elrnmpt1s 5969 | . . . . . . 7
⊢ ((∅
∈ (𝒫 𝐴 ∩
Fin) ∧ 0 ∈ ℂ) → 0 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))) | 
| 57 | 47, 48, 56 | mp2an 692 | . . . . . 6
⊢ 0 ∈
ran (𝑠 ∈ (𝒫
𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) | 
| 58 |  | supxrub 13367 | . . . . . 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 5184 | . . . 4
⊢ (𝜑 → 0 ≤ 𝑆) | 
| 61 |  | elxrge0 13498 | . . . 4
⊢ (𝑆 ∈ (0[,]+∞) ↔
(𝑆 ∈
ℝ* ∧ 0 ≤ 𝑆)) | 
| 62 | 43, 60, 61 | sylanbrc 583 | . . 3
⊢ (𝜑 → 𝑆 ∈ (0[,]+∞)) | 
| 63 |  | letop 23215 | . . . . . 6
⊢
(ordTop‘ ≤ ) ∈ Top | 
| 64 |  | ovex 7465 | . . . . . 6
⊢
(0[,]+∞) ∈ V | 
| 65 |  | elrest 17473 | . . . . . 6
⊢
(((ordTop‘ ≤ ) ∈ Top ∧ (0[,]+∞) ∈ V) →
(𝑢 ∈ ((ordTop‘
≤ ) ↾t (0[,]+∞)) ↔ ∃𝑣 ∈ (ordTop‘ ≤ )𝑢 = (𝑣 ∩ (0[,]+∞)))) | 
| 66 | 63, 64, 65 | mp2an 692 | . . . . 5
⊢ (𝑢 ∈ ((ordTop‘ ≤ )
↾t (0[,]+∞)) ↔ ∃𝑣 ∈ (ordTop‘ ≤ )𝑢 = (𝑣 ∩ (0[,]+∞))) | 
| 67 |  | elinel1 4200 | . . . . . . . 8
⊢ (𝑆 ∈ (𝑣 ∩ (0[,]+∞)) → 𝑆 ∈ 𝑣) | 
| 68 |  | reex 11247 | . . . . . . . . . . . . . 14
⊢ ℝ
∈ V | 
| 69 |  | simplrl 776 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑣 ∈ (ordTop‘ ≤
)) | 
| 70 |  | elrestr 17474 | . . . . . . . . . . . . . 14
⊢
(((ordTop‘ ≤ ) ∈ Top ∧ ℝ ∈ V ∧ 𝑣 ∈ (ordTop‘ ≤ ))
→ (𝑣 ∩ ℝ)
∈ ((ordTop‘ ≤ ) ↾t ℝ)) | 
| 71 | 63, 68, 69, 70 | mp3an12i 1466 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (𝑣 ∩ ℝ) ∈ ((ordTop‘ ≤ )
↾t ℝ)) | 
| 72 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
((ordTop‘ ≤ ) ↾t ℝ) = ((ordTop‘
≤ ) ↾t ℝ) | 
| 73 | 72 | xrtgioo 24829 | . . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) = ((ordTop‘ ≤ ) ↾t
ℝ) | 
| 74 | 71, 73 | eleqtrrdi 2851 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (𝑣 ∩ ℝ) ∈ (topGen‘ran
(,))) | 
| 75 |  | simplrr 777 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑆 ∈ 𝑣) | 
| 76 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑆 ∈ ℝ) | 
| 77 | 75, 76 | elind 4199 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑆 ∈ (𝑣 ∩ ℝ)) | 
| 78 |  | tg2 22973 | . . . . . . . . . . . 12
⊢ (((𝑣 ∩ ℝ) ∈
(topGen‘ran (,)) ∧ 𝑆 ∈ (𝑣 ∩ ℝ)) → ∃𝑢 ∈ ran (,)(𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ))) | 
| 79 | 74, 77, 78 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → ∃𝑢 ∈ ran (,)(𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ))) | 
| 80 |  | ioof 13488 | . . . . . . . . . . . . . 14
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ | 
| 81 |  | ffn 6735 | . . . . . . . . . . . . . 14
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) | 
| 82 |  | ovelrn 7610 | . . . . . . . . . . . . . 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 4236 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑣 ∩ ℝ) ⊆ 𝑣 | 
| 87 | 85, 86 | sstrdi 3995 | . . . . . . . . . . . . . . . . . . . . . 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 4201 | . . . . . . . . . . . . . . . . . . . . . . . . . 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 9395 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ∈ Fin)) | 
| 95 | 94 | simplbi 497 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴) | 
| 96 | 89, 95 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ⊆ 𝐴) | 
| 97 | 93, 96 | fssresd 6774 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑦):𝑦⟶(0[,]+∞)) | 
| 98 | 34 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 0 ∈ V) | 
| 99 | 97, 91, 98 | fdmfifsupp 9416 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑦) finSupp 0) | 
| 100 | 6, 23, 88, 91, 97, 99 | gsumcl 19934 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (0[,]+∞)) | 
| 101 | 2, 100 | sselid 3980 | . . . . . . . . . . . . . . . . . . . . . . 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 9302 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ∈ Fin) | 
| 106 | 104, 96 | sstrd 3993 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ⊆ 𝐴) | 
| 107 | 93, 106 | fssresd 6774 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑧):𝑧⟶(0[,]+∞)) | 
| 108 | 107, 105,
98 | fdmfifsupp 9416 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑧) finSupp 0) | 
| 109 | 6, 23, 88, 105, 107, 108 | gsumcl 19934 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ (0[,]+∞)) | 
| 110 | 2, 109 | sselid 3980 | . . . . . . . . . . . . . . . . . . . . . . . 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 24856 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑧)) ≤ (𝐺 Σg (𝐹 ↾ 𝑦))) | 
| 115 | 103, 110,
101, 111, 114 | xrltletrd 13204 | . . . . . . . . . . . . . . . . . . . . . . 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 7465 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐺 Σg
(𝐹 ↾ 𝑦)) ∈ V | 
| 121 |  | reseq2 5991 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑠 = 𝑦 → (𝐹 ↾ 𝑠) = (𝐹 ↾ 𝑦)) | 
| 122 | 121 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑠 = 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑠)) = (𝐺 Σg (𝐹 ↾ 𝑦))) | 
| 123 | 49, 122 | elrnmpt1s 5969 | . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13367 | . . . . . . . . . . . . . . . . . . . . . . . . . 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 5184 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ≤ 𝑆) | 
| 128 |  | simprrl 780 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑆 ∈ (𝑟(,)𝑤)) | 
| 129 |  | eliooord 13447 | . . . . . . . . . . . . . . . . . . . . . . . . . . 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 13203 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) < 𝑤) | 
| 134 |  | elioo1 13428 | . . . . . . . . . . . . . . . . . . . . . . . 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 1342 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑟(,)𝑤)) | 
| 137 | 87, 136 | sseldd 3983 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣) | 
| 138 | 137, 100 | elind 4199 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))) | 
| 139 | 138 | anassrs 467 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))) | 
| 140 | 139 | expr 456 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) | 
| 141 | 140 | ralrimiva 3145 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) → ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) | 
| 142 | 130 | simpld 494 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑟 < 𝑆) | 
| 143 | 142, 1 | breqtrdi 5183 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, <
)) | 
| 144 | 40 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) ⊆
ℝ*) | 
| 145 |  | supxrlub 13368 | . . . . . . . . . . . . . . . . . . . 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 7465 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐺 Σg
(𝐹 ↾ 𝑧)) ∈ V | 
| 149 | 148 | rgenw 3064 | . . . . . . . . . . . . . . . . . . 19
⊢
∀𝑧 ∈
(𝒫 𝐴 ∩
Fin)(𝐺
Σg (𝐹 ↾ 𝑧)) ∈ V | 
| 150 |  | reseq2 5991 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠 = 𝑧 → (𝐹 ↾ 𝑠) = (𝐹 ↾ 𝑧)) | 
| 151 | 150 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑠)) = (𝐺 Σg (𝐹 ↾ 𝑧))) | 
| 152 | 151 | cbvmptv 5254 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) = (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑧))) | 
| 153 |  | breq2 5146 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = (𝐺 Σg (𝐹 ↾ 𝑧)) → (𝑟 < 𝑤 ↔ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) | 
| 154 | 152, 153 | rexrnmptw 7114 | . . . . . . . . . . . . . . . . . . 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 3170 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) | 
| 158 | 157 | expr 456 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ (𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*))
→ ((𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))) | 
| 159 |  | eleq2 2829 | . . . . . . . . . . . . . . . . 17
⊢ (𝑢 = (𝑟(,)𝑤) → (𝑆 ∈ 𝑢 ↔ 𝑆 ∈ (𝑟(,)𝑤))) | 
| 160 |  | sseq1 4008 | . . . . . . . . . . . . . . . . 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 3212 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (∃𝑟 ∈ ℝ*
∃𝑤 ∈
ℝ* 𝑢 =
(𝑟(,)𝑤) → ((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))) | 
| 165 | 83, 164 | biimtrid 242 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (𝑢 ∈ ran (,) → ((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))) | 
| 166 | 165 | rexlimdv 3152 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (∃𝑢 ∈ ran (,)(𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))) | 
| 167 | 79, 166 | mpd 15 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) | 
| 168 |  | simplrl 776 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → 𝑣 ∈ (ordTop‘ ≤
)) | 
| 169 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → 𝑆 = +∞) | 
| 170 |  | simplrr 777 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → 𝑆 ∈ 𝑣) | 
| 171 | 169, 170 | eqeltrrd 2841 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → +∞ ∈ 𝑣) | 
| 172 |  | pnfnei 23229 | . . . . . . . . . . . 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 6774 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑦):𝑦⟶(0[,]+∞)) | 
| 182 | 34 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 0 ∈ V) | 
| 183 | 181, 177,
182 | fdmfifsupp 9416 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑦) finSupp 0) | 
| 184 | 6, 23, 176, 177, 181, 183 | gsumcl 19934 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (0[,]+∞)) | 
| 185 | 2, 184 | sselid 3980 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈
ℝ*) | 
| 186 |  | rexr 11308 | . . . . . . . . . . . . . . . . . . . 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 9302 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑧 ∈ Fin) | 
| 191 | 189, 180 | sstrd 3993 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑧 ⊆ 𝐴) | 
| 192 | 179, 191 | fssresd 6774 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑧):𝑧⟶(0[,]+∞)) | 
| 193 | 192, 190,
182 | fdmfifsupp 9416 | . . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑧) finSupp 0) | 
| 194 | 6, 23, 176, 190, 192, 193 | gsumcl 19934 | . . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ (0[,]+∞)) | 
| 195 | 2, 194 | sselid 3980 | . . . . . . . . . . . . . . . . . 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 24856 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑧)) ≤ (𝐺 Σg (𝐹 ↾ 𝑦))) | 
| 200 | 188, 195,
185, 196, 199 | xrltletrd 13204 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑦))) | 
| 201 |  | pnfge 13173 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 Σg
(𝐹 ↾ 𝑦)) ∈ ℝ*
→ (𝐺
Σg (𝐹 ↾ 𝑦)) ≤ +∞) | 
| 202 | 185, 201 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ≤ +∞) | 
| 203 |  | pnfxr 11316 | . . . . . . . . . . . . . . . . . 18
⊢ +∞
∈ ℝ* | 
| 204 |  | elioc1 13430 | . . . . . . . . . . . . . . . . . 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 1342 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑟(,]+∞)) | 
| 207 | 175, 206 | sseldd 3983 | . . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣) | 
| 208 | 207, 184 | elind 4199 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))) | 
| 209 | 208 | expr 456 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) | 
| 210 | 209 | ralrimiva 3145 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) → ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) | 
| 211 |  | ltpnf 13163 | . . . . . . . . . . . . . . . . 17
⊢ (𝑟 ∈ ℝ → 𝑟 < +∞) | 
| 212 | 211 | ad2antrl 728 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 < +∞) | 
| 213 |  | simplr 768 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑆 = +∞) | 
| 214 | 212, 213 | breqtrrd 5170 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 < 𝑆) | 
| 215 | 214, 1 | breqtrdi 5183 | . . . . . . . . . . . . . 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 3170 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) | 
| 221 | 173, 220 | rexlimddv 3160 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) | 
| 222 |  | ge0nemnf 13216 | . . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ ℝ*
∧ 0 ≤ 𝑆) →
𝑆 ≠
-∞) | 
| 223 | 43, 60, 222 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ≠ -∞) | 
| 224 | 43, 223 | jca 511 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 ∈ ℝ* ∧ 𝑆 ≠
-∞)) | 
| 225 | 224 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) → (𝑆 ∈ ℝ* ∧ 𝑆 ≠
-∞)) | 
| 226 |  | xrnemnf 13160 | . . . . . . . . . . 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 2829 | . . . . . . . 8
⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → (𝑆 ∈ 𝑢 ↔ 𝑆 ∈ (𝑣 ∩ (0[,]+∞)))) | 
| 232 |  | eleq2 2829 | . . . . . . . . . 10
⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → ((𝐺 Σg
(𝐹 ↾ 𝑦)) ∈ 𝑢 ↔ (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) | 
| 233 | 232 | imbi2d 340 | . . . . . . . . 9
⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → ((𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢) ↔ (𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))) | 
| 234 | 233 | rexralbidv 3222 | . . . . . . . 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 3154 | . . . . 5
⊢ (𝜑 → (∃𝑣 ∈ (ordTop‘ ≤ )𝑢 = (𝑣 ∩ (0[,]+∞)) → (𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)))) | 
| 238 | 66, 237 | biimtrid 242 | . . . 4
⊢ (𝜑 → (𝑢 ∈ ((ordTop‘ ≤ )
↾t (0[,]+∞)) → (𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)))) | 
| 239 | 238 | ralrimiv 3144 | . . 3
⊢ (𝜑 → ∀𝑢 ∈ ((ordTop‘ ≤ )
↾t (0[,]+∞))(𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢))) | 
| 240 |  | xrstset 21400 | . . . . . . 7
⊢
(ordTop‘ ≤ ) =
(TopSet‘ℝ*𝑠) | 
| 241 | 3, 240 | resstset 17410 | . . . . . 6
⊢
((0[,]+∞) ∈ V → (ordTop‘ ≤ ) =
(TopSet‘𝐺)) | 
| 242 | 64, 241 | ax-mp 5 | . . . . 5
⊢
(ordTop‘ ≤ ) = (TopSet‘𝐺) | 
| 243 | 6, 242 | topnval 17480 | . . . 4
⊢
((ordTop‘ ≤ ) ↾t (0[,]+∞)) =
(TopOpen‘𝐺) | 
| 244 |  | eqid 2736 | . . . 4
⊢
(𝒫 𝐴 ∩
Fin) = (𝒫 𝐴 ∩
Fin) | 
| 245 | 25 | a1i 11 | . . . 4
⊢ (𝜑 → 𝐺 ∈ CMnd) | 
| 246 |  | xrstps 23218 | . . . . . . 7
⊢
ℝ*𝑠 ∈ TopSp | 
| 247 |  | resstps 23196 | . . . . . . 7
⊢
((ℝ*𝑠 ∈ TopSp ∧
(0[,]+∞) ∈ V) → (ℝ*𝑠
↾s (0[,]+∞)) ∈ TopSp) | 
| 248 | 246, 64, 247 | mp2an 692 | . . . . . 6
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ TopSp | 
| 249 | 3, 248 | eqeltri 2836 | . . . . 5
⊢ 𝐺 ∈ TopSp | 
| 250 | 249 | a1i 11 | . . . 4
⊢ (𝜑 → 𝐺 ∈ TopSp) | 
| 251 | 6, 243, 244, 245, 250, 112, 29 | eltsms 24142 | . . 3
⊢ (𝜑 → (𝑆 ∈ (𝐺 tsums 𝐹) ↔ (𝑆 ∈ (0[,]+∞) ∧ ∀𝑢 ∈ ((ordTop‘ ≤ )
↾t (0[,]+∞))(𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢))))) | 
| 252 | 62, 239, 251 | mpbir2and 713 | . 2
⊢ (𝜑 → 𝑆 ∈ (𝐺 tsums 𝐹)) | 
| 253 |  | letsr 18639 | . . . . 5
⊢  ≤
∈ TosetRel | 
| 254 |  | ordthaus 23393 | . . . . 5
⊢ ( ≤
∈ TosetRel → (ordTop‘ ≤ ) ∈ Haus) | 
| 255 | 253, 254 | mp1i 13 | . . . 4
⊢ (𝜑 → (ordTop‘ ≤ )
∈ Haus) | 
| 256 |  | resthaus 23377 | . . . 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 24146 | . 2
⊢ (𝜑 → (𝑆 ∈ (𝐺 tsums 𝐹) → (𝐺 tsums 𝐹) = {𝑆})) | 
| 259 | 252, 258 | mpd 15 | 1
⊢ (𝜑 → (𝐺 tsums 𝐹) = {𝑆}) |