Step | Hyp | Ref
| Expression |
1 | | omssubadd.b |
. . . . . 6
⊢ (𝜑 → 𝑋 ≼ ω) |
2 | | nnenom 12641 |
. . . . . . 7
⊢ ℕ
≈ ω |
3 | 2 | ensymi 7892 |
. . . . . 6
⊢ ω
≈ ℕ |
4 | | domentr 7901 |
. . . . . 6
⊢ ((𝑋 ≼ ω ∧ ω
≈ ℕ) → 𝑋
≼ ℕ) |
5 | 1, 3, 4 | sylancl 693 |
. . . . 5
⊢ (𝜑 → 𝑋 ≼ ℕ) |
6 | | brdomi 7852 |
. . . . 5
⊢ (𝑋 ≼ ℕ →
∃𝑓 𝑓:𝑋–1-1→ℕ) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝜑 → ∃𝑓 𝑓:𝑋–1-1→ℕ) |
8 | 7 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → ∃𝑓 𝑓:𝑋–1-1→ℕ) |
9 | | simplll 794 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝜑) |
10 | | ctex 7856 |
. . . . . . . . . . 11
⊢ (𝑋 ≼ ω → 𝑋 ∈ V) |
11 | 1, 10 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ V) |
12 | 9, 11 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑋 ∈ V) |
13 | | nfv 1830 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦𝜑 |
14 | | nfcv 2751 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦𝑋 |
15 | 14 | nfesum1 29429 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) |
16 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦ℝ |
17 | 15, 16 | nfel 2763 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ |
18 | 13, 17 | nfan 1816 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) |
19 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦 𝑓:𝑋–1-1→ℕ |
20 | 18, 19 | nfan 1816 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) |
21 | | nfv 1830 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 𝑒 ∈
ℝ+ |
22 | 20, 21 | nfan 1816 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) |
23 | 9 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝜑) |
24 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
25 | 11 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → 𝑋 ∈ V) |
26 | | oms.o |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑄 ∈ 𝑉) |
27 | | oms.r |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑅:𝑄⟶(0[,]+∞)) |
28 | | omsf 29685 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞)) →
(toOMeas‘𝑅):𝒫
∪ dom 𝑅⟶(0[,]+∞)) |
29 | | oms.m |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑀 = (toOMeas‘𝑅) |
30 | 29 | feq1i 5949 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑀:𝒫 ∪ dom 𝑅⟶(0[,]+∞) ↔
(toOMeas‘𝑅):𝒫
∪ dom 𝑅⟶(0[,]+∞)) |
31 | 28, 30 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞)) → 𝑀:𝒫 ∪ dom 𝑅⟶(0[,]+∞)) |
32 | 26, 27, 31 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑀:𝒫 ∪ dom
𝑅⟶(0[,]+∞)) |
33 | 32 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑀:𝒫 ∪ dom
𝑅⟶(0[,]+∞)) |
34 | | omssubadd.a |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ⊆ ∪ 𝑄) |
35 | | fdm 5964 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑅:𝑄⟶(0[,]+∞) → dom 𝑅 = 𝑄) |
36 | 27, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → dom 𝑅 = 𝑄) |
37 | 36 | unieqd 4382 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ∪ dom 𝑅 = ∪ 𝑄) |
38 | 37 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∪ dom
𝑅 = ∪ 𝑄) |
39 | 34, 38 | sseqtr4d 3605 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ⊆ ∪ dom
𝑅) |
40 | | uniexg 6853 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑄 ∈ 𝑉 → ∪ 𝑄 ∈ V) |
41 | 26, 40 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ∪ 𝑄
∈ V) |
42 | 41 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∪ 𝑄 ∈ V) |
43 | | ssexg 4732 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ⊆ ∪ 𝑄
∧ ∪ 𝑄 ∈ V) → 𝐴 ∈ V) |
44 | 34, 42, 43 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ∈ V) |
45 | | elpwg 4116 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 ∪ dom 𝑅 ↔ 𝐴 ⊆ ∪ dom
𝑅)) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐴 ∈ 𝒫 ∪ dom 𝑅 ↔ 𝐴 ⊆ ∪ dom
𝑅)) |
47 | 39, 46 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ∈ 𝒫 ∪ dom 𝑅) |
48 | 33, 47 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞)) |
49 | 48 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞)) |
50 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) →
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) |
51 | 18, 25, 49, 50 | esumcvgre 29480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ ℝ) |
52 | 51 | adantlr 747 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ ℝ) |
53 | 52 | adantlr 747 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ ℝ) |
54 | | rpssre 11719 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℝ+ ⊆ ℝ |
55 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℝ+) |
56 | | 2rp 11713 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℝ+ |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → 2 ∈
ℝ+) |
58 | | df-f1 5809 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓:𝑋–1-1→ℕ ↔ (𝑓:𝑋⟶ℕ ∧ Fun ◡𝑓)) |
59 | 58 | simplbi 475 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓:𝑋–1-1→ℕ → 𝑓:𝑋⟶ℕ) |
60 | 59 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → 𝑓:𝑋⟶ℕ) |
61 | 60 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℕ) |
62 | 61 | nnzd 11357 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℤ) |
63 | 57, 62 | rpexpcld 12894 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈
ℝ+) |
64 | 63 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈
ℝ+) |
65 | 55, 64 | rpdivcld 11765 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈
ℝ+) |
66 | 54, 65 | sseldi 3566 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
67 | 66 | adantl3r 782 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
68 | | rexadd 11937 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀‘𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) = ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
69 | 53, 67, 68 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) = ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
70 | 9, 48 | sylan 487 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞)) |
71 | | dfrp2 28922 |
. . . . . . . . . . . . . . . . . . . 20
⊢
ℝ+ = (0(,)+∞) |
72 | | ioossicc 12130 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(0(,)+∞) ⊆ (0[,]+∞) |
73 | 71, 72 | eqsstri 3598 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℝ+ ⊆ (0[,]+∞) |
74 | 73, 65 | sseldi 3566 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
75 | 74 | adantl3r 782 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
76 | 70, 75 | xrge0addcld 28917 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
77 | 69, 76 | eqeltrrd 2689 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
78 | 54, 55 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℝ) |
79 | 78 | adantl3r 782 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℝ) |
80 | 54, 63 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℝ) |
81 | 80 | adantlr 747 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℝ) |
82 | 81 | adantl3r 782 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℝ) |
83 | | simplr 788 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℝ+) |
84 | 83 | rpgt0d 11751 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 0 < 𝑒) |
85 | | 2re 10967 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℝ |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 2 ∈ ℝ) |
87 | 62 | adantllr 751 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℤ) |
88 | 87 | adantlr 747 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℤ) |
89 | | 2pos 10989 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 <
2 |
90 | 89 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 0 < 2) |
91 | | expgt0 12755 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℝ ∧ (𝑓‘𝑦) ∈ ℤ ∧ 0 < 2) → 0
< (2↑(𝑓‘𝑦))) |
92 | 86, 88, 90, 91 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 0 < (2↑(𝑓‘𝑦))) |
93 | 79, 82, 84, 92 | divgt0d 10838 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 0 < (𝑒 / (2↑(𝑓‘𝑦)))) |
94 | 67, 53 | ltaddposd 10490 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (0 < (𝑒 / (2↑(𝑓‘𝑦))) ↔ (𝑀‘𝐴) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
95 | 93, 94 | mpbid 221 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
96 | 29 | fveq1i 6104 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀‘𝐴) = ((toOMeas‘𝑅)‘𝐴) |
97 | 26 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑄 ∈ 𝑉) |
98 | 27 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑅:𝑄⟶(0[,]+∞)) |
99 | | omsfval 29683 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
→ ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
100 | 97, 98, 34, 99 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
101 | 96, 100 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
102 | 9, 101 | sylan 487 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
103 | 102 | eqcomd 2616 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) = (𝑀‘𝐴)) |
104 | 103 | breq1d 4593 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ (𝑀‘𝐴) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
105 | 95, 104 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
106 | 77, 105 | jca 553 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞) ∧ inf(ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
107 | | iccssxr 12127 |
. . . . . . . . . . . . . . . . . . 19
⊢
(0[,]+∞) ⊆ ℝ* |
108 | | xrltso 11850 |
. . . . . . . . . . . . . . . . . . 19
⊢ < Or
ℝ* |
109 | | soss 4977 |
. . . . . . . . . . . . . . . . . . 19
⊢
((0[,]+∞) ⊆ ℝ* → ( < Or
ℝ* → < Or (0[,]+∞))) |
110 | 107, 108,
109 | mp2 9 |
. . . . . . . . . . . . . . . . . 18
⊢ < Or
(0[,]+∞) |
111 | | biid 250 |
. . . . . . . . . . . . . . . . . 18
⊢ ( < Or
(0[,]+∞) ↔ < Or (0[,]+∞)) |
112 | 110, 111 | mpbi 219 |
. . . . . . . . . . . . . . . . 17
⊢ < Or
(0[,]+∞) |
113 | 112 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → < Or
(0[,]+∞)) |
114 | | omscl 29684 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ∈ 𝒫 ∪ dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞)) |
115 | 97, 98, 47, 114 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞)) |
116 | | xrge0infss 28915 |
. . . . . . . . . . . . . . . . 17
⊢ (ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞) → ∃𝑣 ∈
(0[,]+∞)(∀ℎ
∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ¬ ℎ < 𝑣 ∧ ∀ℎ ∈ (0[,]+∞)(𝑣 < ℎ → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ℎ))) |
117 | 115, 116 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∃𝑣 ∈ (0[,]+∞)(∀ℎ ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ¬ ℎ < 𝑣 ∧ ∀ℎ ∈ (0[,]+∞)(𝑣 < ℎ → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ℎ))) |
118 | 113, 117 | infglb 8279 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ((((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞) ∧ inf(ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
119 | 118 | imp 444 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞) ∧ inf(ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
120 | 23, 24, 106, 119 | syl21anc 1317 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
121 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) |
122 | | esumex 29418 |
. . . . . . . . . . . . . . . . . . 19
⊢
Σ*𝑤
∈ 𝑥(𝑅‘𝑤) ∈ V |
123 | 121, 122 | elrnmpti 5297 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) |
124 | 123 | anbi1i 727 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
125 | | r19.41v 3070 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑥 ∈
{𝑧 ∈ 𝒫 dom
𝑅 ∣ (𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
(𝑢 =
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
126 | 124, 125 | bitr4i 266 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
127 | 126 | exbii 1764 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ ∃𝑢∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
128 | | df-rex 2902 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑢 ∈ ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
129 | | rexcom4 3198 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑥 ∈
{𝑧 ∈ 𝒫 dom
𝑅 ∣ (𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ ∃𝑢∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
130 | 127, 128,
129 | 3bitr4i 291 |
. . . . . . . . . . . . . 14
⊢
(∃𝑢 ∈ ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
131 | | breq1 4586 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) → (𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
132 | | idd 24 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) → (Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
133 | 131, 132 | sylbid 229 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) → (𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
134 | 133 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
135 | 134 | exlimiv 1845 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
136 | 135 | reximi 2994 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
{𝑧 ∈ 𝒫 dom
𝑅 ∣ (𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
137 | 130, 136 | sylbi 206 |
. . . . . . . . . . . . 13
⊢
(∃𝑢 ∈ ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
138 | 120, 137 | syl 17 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
139 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)
→ 𝑧 ≼
ω) |
140 | 139 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝒫 dom 𝑅 → ((𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω) → 𝑧 ≼ ω)) |
141 | 140 | ss2rabi 3647 |
. . . . . . . . . . . . . 14
⊢ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} |
142 | | rexss 3632 |
. . . . . . . . . . . . . 14
⊢ ({𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
143 | 141, 142 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
{𝑧 ∈ 𝒫 dom
𝑅 ∣ (𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
144 | | unieq 4380 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝑥 → ∪ 𝑧 = ∪
𝑥) |
145 | 144 | sseq2d 3596 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑥 → (𝐴 ⊆ ∪ 𝑧 ↔ 𝐴 ⊆ ∪ 𝑥)) |
146 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑥 → (𝑧 ≼ ω ↔ 𝑥 ≼ ω)) |
147 | 145, 146 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑥 → ((𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω) ↔ (𝐴 ⊆ ∪ 𝑥 ∧ 𝑥 ≼ ω))) |
148 | 147 | elrab 3331 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↔ (𝑥 ∈ 𝒫 dom 𝑅 ∧ (𝐴 ⊆ ∪ 𝑥 ∧ 𝑥 ≼ ω))) |
149 | 148 | simprbi 479 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} → (𝐴 ⊆ ∪ 𝑥 ∧ 𝑥 ≼ ω)) |
150 | 149 | simpld 474 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} → 𝐴 ⊆ ∪ 𝑥) |
151 | 150 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} → 𝐴 ⊆ ∪ 𝑥)) |
152 | 151 | anim1d 586 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ((𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
153 | 152 | reximdv 2999 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
154 | 143, 153 | syl5bi 231 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
155 | 138, 154 | mpd 15 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
156 | 155 | ex 449 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑦 ∈ 𝑋 → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
157 | 22, 156 | ralrimi 2940 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
∀𝑦 ∈ 𝑋 ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
158 | | unieq 4380 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑔‘𝑦) → ∪ 𝑥 = ∪
(𝑔‘𝑦)) |
159 | 158 | sseq2d 3596 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑔‘𝑦) → (𝐴 ⊆ ∪ 𝑥 ↔ 𝐴 ⊆ ∪ (𝑔‘𝑦))) |
160 | | esumeq1 29423 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑔‘𝑦) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) = Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
161 | 160 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑔‘𝑦) → (Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
162 | 159, 161 | anbi12d 743 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑔‘𝑦) → ((𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
163 | 162 | ac6sg 9193 |
. . . . . . . . . 10
⊢ (𝑋 ∈ V → (∀𝑦 ∈ 𝑋 ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))))) |
164 | 163 | imp 444 |
. . . . . . . . 9
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
165 | 12, 157, 164 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
166 | 9 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝜑) |
167 | 39 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅) |
168 | | iunss 4497 |
. . . . . . . . . . . . . . . . . 18
⊢ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅 ↔ ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅) |
169 | 167, 168 | sylibr 223 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅) |
170 | 44 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑦 ∈ 𝑋 𝐴 ∈ V) |
171 | | iunexg 7035 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 𝐴 ∈ V) → ∪ 𝑦 ∈ 𝑋 𝐴 ∈ V) |
172 | 11, 170, 171 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ∈ V) |
173 | | elpwg 4116 |
. . . . . . . . . . . . . . . . . 18
⊢ (∪ 𝑦 ∈ 𝑋 𝐴 ∈ V → (∪ 𝑦 ∈ 𝑋 𝐴 ∈ 𝒫 ∪ dom 𝑅 ↔ ∪
𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅)) |
174 | 172, 173 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (∪ 𝑦 ∈ 𝑋 𝐴 ∈ 𝒫 ∪ dom 𝑅 ↔ ∪
𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅)) |
175 | 169, 174 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ∈ 𝒫 ∪ dom 𝑅) |
176 | 32, 175 | ffvelrnd 6268 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ∈ (0[,]+∞)) |
177 | 107, 176 | sseldi 3566 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ∈
ℝ*) |
178 | 166, 177 | syl 17 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ∈
ℝ*) |
179 | | simplr 788 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
180 | 25 | ad4antr 764 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑋 ∈ V) |
181 | | fex 6394 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ 𝑋 ∈ V) → 𝑔 ∈ V) |
182 | 179, 180,
181 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑔 ∈ V) |
183 | | rnexg 6990 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 ∈ V → ran 𝑔 ∈ V) |
184 | | uniexg 6853 |
. . . . . . . . . . . . . . . 16
⊢ (ran
𝑔 ∈ V → ∪ ran 𝑔 ∈ V) |
185 | 182, 183,
184 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪
ran 𝑔 ∈
V) |
186 | | simp-5l 804 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝜑) |
187 | 27 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑐 ∈ ∪ ran
𝑔) → 𝑅:𝑄⟶(0[,]+∞)) |
188 | | frn 5966 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
189 | | ssrab2 3650 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ⊆ 𝒫 dom 𝑅 |
190 | 188, 189 | syl6ss 3580 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ran 𝑔 ⊆ 𝒫 dom 𝑅) |
191 | 190 | unissd 4398 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∪ ran 𝑔 ⊆ ∪
𝒫 dom 𝑅) |
192 | | unipw 4845 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ∪ 𝒫 dom 𝑅 = dom 𝑅 |
193 | 191, 192 | syl6sseq 3614 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∪ ran 𝑔 ⊆ dom 𝑅) |
194 | 193 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∪ ran 𝑔 ⊆ dom 𝑅) |
195 | 36 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → dom 𝑅 = 𝑄) |
196 | 194, 195 | sseqtrd 3604 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∪ ran 𝑔 ⊆ 𝑄) |
197 | 196 | sselda 3568 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑐 ∈ ∪ ran
𝑔) → 𝑐 ∈ 𝑄) |
198 | 187, 197 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑐 ∈ ∪ ran
𝑔) → (𝑅‘𝑐) ∈ (0[,]+∞)) |
199 | 198 | ralrimiva 2949 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∀𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ (0[,]+∞)) |
200 | 186, 179,
199 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ∈ (0[,]+∞)) |
201 | | nfcv 2751 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑐∪ ran 𝑔 |
202 | 201 | esumcl 29419 |
. . . . . . . . . . . . . . 15
⊢ ((∪ ran 𝑔 ∈ V ∧ ∀𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ∈ (0[,]+∞)) →
Σ*𝑐 ∈
∪ ran 𝑔(𝑅‘𝑐) ∈ (0[,]+∞)) |
203 | 185, 200,
202 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ (0[,]+∞)) |
204 | 107, 203 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈
ℝ*) |
205 | | simp-5r 805 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) |
206 | 205 | rexrd 9968 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈
ℝ*) |
207 | | simpllr 795 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑒 ∈ ℝ+) |
208 | 207 | rpxrd 11749 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑒 ∈ ℝ*) |
209 | 206, 208 | xaddcld 12003 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒) ∈
ℝ*) |
210 | 188 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
211 | | sstr 3576 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ⊆ 𝒫 dom 𝑅) → ran 𝑔 ⊆ 𝒫 dom 𝑅) |
212 | 189, 211 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ran 𝑔 ⊆ 𝒫 dom 𝑅) |
213 | | sspwuni 4547 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ran
𝑔 ⊆ 𝒫 dom
𝑅 ↔ ∪ ran 𝑔 ⊆ dom 𝑅) |
214 | 212, 213 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∪ ran 𝑔 ⊆ dom 𝑅) |
215 | 210, 214 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪
ran 𝑔 ⊆ dom 𝑅) |
216 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → 𝑔 Fn 𝑋) |
217 | 216 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑔 Fn 𝑋) |
218 | 166, 1 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑋 ≼ ω) |
219 | | fnct 28876 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑔 Fn 𝑋 ∧ 𝑋 ≼ ω) → 𝑔 ≼ ω) |
220 | | rnct 28879 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑔 ≼ ω → ran
𝑔 ≼
ω) |
221 | 219, 220 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑔 Fn 𝑋 ∧ 𝑋 ≼ ω) → ran 𝑔 ≼
ω) |
222 | | dfss3 3558 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ↔ ∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
223 | 222 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
224 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 = 𝑤 → (𝑧 ≼ ω ↔ 𝑤 ≼ ω)) |
225 | 224 | elrab 3331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ↔ (𝑤 ∈ 𝒫 dom 𝑅 ∧ 𝑤 ≼ ω)) |
226 | 225 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → 𝑤 ≼ ω) |
227 | 226 | ralimi 2936 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∀𝑤 ∈
ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω) |
228 | 223, 227 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω) |
229 | | unictb 9276 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ran
𝑔 ≼ ω ∧
∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω) → ∪ ran 𝑔 ≼ ω) |
230 | 221, 228,
229 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑔 Fn 𝑋 ∧ 𝑋 ≼ ω) ∧ ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∪ ran 𝑔 ≼ ω) |
231 | 217, 218,
210, 230 | syl21anc 1317 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪
ran 𝑔 ≼
ω) |
232 | | ctex 7856 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (∪ ran 𝑔 ≼ ω → ∪ ran 𝑔 ∈ V) |
233 | | elpwg 4116 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (∪ ran 𝑔 ∈ V → (∪ ran 𝑔 ∈ 𝒫 dom 𝑅 ↔ ∪ ran
𝑔 ⊆ dom 𝑅)) |
234 | 231, 232,
233 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (∪
ran 𝑔 ∈ 𝒫 dom
𝑅 ↔ ∪ ran 𝑔 ⊆ dom 𝑅)) |
235 | 215, 234 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪
ran 𝑔 ∈ 𝒫 dom
𝑅) |
236 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → 𝐴 ⊆ ∪ (𝑔‘𝑦)) |
237 | 236 | ralimi 2936 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑦 ∈
𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ (𝑔‘𝑦)) |
238 | | fvssunirn 6127 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑔‘𝑦) ⊆ ∪ ran
𝑔 |
239 | 238 | unissi 4397 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ∪ (𝑔‘𝑦) ⊆ ∪ ∪ ran 𝑔 |
240 | | sstr 3576 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ ∪ (𝑔‘𝑦) ⊆ ∪ ∪ ran 𝑔) → 𝐴 ⊆ ∪ ∪ ran 𝑔) |
241 | 239, 240 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ⊆ ∪ (𝑔‘𝑦) → 𝐴 ⊆ ∪ ∪ ran 𝑔) |
242 | 241 | ralimi 2936 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∀𝑦 ∈
𝑋 𝐴 ⊆ ∪ (𝑔‘𝑦) → ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔) |
243 | | iunss 4497 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔 ↔ ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔) |
244 | 242, 243 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑦 ∈
𝑋 𝐴 ⊆ ∪ (𝑔‘𝑦) → ∪
𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔) |
245 | 237, 244 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑦 ∈
𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔) |
246 | 245 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔) |
247 | 235, 246,
231 | jca32 556 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (∪
ran 𝑔 ∈ 𝒫 dom
𝑅 ∧ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔 ∧ ∪ ran 𝑔 ≼
ω))) |
248 | | unieq 4380 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = ∪
ran 𝑔 → ∪ 𝑧 =
∪ ∪ ran 𝑔) |
249 | 248 | sseq2d 3596 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = ∪
ran 𝑔 → (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ↔ ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔)) |
250 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = ∪
ran 𝑔 → (𝑧 ≼ ω ↔ ∪ ran 𝑔 ≼ ω)) |
251 | 249, 250 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = ∪
ran 𝑔 → ((∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω) ↔ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔 ∧ ∪ ran 𝑔 ≼
ω))) |
252 | 251 | elrab 3331 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∪ ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↔ (∪ ran 𝑔 ∈ 𝒫 dom 𝑅 ∧ (∪
𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔 ∧ ∪ ran 𝑔 ≼
ω))) |
253 | 247, 252 | sylibr 223 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪
ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}) |
254 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 = 𝑤 → (𝑅‘𝑐) = (𝑅‘𝑤)) |
255 | 254 | cbvesumv 29432 |
. . . . . . . . . . . . . . . . . 18
⊢
Σ*𝑐
∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ ∪ ran
𝑔(𝑅‘𝑤) |
256 | | esumeq1 29423 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = ∪
ran 𝑔 →
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) = Σ*𝑤 ∈ ∪ ran
𝑔(𝑅‘𝑤)) |
257 | 256 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = ∪
ran 𝑔 →
(Σ*𝑐
∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ↔ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ ∪ ran
𝑔(𝑅‘𝑤))) |
258 | 257 | rspcev 3282 |
. . . . . . . . . . . . . . . . . 18
⊢ ((∪ ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧
Σ*𝑐 ∈
∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ ∪ ran
𝑔(𝑅‘𝑤)) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) |
259 | 253, 255,
258 | sylancl 693 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) |
260 | | esumex 29418 |
. . . . . . . . . . . . . . . . . 18
⊢
Σ*𝑐
∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ V |
261 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) |
262 | 261 | elrnmpt 5293 |
. . . . . . . . . . . . . . . . . 18
⊢
(Σ*𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ∈ V → (Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤))) |
263 | 260, 262 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(Σ*𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) |
264 | 259, 263 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))) |
265 | 112 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → < Or
(0[,]+∞)) |
266 | | omscl 29684 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ ∪ 𝑦 ∈ 𝑋 𝐴 ∈ 𝒫 ∪ dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞)) |
267 | 26, 27, 175, 266 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞)) |
268 | | xrge0infss 28915 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞) → ∃𝑒 ∈
(0[,]+∞)(∀𝑡
∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ¬ 𝑡 < 𝑒 ∧ ∀𝑡 ∈ (0[,]+∞)(𝑒 < 𝑡 → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < 𝑡))) |
269 | 267, 268 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∃𝑒 ∈ (0[,]+∞)(∀𝑡 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ¬ 𝑡 < 𝑒 ∧ ∀𝑡 ∈ (0[,]+∞)(𝑒 < 𝑡 → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < 𝑡))) |
270 | 265, 269 | inflb 8278 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) → ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ))) |
271 | 29 | fveq1i 6104 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) = ((toOMeas‘𝑅)‘∪
𝑦 ∈ 𝑋 𝐴) |
272 | 169, 37 | sseqtrd 3604 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑄) |
273 | | omsfval 29683 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑄) → ((toOMeas‘𝑅)‘∪ 𝑦 ∈ 𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
274 | 26, 27, 272, 273 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((toOMeas‘𝑅)‘∪ 𝑦 ∈ 𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
275 | 271, 274 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
276 | 275 | breq2d 4595 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ↔ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ))) |
277 | 276 | notbid 307 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (¬
Σ*𝑐 ∈
∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ↔ ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ))) |
278 | 270, 277 | sylibrd 248 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) → ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴))) |
279 | 166, 264,
278 | sylc 63 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴)) |
280 | | biid 250 |
. . . . . . . . . . . . . . 15
⊢ (¬
Σ*𝑐 ∈
∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ↔ ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴)) |
281 | 279, 280 | sylib 207 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴)) |
282 | | xrlenlt 9982 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ∈ ℝ* ∧
Σ*𝑐 ∈
∪ ran 𝑔(𝑅‘𝑐) ∈ ℝ*) → ((𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ↔ ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴))) |
283 | 178, 204,
282 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ((𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ↔ ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴))) |
284 | 281, 283 | mpbird 246 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐)) |
285 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑦 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} |
286 | 22, 285 | nfan 1816 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑦((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
287 | | nfra1 2925 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑦∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
288 | 286, 287 | nfan 1816 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑦(((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
289 | | simp-6l 806 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → 𝜑) |
290 | | simpllr 795 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
291 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
292 | 27 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑅:𝑄⟶(0[,]+∞)) |
293 | | simpllr 795 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
294 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑦 ∈ 𝑋) |
295 | 293, 294 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
296 | 189, 295 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ∈ 𝒫 dom 𝑅) |
297 | 296 | elpwid 4118 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ⊆ dom 𝑅) |
298 | 292, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → dom 𝑅 = 𝑄) |
299 | 297, 298 | sseqtrd 3604 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ⊆ 𝑄) |
300 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑤 ∈ (𝑔‘𝑦)) |
301 | 299, 300 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑤 ∈ 𝑄) |
302 | 292, 301 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑅‘𝑤) ∈ (0[,]+∞)) |
303 | 302 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → ∀𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
304 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔‘𝑦) ∈ V |
305 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑤(𝑔‘𝑦) |
306 | 305 | esumcl 29419 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑔‘𝑦) ∈ V ∧ ∀𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) →
Σ*𝑤 ∈
(𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
307 | 304, 306 | mpan 702 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑤 ∈
(𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞) →
Σ*𝑤 ∈
(𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
308 | 303, 307 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
309 | 289, 290,
291, 308 | syl21anc 1317 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
310 | 309 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑦 ∈ 𝑋 → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞))) |
311 | 288, 310 | ralrimi 2940 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
312 | 14 | esumcl 29419 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) →
Σ*𝑦 ∈
𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
313 | 180, 311,
312 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
314 | 107, 313 | sseldi 3566 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈
ℝ*) |
315 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑤(𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
316 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
317 | | fniunfv 6409 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 Fn 𝑋 → ∪
𝑦 ∈ 𝑋 (𝑔‘𝑦) = ∪ ran 𝑔) |
318 | 316, 216,
317 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∪ 𝑦 ∈ 𝑋 (𝑔‘𝑦) = ∪ ran 𝑔) |
319 | 315, 318 | esumeq1d 29424 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) →
Σ*𝑤 ∈
∪ 𝑦 ∈ 𝑋 (𝑔‘𝑦)(𝑅‘𝑤) = Σ*𝑤 ∈ ∪ ran
𝑔(𝑅‘𝑤)) |
320 | 11 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → 𝑋 ∈ V) |
321 | 304 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑔‘𝑦) ∈ V) |
322 | 320, 321,
302 | esumiun 29483 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) →
Σ*𝑤 ∈
∪ 𝑦 ∈ 𝑋 (𝑔‘𝑦)(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
323 | 319, 322 | eqbrtrrd 4607 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) →
Σ*𝑤 ∈
∪ ran 𝑔(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
324 | 9, 323 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) →
Σ*𝑤 ∈
∪ ran 𝑔(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
325 | 324 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑤 ∈ ∪ ran 𝑔(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
326 | 255, 325 | syl5eqbr 4618 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
327 | 289, 291,
48 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞)) |
328 | | simplll 794 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈
ℝ+)) |
329 | 328, 291,
75 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
330 | 327, 329 | xrge0addcld 28917 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
331 | 330 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑦 ∈ 𝑋 → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞))) |
332 | 288, 331 | ralrimi 2940 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
333 | 14 | esumcl 29419 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) →
Σ*𝑦 ∈
𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
334 | 180, 332,
333 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
335 | 107, 334 | sseldi 3566 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈
ℝ*) |
336 | 218, 10 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑋 ∈ V) |
337 | | simp-4l 802 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ)) |
338 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
339 | 337, 338,
51 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ ℝ) |
340 | 339 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → (𝑀‘𝐴) ∈ ℝ) |
341 | 67 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
342 | 341 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
343 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
344 | 343 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
345 | 68 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑀‘𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) →
(Σ*𝑤
∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ↔ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
346 | 345 | biimpar 501 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑀‘𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) ∧
Σ*𝑤 ∈
(𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) |
347 | 340, 342,
344, 346 | syl21anc 1317 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) |
348 | 347 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
349 | 337 | simpld 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → 𝜑) |
350 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
351 | 349, 350,
338, 308 | syl21anc 1317 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
352 | 107, 351 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈
ℝ*) |
353 | 339 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈
ℝ*) |
354 | 341 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈
ℝ*) |
355 | 353, 354 | xaddcld 12003 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈
ℝ*) |
356 | | xrltle 11858 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ ℝ* ∧ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ ℝ*) →
(Σ*𝑤
∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
357 | 352, 355,
356 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
358 | 348, 357 | syld 46 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
359 | 358 | adantld 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
360 | 359 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → (𝑦 ∈ 𝑋 → ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))))) |
361 | 286, 360 | ralrimi 2940 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∀𝑦 ∈ 𝑋 ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
362 | | ralim 2932 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑦 ∈
𝑋 ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) → (∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
363 | 361, 362 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → (∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
364 | 363 | imp 444 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) |
365 | 364 | r19.21bi 2916 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) |
366 | 288, 14, 336, 309, 330, 365 | esumlef 29451 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) |
367 | 166, 48 | sylan 487 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞)) |
368 | 288, 14, 336, 367, 329 | esumaddf 29450 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) = (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦))))) |
369 | 329 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑦 ∈ 𝑋 → (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞))) |
370 | 288, 369 | ralrimi 2940 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
371 | 14 | esumcl 29419 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) →
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
372 | 180, 370,
371 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
373 | 107, 372 | sseldi 3566 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈
ℝ*) |
374 | | simp-4r 803 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑓:𝑋–1-1→ℕ) |
375 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑓 ∈ V |
376 | 375 | rnex 6992 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ran 𝑓 ∈ V |
377 | 376 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ran 𝑓 ∈ V) |
378 | | frn 5966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓:𝑋⟶ℕ → ran 𝑓 ⊆
ℕ) |
379 | 60, 378 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → ran 𝑓 ⊆ ℕ) |
380 | 379 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ran 𝑓 ⊆
ℕ) |
381 | 380 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ ℕ) |
382 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 2 ∈
ℝ+) |
383 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 𝑧 ∈ ℕ) |
384 | 383 | nnzd 11357 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 𝑧 ∈ ℤ) |
385 | 382, 384 | rpexpcld 12894 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (2↑𝑧) ∈
ℝ+) |
386 | 385 | rpreccld 11758 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈
ℝ+) |
387 | 73, 386 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈
(0[,]+∞)) |
388 | 387 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ℕ) → (1 /
(2↑𝑧)) ∈
(0[,]+∞)) |
389 | 381, 388 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ran 𝑓) → (1 / (2↑𝑧)) ∈ (0[,]+∞)) |
390 | 389 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
∀𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞)) |
391 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑧ran
𝑓 |
392 | 391 | esumcl 29419 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ran
𝑓 ∈ V ∧
∀𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞)) →
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)) ∈
(0[,]+∞)) |
393 | 377, 390,
392 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)) ∈
(0[,]+∞)) |
394 | 107, 393 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)) ∈
ℝ*) |
395 | | 1re 9918 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
ℝ |
396 | | rexr 9964 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1 ∈
ℝ → 1 ∈ ℝ*) |
397 | 395, 396 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℝ* |
398 | 397 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 1 ∈
ℝ*) |
399 | 73 | sseli 3564 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑒 ∈ ℝ+
→ 𝑒 ∈
(0[,]+∞)) |
400 | 399 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈
(0[,]+∞)) |
401 | | elxrge0 12152 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑒 ∈ (0[,]+∞) ↔
(𝑒 ∈
ℝ* ∧ 0 ≤ 𝑒)) |
402 | 400, 401 | sylib 207 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ∈ ℝ*
∧ 0 ≤ 𝑒)) |
403 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑧(𝜑 ∧ 𝑓:𝑋–1-1→ℕ) |
404 | | nnex 10903 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ℕ
∈ V |
405 | 404 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → ℕ ∈
V) |
406 | 403, 405,
387, 379 | esummono 29443 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ Σ*𝑧 ∈ ℕ(1 / (2↑𝑧))) |
407 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = 𝑤 → (2↑𝑧) = (2↑𝑤)) |
408 | 407 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = 𝑤 → (1 / (2↑𝑧)) = (1 / (2↑𝑤))) |
409 | | ioossico 12133 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(0(,)+∞) ⊆ (0[,)+∞) |
410 | 71, 409 | eqsstri 3598 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
ℝ+ ⊆ (0[,)+∞) |
411 | 410, 386 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈
(0[,)+∞)) |
412 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ ℕ → (𝑤 ∈ ℕ ↦ (1 /
(2↑𝑤))) = (𝑤 ∈ ℕ ↦ (1 /
(2↑𝑤)))) |
413 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → 𝑤 = 𝑧) |
414 | 413 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → (2↑𝑤) = (2↑𝑧)) |
415 | 414 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → (1 / (2↑𝑤)) = (1 / (2↑𝑧))) |
416 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℕ) |
417 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (1 /
(2↑𝑧)) ∈
V |
418 | 417 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ ℕ → (1 /
(2↑𝑧)) ∈
V) |
419 | 412, 415,
416, 418 | fvmptd 6197 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 ∈ ℕ → ((𝑤 ∈ ℕ ↦ (1 /
(2↑𝑤)))‘𝑧) = (1 / (2↑𝑧))) |
420 | 419 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → ((𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))‘𝑧) = (1 / (2↑𝑧))) |
421 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 1 ∈
ℂ |
422 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ ℕ ↦ (1 /
(2↑𝑤))) = (𝑤 ∈ ℕ ↦ (1 /
(2↑𝑤))) |
423 | 422 | geo2lim 14445 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (1 ∈
ℂ → seq1( + , (𝑤
∈ ℕ ↦ (1 / (2↑𝑤)))) ⇝ 1) |
424 | 421, 423 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ seq1( + ,
(𝑤 ∈ ℕ ↦
(1 / (2↑𝑤)))) ⇝
1 |
425 | 424 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → seq1( + , (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))) ⇝ 1) |
426 | 395 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → 1 ∈
ℝ) |
427 | 408, 411,
420, 425, 426 | esumcvgsum 29477 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ℕ(1 /
(2↑𝑧)) = Σ𝑧 ∈ ℕ (1 /
(2↑𝑧))) |
428 | | geoihalfsum 14453 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Σ𝑧 ∈
ℕ (1 / (2↑𝑧)) =
1 |
429 | 427, 428 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ℕ(1 /
(2↑𝑧)) =
1) |
430 | 406, 429 | breqtrd 4609 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1) |
431 | 430 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)) ≤ 1) |
432 | | xlemul2a 11991 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ ℝ* ∧ 1 ∈
ℝ* ∧ (𝑒 ∈ ℝ* ∧ 0 ≤
𝑒)) ∧
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)) ≤ 1) → (𝑒 ·e
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧))) ≤ (𝑒 ·e 1)) |
433 | 394, 398,
402, 431, 432 | syl31anc 1321 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧))) ≤ (𝑒 ·e 1)) |
434 | 13, 19 | nfan 1816 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑦(𝜑 ∧ 𝑓:𝑋–1-1→ℕ) |
435 | 434, 21 | nfan 1816 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑦((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) |
436 | 78 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℂ) |
437 | 80 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℂ) |
438 | 437 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℂ) |
439 | | 2cn 10968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 2 ∈
ℂ |
440 | 439 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → 2 ∈ ℂ) |
441 | | 2ne0 10990 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 2 ≠
0 |
442 | 441 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → 2 ≠ 0) |
443 | 440, 442,
62 | expne0d 12876 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ≠ 0) |
444 | 443 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ≠ 0) |
445 | 436, 438,
444 | divrecd 10683 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) = (𝑒 · (1 / (2↑(𝑓‘𝑦))))) |
446 | | 1rp 11712 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 1 ∈
ℝ+ |
447 | 446 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → 1 ∈
ℝ+) |
448 | 447, 63 | rpdivcld 11765 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈
ℝ+) |
449 | 54, 448 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
450 | 449 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
451 | | rexmul 11973 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑒 ∈ ℝ ∧ (1 /
(2↑(𝑓‘𝑦))) ∈ ℝ) →
(𝑒 ·e (1
/ (2↑(𝑓‘𝑦)))) = (𝑒 · (1 / (2↑(𝑓‘𝑦))))) |
452 | 78, 450, 451 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 ·e (1 / (2↑(𝑓‘𝑦)))) = (𝑒 · (1 / (2↑(𝑓‘𝑦))))) |
453 | 445, 452 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) = (𝑒 ·e (1 / (2↑(𝑓‘𝑦))))) |
454 | 453 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
∀𝑦 ∈ 𝑋 (𝑒 / (2↑(𝑓‘𝑦))) = (𝑒 ·e (1 / (2↑(𝑓‘𝑦))))) |
455 | 435, 454 | esumeq2d 29426 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦))) = Σ*𝑦 ∈ 𝑋(𝑒 ·e (1 / (2↑(𝑓‘𝑦))))) |
456 | 11 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑋 ∈ V) |
457 | 73, 448 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
458 | 457 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
459 | 410 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → ℝ+ ⊆
(0[,)+∞)) |
460 | 459 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈
(0[,)+∞)) |
461 | 456, 458,
460 | esummulc2 29471 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e
Σ*𝑦 ∈
𝑋(1 / (2↑(𝑓‘𝑦)))) = Σ*𝑦 ∈ 𝑋(𝑒 ·e (1 / (2↑(𝑓‘𝑦))))) |
462 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑦(1 /
(2↑𝑧)) |
463 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = (𝑓‘𝑦) → (2↑𝑧) = (2↑(𝑓‘𝑦))) |
464 | 463 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = (𝑓‘𝑦) → (1 / (2↑𝑧)) = (1 / (2↑(𝑓‘𝑦)))) |
465 | 11 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → 𝑋 ∈ V) |
466 | 58 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓:𝑋–1-1→ℕ → Fun ◡𝑓) |
467 | 59 | feqmptd 6159 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓:𝑋–1-1→ℕ → 𝑓 = (𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦))) |
468 | 467 | cnveqd 5220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓:𝑋–1-1→ℕ → ◡𝑓 = ◡(𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦))) |
469 | 468 | funeqd 5825 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓:𝑋–1-1→ℕ → (Fun ◡𝑓 ↔ Fun ◡(𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦)))) |
470 | 466, 469 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓:𝑋–1-1→ℕ → Fun ◡(𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦))) |
471 | 470 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Fun ◡(𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦))) |
472 | 462, 434,
14, 464, 465, 471, 457, 61 | esumc 29440 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑦 ∈ 𝑋(1 / (2↑(𝑓‘𝑦))) = Σ*𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)} (1 / (2↑𝑧))) |
473 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓:𝑋⟶ℕ → 𝑓 Fn 𝑋) |
474 | | fnrnfv 6152 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 Fn 𝑋 → ran 𝑓 = {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)}) |
475 | 60, 473, 474 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → ran 𝑓 = {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)}) |
476 | 403, 475 | esumeq1d 29424 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) = Σ*𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)} (1 / (2↑𝑧))) |
477 | 472, 476 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑦 ∈ 𝑋(1 / (2↑(𝑓‘𝑦))) = Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) |
478 | 477 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑦 ∈
𝑋(1 / (2↑(𝑓‘𝑦))) = Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) |
479 | 478 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e
Σ*𝑦 ∈
𝑋(1 / (2↑(𝑓‘𝑦)))) = (𝑒 ·e
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)))) |
480 | 455, 461,
479 | 3eqtr2rd 2651 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧))) = Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦)))) |
481 | 402 | simpld 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈
ℝ*) |
482 | | xmulid1 11981 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑒 ∈ ℝ*
→ (𝑒
·e 1) = 𝑒) |
483 | 481, 482 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e 1) = 𝑒) |
484 | 433, 480,
483 | 3brtr3d 4614 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦))) ≤ 𝑒) |
485 | 166, 374,
207, 484 | syl21anc 1317 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ≤ 𝑒) |
486 | | xleadd2a 11956 |
. . . . . . . . . . . . . . . . 17
⊢
(((Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ* ∧ 𝑒 ∈ ℝ*
∧ Σ*𝑦
∈ 𝑋(𝑀‘𝐴) ∈ ℝ*) ∧
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦))) ≤ 𝑒) → (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦)))) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
487 | 373, 208,
206, 485, 486 | syl31anc 1321 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦)))) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
488 | 368, 487 | eqbrtrd 4605 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
489 | 314, 335,
209, 366, 488 | xrletrd 11869 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
490 | 204, 314,
209, 326, 489 | xrletrd 11869 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
491 | 178, 204,
209, 284, 490 | xrletrd 11869 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
492 | 207 | rpred 11748 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑒 ∈ ℝ) |
493 | | rexadd 11937 |
. . . . . . . . . . . . 13
⊢
((Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ ∧ 𝑒 ∈ ℝ) →
(Σ*𝑦
∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒) = (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
494 | 205, 492,
493 | syl2anc 691 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒) = (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
495 | 491, 494 | breqtrd 4609 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
496 | 495 | anasss 677 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
497 | 496 | ex 449 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ((𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))) |
498 | 497 | exlimdv 1848 |
. . . . . . . 8
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
(∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))) |
499 | 165, 498 | mpd 15 |
. . . . . . 7
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
500 | 499 | ralrimiva 2949 |
. . . . . 6
⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) → ∀𝑒 ∈ ℝ+ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
501 | | xralrple 11910 |
. . . . . . . 8
⊢ (((𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ∈ ℝ* ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) → ((𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))) |
502 | 177, 501 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → ((𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))) |
503 | 502 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) → ((𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))) |
504 | 500, 503 | mpbird 246 |
. . . . 5
⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴)) |
505 | 504 | ex 449 |
. . . 4
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑓:𝑋–1-1→ℕ → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴))) |
506 | 505 | exlimdv 1848 |
. . 3
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → (∃𝑓 𝑓:𝑋–1-1→ℕ → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴))) |
507 | 8, 506 | mpd 15 |
. 2
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴)) |
508 | 177 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ¬
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ∈
ℝ*) |
509 | | pnfge 11840 |
. . . 4
⊢ ((𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ∈ ℝ* → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ +∞) |
510 | 508, 509 | syl 17 |
. . 3
⊢ ((𝜑 ∧ ¬
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ +∞) |
511 | 48 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ 𝑋 (𝑀‘𝐴) ∈ (0[,]+∞)) |
512 | 14 | esumcl 29419 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 (𝑀‘𝐴) ∈ (0[,]+∞)) →
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ (0[,]+∞)) |
513 | 11, 511, 512 | syl2anc 691 |
. . . 4
⊢ (𝜑 → Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ (0[,]+∞)) |
514 | | xrge0nre 12148 |
. . . 4
⊢
((Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ (0[,]+∞) ∧ ¬
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) →
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) = +∞) |
515 | 513, 514 | sylan 487 |
. . 3
⊢ ((𝜑 ∧ ¬
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) →
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) = +∞) |
516 | 510, 515 | breqtrrd 4611 |
. 2
⊢ ((𝜑 ∧ ¬
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴)) |
517 | 507, 516 | pm2.61dan 828 |
1
⊢ (𝜑 → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴)) |