Step | Hyp | Ref
| Expression |
1 | | xrge0tsmsd.s |
. . . . 5
⊢ (𝜑 → 𝑆 = sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, <
)) |
2 | | iccssxr 12127 |
. . . . . . . . 9
⊢
(0[,]+∞) ⊆ ℝ* |
3 | | xrge0tsmsd.g |
. . . . . . . . . . . 12
⊢ 𝐺 =
(ℝ*𝑠 ↾s
(0[,]+∞)) |
4 | | xrsbas 19581 |
. . . . . . . . . . . 12
⊢
ℝ* =
(Base‘ℝ*𝑠) |
5 | 3, 4 | ressbas2 15758 |
. . . . . . . . . . 11
⊢
((0[,]+∞) ⊆ ℝ* → (0[,]+∞) =
(Base‘𝐺)) |
6 | 2, 5 | ax-mp 5 |
. . . . . . . . . 10
⊢
(0[,]+∞) = (Base‘𝐺) |
7 | | eqid 2610 |
. . . . . . . . . 10
⊢
(0g‘𝐺) = (0g‘𝐺) |
8 | | xrge0cmn 19607 |
. . . . . . . . . . . 12
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ CMnd |
9 | 3, 8 | eqeltri 2684 |
. . . . . . . . . . 11
⊢ 𝐺 ∈ CMnd |
10 | 9 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐺 ∈ CMnd) |
11 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) |
12 | | xrge0tsmsd.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐴⟶(0[,]+∞)) |
13 | | elfpw 8151 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑠 ⊆ 𝐴 ∧ 𝑠 ∈ Fin)) |
14 | 13 | simplbi 475 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) → 𝑠 ⊆ 𝐴) |
15 | | fssres 5983 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶(0[,]+∞) ∧ 𝑠 ⊆ 𝐴) → (𝐹 ↾ 𝑠):𝑠⟶(0[,]+∞)) |
16 | 12, 14, 15 | syl2an 493 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑠):𝑠⟶(0[,]+∞)) |
17 | | elinel2 3762 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) → 𝑠 ∈ Fin) |
18 | 17 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑠 ∈ Fin) |
19 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
(0g‘𝐺) ∈ V |
20 | 19 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) →
(0g‘𝐺)
∈ V) |
21 | 16, 18, 20 | fdmfifsupp 8168 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑠) finSupp (0g‘𝐺)) |
22 | 6, 7, 10, 11, 16, 21 | gsumcl 18139 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑠)) ∈ (0[,]+∞)) |
23 | 2, 22 | sseldi 3566 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑠)) ∈
ℝ*) |
24 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) = (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) |
25 | 23, 24 | fmptd 6292 |
. . . . . . 7
⊢ (𝜑 → (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))):(𝒫 𝐴 ∩
Fin)⟶ℝ*) |
26 | | frn 5966 |
. . . . . . 7
⊢ ((𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))):(𝒫 𝐴 ∩ Fin)⟶ℝ*
→ ran (𝑠 ∈
(𝒫 𝐴 ∩ Fin)
↦ (𝐺
Σg (𝐹 ↾ 𝑠))) ⊆
ℝ*) |
27 | 25, 26 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) ⊆
ℝ*) |
28 | | supxrcl 12017 |
. . . . . 6
⊢ (ran
(𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) ⊆ ℝ*
→ sup(ran (𝑠 ∈
(𝒫 𝐴 ∩ Fin)
↦ (𝐺
Σg (𝐹 ↾ 𝑠))), ℝ*, < ) ∈
ℝ*) |
29 | 27, 28 | syl 17 |
. . . . 5
⊢ (𝜑 → sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))), ℝ*, < )
∈ ℝ*) |
30 | 1, 29 | eqeltrd 2688 |
. . . 4
⊢ (𝜑 → 𝑆 ∈
ℝ*) |
31 | | 0ss 3924 |
. . . . . . . 8
⊢ ∅
⊆ 𝐴 |
32 | | 0fin 8073 |
. . . . . . . 8
⊢ ∅
∈ Fin |
33 | | elfpw 8151 |
. . . . . . . 8
⊢ (∅
∈ (𝒫 𝐴 ∩
Fin) ↔ (∅ ⊆ 𝐴 ∧ ∅ ∈ Fin)) |
34 | 31, 32, 33 | mpbir2an 957 |
. . . . . . 7
⊢ ∅
∈ (𝒫 𝐴 ∩
Fin) |
35 | | 0cn 9911 |
. . . . . . 7
⊢ 0 ∈
ℂ |
36 | | reseq2 5312 |
. . . . . . . . . . 11
⊢ (𝑠 = ∅ → (𝐹 ↾ 𝑠) = (𝐹 ↾ ∅)) |
37 | | res0 5321 |
. . . . . . . . . . 11
⊢ (𝐹 ↾ ∅) =
∅ |
38 | 36, 37 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (𝑠 = ∅ → (𝐹 ↾ 𝑠) = ∅) |
39 | 38 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑠 = ∅ → (𝐺 Σg
(𝐹 ↾ 𝑠)) = (𝐺 Σg
∅)) |
40 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) =
(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) |
41 | 40 | xrge0subm 19606 |
. . . . . . . . . . 11
⊢
(0[,]+∞) ∈
(SubMnd‘(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞}))) |
42 | | xrex 11705 |
. . . . . . . . . . . . . . 15
⊢
ℝ* ∈ V |
43 | | difexg 4735 |
. . . . . . . . . . . . . . 15
⊢
(ℝ* ∈ V → (ℝ* ∖
{-∞}) ∈ V) |
44 | 42, 43 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(ℝ* ∖ {-∞}) ∈ V |
45 | | simpl 472 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ*
∧ 0 ≤ 𝑥) →
𝑥 ∈
ℝ*) |
46 | | ge0nemnf 11878 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ*
∧ 0 ≤ 𝑥) →
𝑥 ≠
-∞) |
47 | 45, 46 | jca 553 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ*
∧ 0 ≤ 𝑥) →
(𝑥 ∈
ℝ* ∧ 𝑥
≠ -∞)) |
48 | | elxrge0 12152 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (0[,]+∞) ↔
(𝑥 ∈
ℝ* ∧ 0 ≤ 𝑥)) |
49 | | eldifsn 4260 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (ℝ*
∖ {-∞}) ↔ (𝑥 ∈ ℝ* ∧ 𝑥 ≠
-∞)) |
50 | 47, 48, 49 | 3imtr4i 280 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (0[,]+∞) →
𝑥 ∈
(ℝ* ∖ {-∞})) |
51 | 50 | ssriv 3572 |
. . . . . . . . . . . . . 14
⊢
(0[,]+∞) ⊆ (ℝ* ∖
{-∞}) |
52 | | ressabs 15766 |
. . . . . . . . . . . . . 14
⊢
(((ℝ* ∖ {-∞}) ∈ V ∧ (0[,]+∞)
⊆ (ℝ* ∖ {-∞})) →
((ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ↾s (0[,]+∞)) =
(ℝ*𝑠 ↾s
(0[,]+∞))) |
53 | 44, 51, 52 | mp2an 704 |
. . . . . . . . . . . . 13
⊢
((ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ↾s (0[,]+∞)) =
(ℝ*𝑠 ↾s
(0[,]+∞)) |
54 | 3, 53 | eqtr4i 2635 |
. . . . . . . . . . . 12
⊢ 𝐺 =
((ℝ*𝑠 ↾s
(ℝ* ∖ {-∞})) ↾s
(0[,]+∞)) |
55 | 40 | xrs10 19604 |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘(ℝ*𝑠
↾s (ℝ* ∖ {-∞}))) |
56 | 54, 55 | subm0 17179 |
. . . . . . . . . . 11
⊢
((0[,]+∞) ∈
(SubMnd‘(ℝ*𝑠 ↾s
(ℝ* ∖ {-∞}))) → 0 =
(0g‘𝐺)) |
57 | 41, 56 | ax-mp 5 |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝐺) |
58 | 57 | gsum0 17101 |
. . . . . . . . 9
⊢ (𝐺 Σg
∅) = 0 |
59 | 39, 58 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝑠 = ∅ → (𝐺 Σg
(𝐹 ↾ 𝑠)) = 0) |
60 | 24, 59 | elrnmpt1s 5294 |
. . . . . . 7
⊢ ((∅
∈ (𝒫 𝐴 ∩
Fin) ∧ 0 ∈ ℂ) → 0 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))) |
61 | 34, 35, 60 | mp2an 704 |
. . . . . 6
⊢ 0 ∈
ran (𝑠 ∈ (𝒫
𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) |
62 | | supxrub 12026 |
. . . . . 6
⊢ ((ran
(𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) ⊆ ℝ*
∧ 0 ∈ ran (𝑠
∈ (𝒫 𝐴 ∩
Fin) ↦ (𝐺
Σg (𝐹 ↾ 𝑠)))) → 0 ≤ sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))), ℝ*, <
)) |
63 | 27, 61, 62 | sylancl 693 |
. . . . 5
⊢ (𝜑 → 0 ≤ sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))), ℝ*, <
)) |
64 | 63, 1 | breqtrrd 4611 |
. . . 4
⊢ (𝜑 → 0 ≤ 𝑆) |
65 | | elxrge0 12152 |
. . . 4
⊢ (𝑆 ∈ (0[,]+∞) ↔
(𝑆 ∈
ℝ* ∧ 0 ≤ 𝑆)) |
66 | 30, 64, 65 | sylanbrc 695 |
. . 3
⊢ (𝜑 → 𝑆 ∈ (0[,]+∞)) |
67 | | letop 20820 |
. . . . . 6
⊢
(ordTop‘ ≤ ) ∈ Top |
68 | | ovex 6577 |
. . . . . 6
⊢
(0[,]+∞) ∈ V |
69 | | elrest 15911 |
. . . . . 6
⊢
(((ordTop‘ ≤ ) ∈ Top ∧ (0[,]+∞) ∈ V) →
(𝑢 ∈ ((ordTop‘
≤ ) ↾t (0[,]+∞)) ↔ ∃𝑣 ∈ (ordTop‘ ≤ )𝑢 = (𝑣 ∩ (0[,]+∞)))) |
70 | 67, 68, 69 | mp2an 704 |
. . . . 5
⊢ (𝑢 ∈ ((ordTop‘ ≤ )
↾t (0[,]+∞)) ↔ ∃𝑣 ∈ (ordTop‘ ≤ )𝑢 = (𝑣 ∩ (0[,]+∞))) |
71 | | elinel1 3761 |
. . . . . . . 8
⊢ (𝑆 ∈ (𝑣 ∩ (0[,]+∞)) → 𝑆 ∈ 𝑣) |
72 | | simplrl 796 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑣 ∈ (ordTop‘ ≤
)) |
73 | | reex 9906 |
. . . . . . . . . . . . . . 15
⊢ ℝ
∈ V |
74 | | elrestr 15912 |
. . . . . . . . . . . . . . 15
⊢
(((ordTop‘ ≤ ) ∈ Top ∧ ℝ ∈ V ∧ 𝑣 ∈ (ordTop‘ ≤ ))
→ (𝑣 ∩ ℝ)
∈ ((ordTop‘ ≤ ) ↾t ℝ)) |
75 | 67, 73, 74 | mp3an12 1406 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ (ordTop‘ ≤ )
→ (𝑣 ∩ ℝ)
∈ ((ordTop‘ ≤ ) ↾t ℝ)) |
76 | 72, 75 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (𝑣 ∩ ℝ) ∈ ((ordTop‘ ≤ )
↾t ℝ)) |
77 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
((ordTop‘ ≤ ) ↾t ℝ) = ((ordTop‘
≤ ) ↾t ℝ) |
78 | 77 | xrtgioo 22417 |
. . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) = ((ordTop‘ ≤ ) ↾t
ℝ) |
79 | 76, 78 | syl6eleqr 2699 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (𝑣 ∩ ℝ) ∈ (topGen‘ran
(,))) |
80 | | simplrr 797 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑆 ∈ 𝑣) |
81 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑆 ∈ ℝ) |
82 | 80, 81 | elind 3760 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → 𝑆 ∈ (𝑣 ∩ ℝ)) |
83 | | tg2 20580 |
. . . . . . . . . . . 12
⊢ (((𝑣 ∩ ℝ) ∈
(topGen‘ran (,)) ∧ 𝑆 ∈ (𝑣 ∩ ℝ)) → ∃𝑢 ∈ ran (,)(𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ))) |
84 | 79, 82, 83 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → ∃𝑢 ∈ ran (,)(𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ))) |
85 | | ioof 12142 |
. . . . . . . . . . . . . 14
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
86 | | ffn 5958 |
. . . . . . . . . . . . . 14
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
87 | | ovelrn 6708 |
. . . . . . . . . . . . . 14
⊢ ((,) Fn
(ℝ* × ℝ*) → (𝑢 ∈ ran (,) ↔ ∃𝑟 ∈ ℝ*
∃𝑤 ∈
ℝ* 𝑢 =
(𝑟(,)𝑤))) |
88 | 85, 86, 87 | mp2b 10 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ ran (,) ↔
∃𝑟 ∈
ℝ* ∃𝑤 ∈ ℝ* 𝑢 = (𝑟(,)𝑤)) |
89 | | simprrr 801 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)) |
90 | 89 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)) |
91 | | inss1 3795 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑣 ∩ ℝ) ⊆ 𝑣 |
92 | 90, 91 | syl6ss 3580 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝑟(,)𝑤) ⊆ 𝑣) |
93 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝐺 ∈ CMnd) |
94 | | simprrl 800 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) |
95 | | elinel2 3762 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ∈ Fin) |
97 | | simp-4l 802 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝜑) |
98 | 97, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝐹:𝐴⟶(0[,]+∞)) |
99 | | elfpw 8151 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ∈ Fin)) |
100 | 99 | simplbi 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴) |
101 | 94, 100 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ⊆ 𝐴) |
102 | 98, 101 | fssresd 5984 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑦):𝑦⟶(0[,]+∞)) |
103 | | ffun 5961 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐹:𝐴⟶(0[,]+∞) → Fun 𝐹) |
104 | 12, 103 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → Fun 𝐹) |
105 | 104 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → Fun 𝐹) |
106 | 105 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → Fun 𝐹) |
107 | | c0ex 9913 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 ∈
V |
108 | 107 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 0 ∈ V) |
109 | 106, 96, 108 | resfifsupp 8186 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑦) finSupp 0) |
110 | 6, 57, 93, 96, 102, 109 | gsumcl 18139 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (0[,]+∞)) |
111 | 2, 110 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈
ℝ*) |
112 | | simprll 798 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑟 ∈ ℝ*) |
113 | 112 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑟 ∈ ℝ*) |
114 | | simprll 798 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) |
115 | | simprrr 801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ⊆ 𝑦) |
116 | 115, 101 | sstrd 3578 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ⊆ 𝐴) |
117 | 98, 116 | fssresd 5984 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑧):𝑧⟶(0[,]+∞)) |
118 | | ssfi 8065 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑦 ∈ Fin ∧ 𝑧 ⊆ 𝑦) → 𝑧 ∈ Fin) |
119 | 96, 115, 118 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ∈ Fin) |
120 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (0g‘𝐺) ∈ V) |
121 | 117, 119,
120 | fdmfifsupp 8168 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐹 ↾ 𝑧) finSupp (0g‘𝐺)) |
122 | 6, 7, 93, 114, 117, 121 | gsumcl 18139 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ (0[,]+∞)) |
123 | 2, 122 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈
ℝ*) |
124 | | simprlr 799 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) |
125 | | xrge0tsmsd.a |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
126 | 97, 125 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝐴 ∈ 𝑉) |
127 | 3, 126, 98, 94, 115 | xrge0gsumle 22444 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑧)) ≤ (𝐺 Σg (𝐹 ↾ 𝑦))) |
128 | 113, 123,
111, 124, 127 | xrltletrd 11868 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑦))) |
129 | 97, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑆 ∈
ℝ*) |
130 | | simprlr 799 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑤 ∈ ℝ*) |
131 | 130 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑤 ∈ ℝ*) |
132 | 97, 27 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) ⊆
ℝ*) |
133 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐺 Σg
(𝐹 ↾ 𝑦)) ∈ V |
134 | | reseq2 5312 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑠 = 𝑦 → (𝐹 ↾ 𝑠) = (𝐹 ↾ 𝑦)) |
135 | 134 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑠 = 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑠)) = (𝐺 Σg (𝐹 ↾ 𝑦))) |
136 | 24, 135 | elrnmpt1s 5294 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ (𝐺 Σg
(𝐹 ↾ 𝑦)) ∈ V) → (𝐺 Σg
(𝐹 ↾ 𝑦)) ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠)))) |
137 | 94, 133, 136 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))) |
138 | | supxrub 12026 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((ran
(𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) ⊆ ℝ*
∧ (𝐺
Σg (𝐹 ↾ 𝑦)) ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ≤ sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, <
)) |
139 | 132, 137,
138 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ≤ sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, <
)) |
140 | 97, 1 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑆 = sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, <
)) |
141 | 139, 140 | breqtrrd 4611 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ≤ 𝑆) |
142 | | simprrl 800 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑆 ∈ (𝑟(,)𝑤)) |
143 | | eliooord 12104 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑆 ∈ (𝑟(,)𝑤) → (𝑟 < 𝑆 ∧ 𝑆 < 𝑤)) |
144 | 142, 143 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → (𝑟 < 𝑆 ∧ 𝑆 < 𝑤)) |
145 | 144 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑆 < 𝑤) |
146 | 145 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → 𝑆 < 𝑤) |
147 | 111, 129,
131, 141, 146 | xrlelttrd 11867 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) < 𝑤) |
148 | | elioo1 12086 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑟 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑟(,)𝑤) ↔ ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ ℝ* ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑦)) ∧ (𝐺 Σg (𝐹 ↾ 𝑦)) < 𝑤))) |
149 | 113, 131,
148 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑟(,)𝑤) ↔ ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ ℝ* ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑦)) ∧ (𝐺 Σg (𝐹 ↾ 𝑦)) < 𝑤))) |
150 | 111, 128,
147, 149 | mpbir3and 1238 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑟(,)𝑤)) |
151 | 92, 150 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣) |
152 | 151, 110 | elind 3760 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ ((𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦))) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))) |
153 | 152 | anassrs 678 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))) |
154 | 153 | expr 641 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) |
155 | 154 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) → ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) |
156 | 144 | simpld 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑟 < 𝑆) |
157 | 1 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑆 = sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, <
)) |
158 | 156, 157 | breqtrd 4609 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → 𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, <
)) |
159 | 27 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) ⊆
ℝ*) |
160 | | supxrlub 12027 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ran
(𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) ⊆ ℝ*
∧ 𝑟 ∈
ℝ*) → (𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < ) ↔
∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠)))𝑟 < 𝑤)) |
161 | 159, 112,
160 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → (𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < ) ↔
∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠)))𝑟 < 𝑤)) |
162 | 158, 161 | mpbid 221 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))𝑟 < 𝑤) |
163 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐺 Σg
(𝐹 ↾ 𝑧)) ∈ V |
164 | 163 | rgenw 2908 |
. . . . . . . . . . . . . . . . . . 19
⊢
∀𝑧 ∈
(𝒫 𝐴 ∩
Fin)(𝐺
Σg (𝐹 ↾ 𝑧)) ∈ V |
165 | | reseq2 5312 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠 = 𝑧 → (𝐹 ↾ 𝑠) = (𝐹 ↾ 𝑧)) |
166 | 165 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑠)) = (𝐺 Σg (𝐹 ↾ 𝑧))) |
167 | 166 | cbvmptv 4678 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠))) = (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑧))) |
168 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = (𝐺 Σg (𝐹 ↾ 𝑧)) → (𝑟 < 𝑤 ↔ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) |
169 | 167, 168 | rexrnmpt 6277 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑧 ∈
(𝒫 𝐴 ∩
Fin)(𝐺
Σg (𝐹 ↾ 𝑧)) ∈ V → (∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))𝑟 < 𝑤 ↔ ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) |
170 | 164, 169 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑤 ∈ ran
(𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠)))𝑟 < 𝑤 ↔ ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) |
171 | 162, 170 | sylib 207 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) |
172 | 155, 171 | reximddv 3001 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ ((𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
∧ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) |
173 | 172 | expr 641 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ (𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*))
→ ((𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))) |
174 | | eleq2 2677 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = (𝑟(,)𝑤) → (𝑆 ∈ 𝑢 ↔ 𝑆 ∈ (𝑟(,)𝑤))) |
175 | | sseq1 3589 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = (𝑟(,)𝑤) → (𝑢 ⊆ (𝑣 ∩ ℝ) ↔ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ))) |
176 | 174, 175 | anbi12d 743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = (𝑟(,)𝑤) → ((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) ↔ (𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)))) |
177 | 176 | imbi1d 330 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = (𝑟(,)𝑤) → (((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) ↔ ((𝑆 ∈ (𝑟(,)𝑤) ∧ (𝑟(,)𝑤) ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))) |
178 | 173, 177 | syl5ibrcom 236 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) ∧ (𝑟 ∈ ℝ* ∧ 𝑤 ∈ ℝ*))
→ (𝑢 = (𝑟(,)𝑤) → ((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))) |
179 | 178 | rexlimdvva 3020 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (∃𝑟 ∈ ℝ*
∃𝑤 ∈
ℝ* 𝑢 =
(𝑟(,)𝑤) → ((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))) |
180 | 88, 179 | syl5bi 231 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (𝑢 ∈ ran (,) → ((𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))) |
181 | 180 | rexlimdv 3012 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → (∃𝑢 ∈ ran (,)(𝑆 ∈ 𝑢 ∧ 𝑢 ⊆ (𝑣 ∩ ℝ)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))) |
182 | 84, 181 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 ∈ ℝ) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) |
183 | | simplrl 796 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → 𝑣 ∈ (ordTop‘ ≤
)) |
184 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → 𝑆 = +∞) |
185 | | simplrr 797 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → 𝑆 ∈ 𝑣) |
186 | 184, 185 | eqeltrrd 2689 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → +∞ ∈ 𝑣) |
187 | | pnfnei 20834 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ (ordTop‘ ≤ )
∧ +∞ ∈ 𝑣)
→ ∃𝑟 ∈
ℝ (𝑟(,]+∞)
⊆ 𝑣) |
188 | 183, 186,
187 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → ∃𝑟 ∈ ℝ (𝑟(,]+∞) ⊆ 𝑣) |
189 | | simprr 792 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → (𝑟(,]+∞) ⊆ 𝑣) |
190 | 189 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝑟(,]+∞) ⊆ 𝑣) |
191 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝐺 ∈ CMnd) |
192 | | simprl 790 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) |
193 | | simp-5l 804 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝜑) |
194 | 193, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝐹:𝐴⟶(0[,]+∞)) |
195 | 100 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑦 ⊆ 𝐴) |
196 | 194, 195 | fssresd 5984 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑦):𝑦⟶(0[,]+∞)) |
197 | 95 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑦 ∈ Fin) |
198 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (0g‘𝐺) ∈ V) |
199 | 196, 197,
198 | fdmfifsupp 8168 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑦) finSupp (0g‘𝐺)) |
200 | 6, 7, 191, 192, 196, 199 | gsumcl 18139 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (0[,]+∞)) |
201 | 2, 200 | sseldi 3566 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈
ℝ*) |
202 | | rexr 9964 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 ∈ ℝ → 𝑟 ∈
ℝ*) |
203 | 202 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 ∈ ℝ*) |
204 | 203 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑟 ∈ ℝ*) |
205 | | simplrl 796 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) |
206 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑧 ⊆ 𝑦) |
207 | 206, 195 | sstrd 3578 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑧 ⊆ 𝐴) |
208 | 194, 207 | fssresd 5984 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑧):𝑧⟶(0[,]+∞)) |
209 | 197, 206,
118 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑧 ∈ Fin) |
210 | 208, 209,
198 | fdmfifsupp 8168 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐹 ↾ 𝑧) finSupp (0g‘𝐺)) |
211 | 6, 7, 191, 205, 208, 210 | gsumcl 18139 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ (0[,]+∞)) |
212 | 2, 211 | sseldi 3566 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈
ℝ*) |
213 | | simplrr 797 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) |
214 | 193, 125 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝐴 ∈ 𝑉) |
215 | 3, 214, 194, 192, 206 | xrge0gsumle 22444 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑧)) ≤ (𝐺 Σg (𝐹 ↾ 𝑦))) |
216 | 204, 212,
201, 213, 215 | xrltletrd 11868 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑦))) |
217 | | pnfge 11840 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 Σg
(𝐹 ↾ 𝑦)) ∈ ℝ*
→ (𝐺
Σg (𝐹 ↾ 𝑦)) ≤ +∞) |
218 | 201, 217 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ≤ +∞) |
219 | | pnfxr 9971 |
. . . . . . . . . . . . . . . . . 18
⊢ +∞
∈ ℝ* |
220 | | elioc1 12088 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑟 ∈ ℝ*
∧ +∞ ∈ ℝ*) → ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑟(,]+∞) ↔ ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ ℝ* ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑦)) ∧ (𝐺 Σg (𝐹 ↾ 𝑦)) ≤ +∞))) |
221 | 204, 219,
220 | sylancl 693 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑟(,]+∞) ↔ ((𝐺 Σg (𝐹 ↾ 𝑦)) ∈ ℝ* ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑦)) ∧ (𝐺 Σg (𝐹 ↾ 𝑦)) ≤ +∞))) |
222 | 201, 216,
218, 221 | mpbir3and 1238 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑟(,]+∞)) |
223 | 190, 222 | sseldd 3569 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑣) |
224 | 223, 200 | elind 3760 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑧 ⊆ 𝑦)) → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))) |
225 | 224 | expr 641 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) |
226 | 225 | ralrimiva 2949 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ )
∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧)))) → ∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) |
227 | | ltpnf 11830 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 ∈ ℝ → 𝑟 < +∞) |
228 | 227 | ad2antrl 760 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 < +∞) |
229 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑆 = +∞) |
230 | 228, 229 | breqtrrd 4611 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 < 𝑆) |
231 | 1 | ad3antrrr 762 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑆 = sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, <
)) |
232 | 230, 231 | breqtrd 4609 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → 𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, <
)) |
233 | 27 | ad3antrrr 762 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))) ⊆
ℝ*) |
234 | 233, 203,
160 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → (𝑟 < sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < ) ↔
∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg
(𝐹 ↾ 𝑠)))𝑟 < 𝑤)) |
235 | 232, 234 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → ∃𝑤 ∈ ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠)))𝑟 < 𝑤) |
236 | 235, 170 | sylib 207 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)𝑟 < (𝐺 Σg (𝐹 ↾ 𝑧))) |
237 | 226, 236 | reximddv 3001 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) ∧ (𝑟 ∈ ℝ ∧ (𝑟(,]+∞) ⊆ 𝑣)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) |
238 | 188, 237 | rexlimddv 3017 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) ∧ 𝑆 = +∞) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) |
239 | | ge0nemnf 11878 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ ℝ*
∧ 0 ≤ 𝑆) →
𝑆 ≠
-∞) |
240 | 30, 64, 239 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ≠ -∞) |
241 | 30, 240 | jca 553 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 ∈ ℝ* ∧ 𝑆 ≠
-∞)) |
242 | 241 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) → (𝑆 ∈ ℝ* ∧ 𝑆 ≠
-∞)) |
243 | | xrnemnf 11827 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ ℝ*
∧ 𝑆 ≠ -∞)
↔ (𝑆 ∈ ℝ
∨ 𝑆 =
+∞)) |
244 | 242, 243 | sylib 207 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) → (𝑆 ∈ ℝ ∨ 𝑆 = +∞)) |
245 | 182, 238,
244 | mpjaodan 823 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ (ordTop‘ ≤ ) ∧ 𝑆 ∈ 𝑣)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) |
246 | 245 | expr 641 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 ∈ (ordTop‘ ≤ )) → (𝑆 ∈ 𝑣 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))) |
247 | 71, 246 | syl5 33 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ (ordTop‘ ≤ )) → (𝑆 ∈ (𝑣 ∩ (0[,]+∞)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))) |
248 | | eleq2 2677 |
. . . . . . . 8
⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → (𝑆 ∈ 𝑢 ↔ 𝑆 ∈ (𝑣 ∩ (0[,]+∞)))) |
249 | | eleq2 2677 |
. . . . . . . . . 10
⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → ((𝐺 Σg
(𝐹 ↾ 𝑦)) ∈ 𝑢 ↔ (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))) |
250 | 249 | imbi2d 329 |
. . . . . . . . 9
⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → ((𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢) ↔ (𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))) |
251 | 250 | rexralbidv 3040 |
. . . . . . . 8
⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → (∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢) ↔ ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞))))) |
252 | 248, 251 | imbi12d 333 |
. . . . . . 7
⊢ (𝑢 = (𝑣 ∩ (0[,]+∞)) → ((𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)) ↔ (𝑆 ∈ (𝑣 ∩ (0[,]+∞)) → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ (𝑣 ∩ (0[,]+∞)))))) |
253 | 247, 252 | syl5ibrcom 236 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ (ordTop‘ ≤ )) → (𝑢 = (𝑣 ∩ (0[,]+∞)) → (𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)))) |
254 | 253 | rexlimdva 3013 |
. . . . 5
⊢ (𝜑 → (∃𝑣 ∈ (ordTop‘ ≤ )𝑢 = (𝑣 ∩ (0[,]+∞)) → (𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)))) |
255 | 70, 254 | syl5bi 231 |
. . . 4
⊢ (𝜑 → (𝑢 ∈ ((ordTop‘ ≤ )
↾t (0[,]+∞)) → (𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢)))) |
256 | 255 | ralrimiv 2948 |
. . 3
⊢ (𝜑 → ∀𝑢 ∈ ((ordTop‘ ≤ )
↾t (0[,]+∞))(𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢))) |
257 | | xrstset 19584 |
. . . . . . 7
⊢
(ordTop‘ ≤ ) =
(TopSet‘ℝ*𝑠) |
258 | 3, 257 | resstset 15869 |
. . . . . 6
⊢
((0[,]+∞) ∈ V → (ordTop‘ ≤ ) =
(TopSet‘𝐺)) |
259 | 68, 258 | ax-mp 5 |
. . . . 5
⊢
(ordTop‘ ≤ ) = (TopSet‘𝐺) |
260 | 6, 259 | topnval 15918 |
. . . 4
⊢
((ordTop‘ ≤ ) ↾t (0[,]+∞)) =
(TopOpen‘𝐺) |
261 | | eqid 2610 |
. . . 4
⊢
(𝒫 𝐴 ∩
Fin) = (𝒫 𝐴 ∩
Fin) |
262 | 9 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ CMnd) |
263 | | xrstps 20823 |
. . . . . . 7
⊢
ℝ*𝑠 ∈ TopSp |
264 | | resstps 20801 |
. . . . . . 7
⊢
((ℝ*𝑠 ∈ TopSp ∧
(0[,]+∞) ∈ V) → (ℝ*𝑠
↾s (0[,]+∞)) ∈ TopSp) |
265 | 263, 68, 264 | mp2an 704 |
. . . . . 6
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ TopSp |
266 | 3, 265 | eqeltri 2684 |
. . . . 5
⊢ 𝐺 ∈ TopSp |
267 | 266 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ TopSp) |
268 | 6, 260, 261, 262, 267, 125, 12 | eltsms 21746 |
. . 3
⊢ (𝜑 → (𝑆 ∈ (𝐺 tsums 𝐹) ↔ (𝑆 ∈ (0[,]+∞) ∧ ∀𝑢 ∈ ((ordTop‘ ≤ )
↾t (0[,]+∞))(𝑆 ∈ 𝑢 → ∃𝑧 ∈ (𝒫 𝐴 ∩ Fin)∀𝑦 ∈ (𝒫 𝐴 ∩ Fin)(𝑧 ⊆ 𝑦 → (𝐺 Σg (𝐹 ↾ 𝑦)) ∈ 𝑢))))) |
269 | 66, 256, 268 | mpbir2and 959 |
. 2
⊢ (𝜑 → 𝑆 ∈ (𝐺 tsums 𝐹)) |
270 | | letsr 17050 |
. . . . 5
⊢ ≤
∈ TosetRel |
271 | | ordthaus 20998 |
. . . . 5
⊢ ( ≤
∈ TosetRel → (ordTop‘ ≤ ) ∈ Haus) |
272 | 270, 271 | mp1i 13 |
. . . 4
⊢ (𝜑 → (ordTop‘ ≤ )
∈ Haus) |
273 | | resthaus 20982 |
. . . 4
⊢
(((ordTop‘ ≤ ) ∈ Haus ∧ (0[,]+∞) ∈ V)
→ ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈
Haus) |
274 | 272, 68, 273 | sylancl 693 |
. . 3
⊢ (𝜑 → ((ordTop‘ ≤ )
↾t (0[,]+∞)) ∈ Haus) |
275 | 6, 262, 267, 125, 12, 260, 274 | haustsms2 21750 |
. 2
⊢ (𝜑 → (𝑆 ∈ (𝐺 tsums 𝐹) → (𝐺 tsums 𝐹) = {𝑆})) |
276 | 269, 275 | mpd 15 |
1
⊢ (𝜑 → (𝐺 tsums 𝐹) = {𝑆}) |