| Step | Hyp | Ref
| Expression |
| 1 | | xrge0tsmsd.s |
. . . . 5
⊢ (𝜑 → 𝑆 = sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, <
)) |
| 2 | | iccssxr 13470 |
. . . . . . . . 9
⊢
(0[,]+∞) ⊆ ℝ* |
| 3 | | xrge0tsmsd.g |
. . . . . . . . . . . 12
⊢ 𝐺 =
(ℝ*𝑠 ↾s
(0[,]+∞)) |
| 4 | | xrsbas 21396 |
. . . . . . . . . . . 12
⊢
ℝ* =
(Base‘ℝ*𝑠) |
| 5 | 3, 4 | ressbas2 17283 |
. . . . . . . . . . 11
⊢
((0[,]+∞) ⊆ ℝ* → (0[,]+∞) =
(Base‘𝐺)) |
| 6 | 2, 5 | ax-mp 5 |
. . . . . . . . . 10
⊢
(0[,]+∞) = (Base‘𝐺) |
| 7 | | eqid 2737 |
. . . . . . . . . 10
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 8 | | xrge0cmn 21426 |
. . . . . . . . . . . 12
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ CMnd |
| 9 | 3, 8 | eqeltri 2837 |
. . . . . . . . . . 11
⊢ 𝐺 ∈ CMnd |
| 10 | 9 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐺 ∈ CMnd) |
| 11 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) |
| 12 | | xrge0tsmsd.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐴⟶(0[,]+∞)) |
| 13 | | elfpw 9394 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑠 ⊆ 𝐴 ∧ 𝑠 ∈ Fin)) |
| 14 | 13 | simplbi 497 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) → 𝑠 ⊆ 𝐴) |
| 15 | | fssres 6774 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶(0[,]+∞) ∧ 𝑠 ⊆ 𝐴) → (𝐹 ↾ 𝑠):𝑠⟶(0[,]+∞)) |
| 16 | 12, 14, 15 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑠):𝑠⟶(0[,]+∞)) |
| 17 | | elinel2 4202 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) → 𝑠 ∈ Fin) |
| 18 | 17 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑠 ∈ Fin) |
| 19 | | fvexd 6921 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) →
(0g‘𝐺)
∈ V) |
| 20 | 16, 18, 19 | fdmfifsupp 9415 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑠) finSupp (0g‘𝐺)) |
| 21 | 6, 7, 10, 11, 16, 20 | gsumcl 19933 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑠)) ∈ (0[,]+∞)) |
| 22 | 2, 21 | sselid 3981 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑠)) ∈
ℝ*) |
| 23 | 22 | fmpttd 7135 |
. . . . . . 7
⊢ (𝜑 → (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))):(𝒫 𝐴 ∩
Fin)⟶ℝ*) |
| 24 | 23 | frnd 6744 |
. . . . . 6
⊢ (𝜑 → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) ⊆
ℝ*) |
| 25 | | supxrcl 13357 |
. . . . . 6
⊢ (ran
(𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) ⊆ ℝ*
→ sup(ran (𝑠 ∈
(𝒫 𝐴 ∩ Fin)
↦ (𝐺
Σg (𝐹 ↾ 𝑠))), ℝ*, < ) ∈
ℝ*) |
| 26 | 24, 25 | syl 17 |
. . . . 5
⊢ (𝜑 → sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))), ℝ*, < )
∈ ℝ*) |
| 27 | 1, 26 | eqeltrd 2841 |
. . . 4
⊢ (𝜑 → 𝑆 ∈
ℝ*) |
| 28 | | 0ss 4400 |
. . . . . . . 8
⊢ ∅
⊆ 𝐴 |
| 29 | | 0fi 9082 |
. . . . . . . 8
⊢ ∅
∈ Fin |
| 30 | | elfpw 9394 |
. . . . . . . 8
⊢ (∅
∈ (𝒫 𝐴 ∩
Fin) ↔ (∅ ⊆ 𝐴 ∧ ∅ ∈ Fin)) |
| 31 | 28, 29, 30 | mpbir2an 711 |
. . . . . . 7
⊢ ∅
∈ (𝒫 𝐴 ∩
Fin) |
| 32 | | 0cn 11253 |
. . . . . . 7
⊢ 0 ∈
ℂ |
| 33 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) = (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) |
| 34 | | reseq2 5992 |
. . . . . . . . . . 11
⊢ (𝑠 = ∅ → (𝐹 ↾ 𝑠) = (𝐹 ↾ ∅)) |
| 35 | | res0 6001 |
. . . . . . . . . . 11
⊢ (𝐹 ↾ ∅) =
∅ |
| 36 | 34, 35 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝑠 = ∅ → (𝐹 ↾ 𝑠) = ∅) |
| 37 | 36 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑠 = ∅ → (𝐺 Σg
(𝐹 ↾ 𝑠)) = (𝐺 Σg
∅)) |
| 38 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) =
(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) |
| 39 | 38 | xrge0subm 21425 |
. . . . . . . . . . 11
⊢
(0[,]+∞) ∈
(SubMnd‘(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞}))) |
| 40 | | xrex 13029 |
. . . . . . . . . . . . . . 15
⊢
ℝ* ∈ V |
| 41 | | difexg 5329 |
. . . . . . . . . . . . . . 15
⊢
(ℝ* ∈ V → (ℝ* ∖
{-∞}) ∈ V) |
| 42 | 40, 41 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(ℝ* ∖ {-∞}) ∈ V |
| 43 | | simpl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ*
∧ 0 ≤ 𝑥) →
𝑥 ∈
ℝ*) |
| 44 | | ge0nemnf 13215 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ*
∧ 0 ≤ 𝑥) →
𝑥 ≠
-∞) |
| 45 | 43, 44 | jca 511 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ*
∧ 0 ≤ 𝑥) →
(𝑥 ∈
ℝ* ∧ 𝑥
≠ -∞)) |
| 46 | | elxrge0 13497 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (0[,]+∞) ↔
(𝑥 ∈
ℝ* ∧ 0 ≤ 𝑥)) |
| 47 | | eldifsn 4786 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (ℝ*
∖ {-∞}) ↔ (𝑥 ∈ ℝ* ∧ 𝑥 ≠
-∞)) |
| 48 | 45, 46, 47 | 3imtr4i 292 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0[,]+∞) →
𝑥 ∈
(ℝ* ∖ {-∞})) |
| 49 | 48 | ssriv 3987 |
. . . . . . . . . . . . . 14
⊢
(0[,]+∞) ⊆ (ℝ* ∖
{-∞}) |
| 50 | | ressabs 17294 |
. . . . . . . . . . . . . 14
⊢
(((ℝ* ∖ {-∞}) ∈ V ∧ (0[,]+∞)
⊆ (ℝ* ∖ {-∞})) →
((ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ↾s (0[,]+∞)) =
(ℝ*𝑠 ↾s
(0[,]+∞))) |
| 51 | 42, 49, 50 | mp2an 692 |
. . . . . . . . . . . . 13
⊢
((ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ↾s (0[,]+∞)) =
(ℝ*𝑠 ↾s
(0[,]+∞)) |
| 52 | 3, 51 | eqtr4i 2768 |
. . . . . . . . . . . 12
⊢ 𝐺 =
((ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ↾s
(0[,]+∞)) |
| 53 | 38 | xrs10 21423 |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘(ℝ*𝑠
↾s (ℝ* ∖ {-∞}))) |
| 54 | 52, 53 | subm0 18828 |
. . . . . . . . . . 11
⊢
((0[,]+∞) ∈
(SubMnd‘(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞}))) → 0 =
(0g‘𝐺)) |
| 55 | 39, 54 | ax-mp 5 |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝐺) |
| 56 | 55 | gsum0 18697 |
. . . . . . . . 9
⊢ (𝐺 Σg
∅) = 0 |
| 57 | 37, 56 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑠 = ∅ → (𝐺 Σg
(𝐹 ↾ 𝑠)) = 0) |
| 58 | 33, 57 | elrnmpt1s 5970 |
. . . . . . 7
⊢ ((∅
∈ (𝒫 𝐴 ∩
Fin) ∧ 0 ∈ ℂ) → 0 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))) |
| 59 | 31, 32, 58 | mp2an 692 |
. . . . . 6
⊢ 0 ∈
ran (𝑠 ∈ (𝒫
𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) |
| 60 | | supxrub 13366 |
. . . . . 6
⊢ ((ran
(𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) ⊆ ℝ*
∧ 0 ∈ ran (𝑠
∈ (𝒫 𝐴 ∩
Fin) ↦ (𝐺
Σg (𝐹 ↾ 𝑠)))) → 0 ≤ sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))), ℝ*, <
)) |
| 61 | 24, 59, 60 | sylancl 586 |
. . . . 5
⊢ (𝜑 → 0 ≤ sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))), ℝ*, <
)) |
| 62 | 61, 1 | breqtrrd 5171 |
. . . 4
⊢ (𝜑 → 0 ≤ 𝑆) |
| 63 | | elxrge0 13497 |
. . . 4
⊢ (𝑆 ∈ (0[,]+∞) ↔
(𝑆 ∈
ℝ* ∧ 0 ≤ 𝑆)) |
| 64 | 27, 62, 63 | sylanbrc 583 |
. . 3
⊢ (𝜑 → 𝑆 ∈ (0[,]+∞)) |
| 65 | | letop 23214 |
. . . . . 6
⊢
(ordTop‘ ≤ ) ∈ Top |
| 66 | | ovex 7464 |
. . . . . 6
⊢
(0[,]+∞) ∈ V |
| 67 | | elrest 17472 |
. . . . . 6
⊢
(((ordTop‘ ≤ ) ∈ Top ∧ (0[,]+∞) ∈ V) →
(𝑢 ∈ ((ordTop‘
≤ ) ↾t (0[,]+∞)) ↔ ∃𝑣 ∈ (ordTop‘ ≤ )𝑢 = (𝑣 ∩ (0[,]+∞)))) |
| 68 | 65, 66, 67 | mp2an 692 |
. . . . 5
⊢ (𝑢 ∈ ((ordTop‘ ≤ )
↾t (0[,]+∞)) ↔ ∃𝑣 ∈ (ordTop‘ ≤ )𝑢 = (𝑣 ∩ (0[,]+∞))) |
| 69 | | elinel1 4201 |
. . . . . . . 8
⊢ (𝑆 ∈ (𝑣 ∩ (0[,]+∞)) → 𝑆 ∈ 𝑣) |
| 70 | | simplrl 777 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑣 ∈ (ordTop‘ ≤
)) |
| 71 | | reex 11246 |
. . . . . . . . . . . . . . 15
⊢ ℝ
∈ V |
| 72 | | elrestr 17473 |
. . . . . . . . . . . . . . 15
⊢
(((ordTop‘ ≤ ) ∈ Top ∧ ℝ ∈ V ∧ 𝑣 ∈ (ordTop‘ ≤ ))
→ (𝑣 ∩ ℝ)
∈ ((ordTop‘ ≤ ) ↾t ℝ)) |
| 73 | 65, 71, 72 | mp3an12 1453 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ (ordTop‘ ≤ )
→ (𝑣 ∩ ℝ)
∈ ((ordTop‘ ≤ ) ↾t ℝ)) |
| 74 | 70, 73 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (𝑣 ∩ ℝ) ∈ ((ordTop‘ ≤ )
↾t ℝ)) |
| 75 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
((ordTop‘ ≤ ) ↾t ℝ) = ((ordTop‘
≤ ) ↾t ℝ) |
| 76 | 75 | xrtgioo 24828 |
. . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) = ((ordTop‘ ≤ ) ↾t
ℝ) |
| 77 | 74, 76 | eleqtrrdi 2852 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (𝑣 ∩ ℝ) ∈ (topGen‘ran
(,))) |
| 78 | | simplrr 778 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑆 ∈ 𝑣) |
| 79 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑆 ∈ ℝ) |
| 80 | 78, 79 | elind 4200 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑆 ∈ (𝑣 ∩ ℝ)) |
| 81 | | tg2 22972 |
. . . . . . . . . . . 12
⊢ (((𝑣 ∩ ℝ) ∈
(topGen‘ran (,)) ∧ 𝑆 ∈ (𝑣 ∩ ℝ)) → ∃𝑢 ∈ ran (,)(𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ))) |
| 82 | 77, 80, 81 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → ∃𝑢 ∈ ran (,)(𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ))) |
| 83 | | ioof 13487 |
. . . . . . . . . . . . . 14
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
| 84 | | ffn 6736 |
. . . . . . . . . . . . . 14
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
| 85 | | ovelrn 7609 |
. . . . . . . . . . . . . 14
⊢ ((,) Fn
(ℝ* × ℝ*) → (𝑢 ∈ ran (,) ↔ ∃𝑟 ∈ ℝ*
∃𝑤 ∈
ℝ* 𝑢 =
(𝑟(,)𝑤))) |
| 86 | 83, 84, 85 | mp2b 10 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ ran (,) ↔
∃𝑟 ∈
ℝ* ∃𝑤 ∈ ℝ* 𝑢 = (𝑟(,)𝑤)) |
| 87 | | simprrr 782 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)) |
| 88 | 87 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)) |
| 89 | | inss1 4237 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑣 ∩ ℝ) ⊆ 𝑣 |
| 90 | 88, 89 | sstrdi 3996 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝑟(,)𝑤) ⊆ 𝑣) |
| 91 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝐺 ∈ CMnd) |
| 92 | | simprrl 781 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) |
| 93 | | elinel2 4202 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin) |
| 94 | 92, 93 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ∈ Fin) |
| 95 | | simp-4l 783 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝜑) |
| 96 | 95, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝐹:𝐴⟶(0[,]+∞)) |
| 97 | | elfpw 9394 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ∈ Fin)) |
| 98 | 97 | simplbi 497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴) |
| 99 | 92, 98 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ⊆ 𝐴) |
| 100 | 96, 99 | fssresd 6775 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑦):𝑦⟶(0[,]+∞)) |
| 101 | 12 | ffund 6740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → Fun 𝐹) |
| 102 | 101 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → Fun 𝐹) |
| 103 | 102 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → Fun 𝐹) |
| 104 | | c0ex 11255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 ∈
V |
| 105 | 104 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 0 ∈ V) |
| 106 | 103, 94, 105 | resfifsupp 9437 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑦) finSupp 0) |
| 107 | 6, 55, 91, 94, 100, 106 | gsumcl 19933 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (0[,]+∞)) |
| 108 | 2, 107 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈
ℝ*) |
| 109 | | simprll 779 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑟 ∈ ℝ*) |
| 110 | 109 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑟 ∈ ℝ*) |
| 111 | | simprll 779 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) |
| 112 | | simprrr 782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ⊆ 𝑦) |
| 113 | 112, 99 | sstrd 3994 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ⊆ 𝐴) |
| 114 | 96, 113 | fssresd 6775 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑧):𝑧⟶(0[,]+∞)) |
| 115 | | ssfi 9213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑦 ∈ Fin ∧ 𝑧 ⊆ 𝑦) → 𝑧 ∈ Fin) |
| 116 | 94, 112, 115 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ∈ Fin) |
| 117 | | fvexd 6921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (0g‘𝐺) ∈ V) |
| 118 | 114, 116,
117 | fdmfifsupp 9415 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑧) finSupp (0g‘𝐺)) |
| 119 | 6, 7, 91, 111, 114, 118 | gsumcl 19933 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ (0[,]+∞)) |
| 120 | 2, 119 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈
ℝ*) |
| 121 | | simprlr 780 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) |
| 122 | | xrge0tsmsd.a |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 123 | 95, 122 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝐴 ∈ 𝑉) |
| 124 | 3, 123, 96, 92, 112 | xrge0gsumle 24855 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑧)) ≤ (𝐺 Σg (𝐹 ↾ 𝑦))) |
| 125 | 110, 120,
108, 121, 124 | xrltletrd 13203 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑦))) |
| 126 | 95, 27 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑆 ∈
ℝ*) |
| 127 | | simprlr 780 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑤 ∈ ℝ*) |
| 128 | 127 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑤 ∈ ℝ*) |
| 129 | 95, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) ⊆
ℝ*) |
| 130 | | ovex 7464 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐺 Σg
(𝐹 ↾ 𝑦)) ∈ V |
| 131 | | reseq2 5992 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑠 = 𝑦 → (𝐹 ↾ 𝑠) = (𝐹 ↾ 𝑦)) |
| 132 | 131 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑠 = 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑠)) = (𝐺 Σg (𝐹 ↾ 𝑦))) |
| 133 | 33, 132 | elrnmpt1s 5970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ (𝐺 Σg
(𝐹 ↾ 𝑦)) ∈ V) → (𝐺 Σg
(𝐹 ↾ 𝑦)) ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠)))) |
| 134 | 92, 130, 133 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))) |
| 135 | | supxrub 13366 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((ran
(𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) ⊆ ℝ*
∧ (𝐺
Σg (𝐹 ↾ 𝑦)) ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ≤ sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, <
)) |
| 136 | 129, 134,
135 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ≤ sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, <
)) |
| 137 | 95, 1 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑆 = sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, <
)) |
| 138 | 136, 137 | breqtrrd 5171 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ≤ 𝑆) |
| 139 | | simprrl 781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑆 ∈ (𝑟(,)𝑤)) |
| 140 | | eliooord 13446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑆 ∈ (𝑟(,)𝑤) → (𝑟 < 𝑆 ∧ 𝑆 < 𝑤)) |
| 141 | 139, 140 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → (𝑟 < 𝑆 ∧ 𝑆 < 𝑤)) |
| 142 | 141 | simprd 495 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑆 < 𝑤) |
| 143 | 142 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑆 < 𝑤) |
| 144 | 108, 126,
128, 138, 143 | xrlelttrd 13202 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) < 𝑤) |
| 145 | | elioo1 13427 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑟 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑟(,)𝑤) ↔ ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ ℝ* ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑦)) ∧ (𝐺 Σg (𝐹 ↾ 𝑦)) < 𝑤))) |
| 146 | 110, 128,
145 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑟(,)𝑤) ↔ ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ ℝ* ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑦)) ∧ (𝐺 Σg (𝐹 ↾ 𝑦)) < 𝑤))) |
| 147 | 108, 125,
144, 146 | mpbir3and 1343 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑟(,)𝑤)) |
| 148 | 90, 147 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣) |
| 149 | 148, 107 | elind 4200 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))) |
| 150 | 149 | anassrs 467 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))) |
| 151 | 150 | expr 456 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) |
| 152 | 151 | ralrimiva 3146 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) → ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) |
| 153 | 141 | simpld 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑟 < 𝑆) |
| 154 | 1 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑆 = sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, <
)) |
| 155 | 153, 154 | breqtrd 5169 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, <
)) |
| 156 | 24 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) ⊆
ℝ*) |
| 157 | | supxrlub 13367 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ran
(𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) ⊆ ℝ*
∧ 𝑟 ∈
ℝ*) → (𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < ) ↔
∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠)))𝑟 < 𝑤)) |
| 158 | 156, 109,
157 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → (𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < ) ↔
∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠)))𝑟 < 𝑤)) |
| 159 | 155, 158 | mpbid 232 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))𝑟 < 𝑤) |
| 160 | | ovex 7464 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐺 Σg
(𝐹 ↾ 𝑧)) ∈ V |
| 161 | 160 | rgenw 3065 |
. . . . . . . . . . . . . . . . . . 19
⊢
∀𝑧 ∈
(𝒫 𝐴 ∩
Fin)(𝐺
Σg (𝐹 ↾ 𝑧)) ∈ V |
| 162 | | reseq2 5992 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠 = 𝑧 → (𝐹 ↾ 𝑠) = (𝐹 ↾ 𝑧)) |
| 163 | 162 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑠)) = (𝐺 Σg (𝐹 ↾ 𝑧))) |
| 164 | 163 | cbvmptv 5255 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) = (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑧))) |
| 165 | | breq2 5147 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = (𝐺 Σg (𝐹 ↾ 𝑧)) → (𝑟 < 𝑤 ↔ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) |
| 166 | 164, 165 | rexrnmptw 7115 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑧 ∈
(𝒫 𝐴 ∩
Fin)(𝐺
Σg (𝐹 ↾ 𝑧)) ∈ V → (∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))𝑟 < 𝑤 ↔ ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) |
| 167 | 161, 166 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑤 ∈ ran
(𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠)))𝑟 < 𝑤 ↔ ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) |
| 168 | 159, 167 | sylib 218 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) |
| 169 | 152, 168 | reximddv 3171 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) |
| 170 | 169 | expr 456 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ (𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*))
→ ((𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))) |
| 171 | | eleq2 2830 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = (𝑟(,)𝑤) → (𝑆 ∈ 𝑢 ↔ 𝑆 ∈ (𝑟(,)𝑤))) |
| 172 | | sseq1 4009 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = (𝑟(,)𝑤) → (𝑢 ⊆ (𝑣 ∩ ℝ) ↔ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ))) |
| 173 | 171, 172 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = (𝑟(,)𝑤) → ((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) ↔ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) |
| 174 | 173 | imbi1d 341 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = (𝑟(,)𝑤) → (((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) ↔ ((𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))) |
| 175 | 170, 174 | syl5ibrcom 247 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ (𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*))
→ (𝑢 = (𝑟(,)𝑤) → ((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))) |
| 176 | 175 | rexlimdvva 3213 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (∃𝑟 ∈ ℝ*
∃𝑤 ∈
ℝ* 𝑢 =
(𝑟(,)𝑤) → ((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))) |
| 177 | 86, 176 | biimtrid 242 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (𝑢 ∈ ran (,) → ((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))) |
| 178 | 177 | rexlimdv 3153 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (∃𝑢 ∈ ran (,)(𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))) |
| 179 | 82, 178 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) |
| 180 | | simplrl 777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → 𝑣 ∈ (ordTop‘ ≤
)) |
| 181 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → 𝑆 = +∞) |
| 182 | | simplrr 778 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → 𝑆 ∈ 𝑣) |
| 183 | 181, 182 | eqeltrrd 2842 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → +∞ ∈ 𝑣) |
| 184 | | pnfnei 23228 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ (ordTop‘ ≤ )
∧ +∞ ∈ 𝑣)
→ ∃𝑟 ∈
ℝ (𝑟(,]+∞)
⊆ 𝑣) |
| 185 | 180, 183,
184 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → ∃𝑟 ∈ ℝ (𝑟(,]+∞) ⊆ 𝑣) |
| 186 | | simprr 773 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → (𝑟(,]+∞) ⊆ 𝑣) |
| 187 | 186 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝑟(,]+∞) ⊆ 𝑣) |
| 188 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝐺 ∈ CMnd) |
| 189 | | simprl 771 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) |
| 190 | | simp-5l 785 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝜑) |
| 191 | 190, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝐹:𝐴⟶(0[,]+∞)) |
| 192 | 98 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑦 ⊆ 𝐴) |
| 193 | 191, 192 | fssresd 6775 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑦):𝑦⟶(0[,]+∞)) |
| 194 | 93 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑦 ∈ Fin) |
| 195 | | fvexd 6921 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (0g‘𝐺) ∈ V) |
| 196 | 193, 194,
195 | fdmfifsupp 9415 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑦) finSupp (0g‘𝐺)) |
| 197 | 6, 7, 188, 189, 193, 196 | gsumcl 19933 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (0[,]+∞)) |
| 198 | 2, 197 | sselid 3981 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈
ℝ*) |
| 199 | | rexr 11307 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 ∈ ℝ → 𝑟 ∈
ℝ*) |
| 200 | 199 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 ∈ ℝ*) |
| 201 | 200 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑟 ∈ ℝ*) |
| 202 | | simplrl 777 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) |
| 203 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑧 ⊆ 𝑦) |
| 204 | 203, 192 | sstrd 3994 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑧 ⊆ 𝐴) |
| 205 | 191, 204 | fssresd 6775 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑧):𝑧⟶(0[,]+∞)) |
| 206 | 194, 203,
115 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑧 ∈ Fin) |
| 207 | 205, 206,
195 | fdmfifsupp 9415 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑧) finSupp (0g‘𝐺)) |
| 208 | 6, 7, 188, 202, 205, 207 | gsumcl 19933 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ (0[,]+∞)) |
| 209 | 2, 208 | sselid 3981 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈
ℝ*) |
| 210 | | simplrr 778 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) |
| 211 | 190, 122 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝐴 ∈ 𝑉) |
| 212 | 3, 211, 191, 189, 203 | xrge0gsumle 24855 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑧)) ≤ (𝐺 Σg (𝐹 ↾ 𝑦))) |
| 213 | 201, 209,
198, 210, 212 | xrltletrd 13203 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑦))) |
| 214 | | pnfge 13172 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 Σg
(𝐹 ↾ 𝑦)) ∈ ℝ*
→ (𝐺
Σg (𝐹 ↾ 𝑦)) ≤ +∞) |
| 215 | 198, 214 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ≤ +∞) |
| 216 | | pnfxr 11315 |
. . . . . . . . . . . . . . . . . 18
⊢ +∞
∈ ℝ* |
| 217 | | elioc1 13429 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑟 ∈ ℝ*
∧ +∞ ∈ ℝ*) → ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑟(,]+∞) ↔ ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ ℝ* ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑦)) ∧ (𝐺 Σg (𝐹 ↾ 𝑦)) ≤ +∞))) |
| 218 | 201, 216,
217 | sylancl 586 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑟(,]+∞) ↔ ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ ℝ* ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑦)) ∧ (𝐺 Σg (𝐹 ↾ 𝑦)) ≤ +∞))) |
| 219 | 198, 213,
215, 218 | mpbir3and 1343 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑟(,]+∞)) |
| 220 | 187, 219 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣) |
| 221 | 220, 197 | elind 4200 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))) |
| 222 | 221 | expr 456 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) |
| 223 | 222 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) → ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) |
| 224 | | ltpnf 13162 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 ∈ ℝ → 𝑟 < +∞) |
| 225 | 224 | ad2antrl 728 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 < +∞) |
| 226 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑆 = +∞) |
| 227 | 225, 226 | breqtrrd 5171 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 < 𝑆) |
| 228 | 1 | ad3antrrr 730 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑆 = sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, <
)) |
| 229 | 227, 228 | breqtrd 5169 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, <
)) |
| 230 | 24 | ad3antrrr 730 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) ⊆
ℝ*) |
| 231 | 230, 200,
157 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → (𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < ) ↔
∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠)))𝑟 < 𝑤)) |
| 232 | 229, 231 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → ∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))𝑟 < 𝑤) |
| 233 | 232, 167 | sylib 218 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) |
| 234 | 223, 233 | reximddv 3171 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) |
| 235 | 185, 234 | rexlimddv 3161 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) |
| 236 | | ge0nemnf 13215 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ ℝ*
∧ 0 ≤ 𝑆) →
𝑆 ≠
-∞) |
| 237 | 27, 62, 236 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ≠ -∞) |
| 238 | 27, 237 | jca 511 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 ∈ ℝ* ∧ 𝑆 ≠
-∞)) |
| 239 | 238 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) → (𝑆 ∈ ℝ* ∧ 𝑆 ≠
-∞)) |
| 240 | | xrnemnf 13159 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ ℝ*
∧ 𝑆 ≠ -∞)
↔ (𝑆 ∈ ℝ
∨ 𝑆 =
+∞)) |
| 241 | 239, 240 | sylib 218 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) → (𝑆 ∈ ℝ ∨ 𝑆 = +∞)) |
| 242 | 179, 235,
241 | mpjaodan 961 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) |
| 243 | 242 | expr 456 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 ∈ (ordTop‘ ≤ )) → (𝑆 ∈ 𝑣 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))) |
| 244 | 69, 243 | syl5 34 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ (ordTop‘ ≤ )) → (𝑆 ∈ (𝑣 ∩ (0[,]+∞)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))) |
| 245 | | eleq2 2830 |
. . . . . . . 8
⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → (𝑆 ∈ 𝑢 ↔ 𝑆 ∈ (𝑣 ∩ (0[,]+∞)))) |
| 246 | | eleq2 2830 |
. . . . . . . . . 10
⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → ((𝐺 Σg
(𝐹 ↾ 𝑦)) ∈ 𝑢 ↔ (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) |
| 247 | 246 | imbi2d 340 |
. . . . . . . . 9
⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → ((𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢) ↔ (𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))) |
| 248 | 247 | rexralbidv 3223 |
. . . . . . . 8
⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → (∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢) ↔ ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))) |
| 249 | 245, 248 | imbi12d 344 |
. . . . . . 7
⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → ((𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)) ↔ (𝑆 ∈ (𝑣 ∩ (0[,]+∞)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))) |
| 250 | 244, 249 | syl5ibrcom 247 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ (ordTop‘ ≤ )) → (𝑢 = (𝑣 ∩ (0[,]+∞)) → (𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)))) |
| 251 | 250 | rexlimdva 3155 |
. . . . 5
⊢ (𝜑 → (∃𝑣 ∈ (ordTop‘ ≤ )𝑢 = (𝑣 ∩ (0[,]+∞)) → (𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)))) |
| 252 | 68, 251 | biimtrid 242 |
. . . 4
⊢ (𝜑 → (𝑢 ∈ ((ordTop‘ ≤ )
↾t (0[,]+∞)) → (𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)))) |
| 253 | 252 | ralrimiv 3145 |
. . 3
⊢ (𝜑 → ∀𝑢 ∈ ((ordTop‘ ≤ )
↾t (0[,]+∞))(𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢))) |
| 254 | | xrstset 21399 |
. . . . . . 7
⊢
(ordTop‘ ≤ ) =
(TopSet‘ℝ*𝑠) |
| 255 | 3, 254 | resstset 17409 |
. . . . . 6
⊢
((0[,]+∞) ∈ V → (ordTop‘ ≤ ) =
(TopSet‘𝐺)) |
| 256 | 66, 255 | ax-mp 5 |
. . . . 5
⊢
(ordTop‘ ≤ ) = (TopSet‘𝐺) |
| 257 | 6, 256 | topnval 17479 |
. . . 4
⊢
((ordTop‘ ≤ ) ↾t (0[,]+∞)) =
(TopOpen‘𝐺) |
| 258 | | eqid 2737 |
. . . 4
⊢
(𝒫 𝐴 ∩
Fin) = (𝒫 𝐴 ∩
Fin) |
| 259 | 9 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ CMnd) |
| 260 | | xrstps 23217 |
. . . . . . 7
⊢
ℝ*𝑠 ∈ TopSp |
| 261 | | resstps 23195 |
. . . . . . 7
⊢
((ℝ*𝑠 ∈ TopSp ∧
(0[,]+∞) ∈ V) → (ℝ*𝑠
↾s (0[,]+∞)) ∈ TopSp) |
| 262 | 260, 66, 261 | mp2an 692 |
. . . . . 6
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ TopSp |
| 263 | 3, 262 | eqeltri 2837 |
. . . . 5
⊢ 𝐺 ∈ TopSp |
| 264 | 263 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ TopSp) |
| 265 | 6, 257, 258, 259, 264, 122, 12 | eltsms 24141 |
. . 3
⊢ (𝜑 → (𝑆 ∈ (𝐺 tsums 𝐹) ↔ (𝑆 ∈ (0[,]+∞) ∧ ∀𝑢 ∈ ((ordTop‘ ≤ )
↾t (0[,]+∞))(𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢))))) |
| 266 | 64, 253, 265 | mpbir2and 713 |
. 2
⊢ (𝜑 → 𝑆 ∈ (𝐺 tsums 𝐹)) |
| 267 | | letsr 18638 |
. . . . 5
⊢ ≤
∈ TosetRel |
| 268 | | ordthaus 23392 |
. . . . 5
⊢ ( ≤
∈ TosetRel → (ordTop‘ ≤ ) ∈ Haus) |
| 269 | 267, 268 | mp1i 13 |
. . . 4
⊢ (𝜑 → (ordTop‘ ≤ )
∈ Haus) |
| 270 | | resthaus 23376 |
. . . 4
⊢
(((ordTop‘ ≤ ) ∈ Haus ∧ (0[,]+∞) ∈ V)
→ ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈
Haus) |
| 271 | 269, 66, 270 | sylancl 586 |
. . 3
⊢ (𝜑 → ((ordTop‘ ≤ )
↾t (0[,]+∞)) ∈ Haus) |
| 272 | 6, 259, 264, 122, 12, 257, 271 | haustsms2 24145 |
. 2
⊢ (𝜑 → (𝑆 ∈ (𝐺 tsums 𝐹) → (𝐺 tsums 𝐹) = {𝑆})) |
| 273 | 266, 272 | mpd 15 |
1
⊢ (𝜑 → (𝐺 tsums 𝐹) = {𝑆}) |