Step | Hyp | Ref
| Expression |
1 | | esumlub.3 |
. . . 4
⊢ (𝜑 → 𝑋 < Σ*𝑘 ∈ 𝐴𝐵) |
2 | | esumlub.f |
. . . . . . 7
⊢
Ⅎ𝑘𝜑 |
3 | | nfcv 2904 |
. . . . . . 7
⊢
Ⅎ𝑘𝐴 |
4 | | esumlub.0 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
5 | | esumlub.1 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,]+∞)) |
6 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))) |
7 | 2, 3, 4, 5, 6 | esumval 31726 |
. . . . . 6
⊢ (𝜑 → Σ*𝑘 ∈ 𝐴𝐵 = sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))), ℝ*, <
)) |
8 | 7 | breq2d 5065 |
. . . . 5
⊢ (𝜑 → (𝑋 < Σ*𝑘 ∈ 𝐴𝐵 ↔ 𝑋 < sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))), ℝ*, <
))) |
9 | | iccssxr 13018 |
. . . . . . . . 9
⊢
(0[,]+∞) ⊆ ℝ* |
10 | | xrge0base 31013 |
. . . . . . . . . 10
⊢
(0[,]+∞) = (Base‘(ℝ*𝑠
↾s (0[,]+∞))) |
11 | | xrge0cmn 20405 |
. . . . . . . . . . 11
⊢
(ℝ*𝑠 ↾s
(0[,]+∞)) ∈ CMnd |
12 | 11 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
(ℝ*𝑠 ↾s (0[,]+∞))
∈ CMnd) |
13 | | inss2 4144 |
. . . . . . . . . . 11
⊢
(𝒫 𝐴 ∩
Fin) ⊆ Fin |
14 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) |
15 | 13, 14 | sseldi 3899 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑥 ∈ Fin) |
16 | | nfv 1922 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘 𝑥 ∈ (𝒫 𝐴 ∩ Fin) |
17 | 2, 16 | nfan 1907 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) |
18 | | simpll 767 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝜑) |
19 | | inss1 4143 |
. . . . . . . . . . . . . . . . 17
⊢
(𝒫 𝐴 ∩
Fin) ⊆ 𝒫 𝐴 |
20 | 19 | sseli 3896 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ 𝒫 𝐴) |
21 | 20 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑥 ∈ 𝒫 𝐴) |
22 | 21 | elpwid 4524 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑥 ⊆ 𝐴) |
23 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ 𝑥) |
24 | 22, 23 | sseldd 3902 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝑘 ∈ 𝐴) |
25 | 18, 24, 5 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑥) → 𝐵 ∈ (0[,]+∞)) |
26 | 25 | ex 416 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑘 ∈ 𝑥 → 𝐵 ∈ (0[,]+∞))) |
27 | 17, 26 | ralrimi 3137 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) → ∀𝑘 ∈ 𝑥 𝐵 ∈ (0[,]+∞)) |
28 | 10, 12, 15, 27 | gsummptcl 19352 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) ∈ (0[,]+∞)) |
29 | 9, 28 | sseldi 3899 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) ∈
ℝ*) |
30 | 29 | ralrimiva 3105 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (𝒫 𝐴 ∩
Fin)((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) ∈
ℝ*) |
31 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))) = (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))) |
32 | 31 | rnmptss 6939 |
. . . . . . 7
⊢
(∀𝑥 ∈
(𝒫 𝐴 ∩
Fin)((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) ∈ ℝ* → ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))) ⊆
ℝ*) |
33 | 30, 32 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))) ⊆
ℝ*) |
34 | | esumlub.2 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈
ℝ*) |
35 | | supxrlub 12915 |
. . . . . 6
⊢ ((ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))) ⊆ ℝ* ∧ 𝑋 ∈ ℝ*)
→ (𝑋 < sup(ran
(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))), ℝ*, < ) ↔
∃𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)))𝑋 < 𝑦)) |
36 | 33, 34, 35 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝑋 < sup(ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))), ℝ*, < ) ↔
∃𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)))𝑋 < 𝑦)) |
37 | 8, 36 | bitrd 282 |
. . . 4
⊢ (𝜑 → (𝑋 < Σ*𝑘 ∈ 𝐴𝐵 ↔ ∃𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)))𝑋 < 𝑦)) |
38 | 1, 37 | mpbid 235 |
. . 3
⊢ (𝜑 → ∃𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)))𝑋 < 𝑦) |
39 | | ovex 7246 |
. . . . 5
⊢
((ℝ*𝑠 ↾s
(0[,]+∞)) Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ∈ V |
40 | 39 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ∈ V) |
41 | | mpteq1 5143 |
. . . . . . . 8
⊢ (𝑥 = 𝑎 → (𝑘 ∈ 𝑥 ↦ 𝐵) = (𝑘 ∈ 𝑎 ↦ 𝐵)) |
42 | 41 | oveq2d 7229 |
. . . . . . 7
⊢ (𝑥 = 𝑎 →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)) =
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵))) |
43 | 42 | cbvmptv 5158 |
. . . . . 6
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))) = (𝑎 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵))) |
44 | 43, 39 | elrnmpti 5829 |
. . . . 5
⊢ (𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))) ↔ ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((ℝ*𝑠
↾s (0[,]+∞)) Σg (𝑘 ∈ 𝑎 ↦ 𝐵))) |
45 | 44 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵))) ↔ ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ((ℝ*𝑠
↾s (0[,]+∞)) Σg (𝑘 ∈ 𝑎 ↦ 𝐵)))) |
46 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 = ((ℝ*𝑠
↾s (0[,]+∞)) Σg (𝑘 ∈ 𝑎 ↦ 𝐵))) → 𝑦 = ((ℝ*𝑠
↾s (0[,]+∞)) Σg (𝑘 ∈ 𝑎 ↦ 𝐵))) |
47 | 46 | breq2d 5065 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 = ((ℝ*𝑠
↾s (0[,]+∞)) Σg (𝑘 ∈ 𝑎 ↦ 𝐵))) → (𝑋 < 𝑦 ↔ 𝑋 <
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)))) |
48 | 40, 45, 47 | rexxfr2d 5304 |
. . 3
⊢ (𝜑 → (∃𝑦 ∈ ran (𝑥 ∈ (𝒫 𝐴 ∩ Fin) ↦
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑥 ↦ 𝐵)))𝑋 < 𝑦 ↔ ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑋 <
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)))) |
49 | 38, 48 | mpbid 235 |
. 2
⊢ (𝜑 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑋 <
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵))) |
50 | | nfv 1922 |
. . . . . . 7
⊢
Ⅎ𝑘 𝑎 ∈ (𝒫 𝐴 ∩ Fin) |
51 | 2, 50 | nfan 1907 |
. . . . . 6
⊢
Ⅎ𝑘(𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) |
52 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) |
53 | 13, 52 | sseldi 3899 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑎 ∈ Fin) |
54 | | simpll 767 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑎) → 𝜑) |
55 | 19 | sseli 3896 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (𝒫 𝐴 ∩ Fin) → 𝑎 ∈ 𝒫 𝐴) |
56 | 55 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑎) → 𝑎 ∈ 𝒫 𝐴) |
57 | 56 | elpwid 4524 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑎) → 𝑎 ⊆ 𝐴) |
58 | | simpr 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑎) → 𝑘 ∈ 𝑎) |
59 | 57, 58 | sseldd 3902 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑎) → 𝑘 ∈ 𝐴) |
60 | 54, 59, 5 | syl2anc 587 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑘 ∈ 𝑎) → 𝐵 ∈ (0[,]+∞)) |
61 | 51, 53, 60 | gsumesum 31739 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) →
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) = Σ*𝑘 ∈ 𝑎𝐵) |
62 | 61 | breq2d 5065 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑋 <
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) ↔ 𝑋 < Σ*𝑘 ∈ 𝑎𝐵)) |
63 | 62 | biimpd 232 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑋 <
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) → 𝑋 < Σ*𝑘 ∈ 𝑎𝐵)) |
64 | 63 | reximdva 3193 |
. 2
⊢ (𝜑 → (∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑋 <
((ℝ*𝑠 ↾s (0[,]+∞))
Σg (𝑘 ∈ 𝑎 ↦ 𝐵)) → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑋 < Σ*𝑘 ∈ 𝑎𝐵)) |
65 | 49, 64 | mpd 15 |
1
⊢ (𝜑 → ∃𝑎 ∈ (𝒫 𝐴 ∩ Fin)𝑋 < Σ*𝑘 ∈ 𝑎𝐵) |