Step | Hyp | Ref
| Expression |
1 | | omssubadd.b |
. . . . . 6
⊢ (𝜑 → 𝑋 ≼ ω) |
2 | | nnenom 13342 |
. . . . . . 7
⊢ ℕ
≈ ω |
3 | 2 | ensymi 8553 |
. . . . . 6
⊢ ω
≈ ℕ |
4 | | domentr 8562 |
. . . . . 6
⊢ ((𝑋 ≼ ω ∧ ω
≈ ℕ) → 𝑋
≼ ℕ) |
5 | 1, 3, 4 | sylancl 588 |
. . . . 5
⊢ (𝜑 → 𝑋 ≼ ℕ) |
6 | | brdomi 8514 |
. . . . 5
⊢ (𝑋 ≼ ℕ →
∃𝑓 𝑓:𝑋–1-1→ℕ) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝜑 → ∃𝑓 𝑓:𝑋–1-1→ℕ) |
8 | 7 | adantr 483 |
. . 3
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → ∃𝑓 𝑓:𝑋–1-1→ℕ) |
9 | | simplll 773 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝜑) |
10 | | ctex 8518 |
. . . . . . . . . . 11
⊢ (𝑋 ≼ ω → 𝑋 ∈ V) |
11 | 1, 10 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ V) |
12 | 9, 11 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑋 ∈ V) |
13 | | nfv 1911 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦𝜑 |
14 | | nfcv 2977 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦𝑋 |
15 | 14 | nfesum1 31294 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) |
16 | | nfcv 2977 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦ℝ |
17 | 15, 16 | nfel 2992 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ |
18 | 13, 17 | nfan 1896 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) |
19 | | nfv 1911 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦 𝑓:𝑋–1-1→ℕ |
20 | 18, 19 | nfan 1896 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) |
21 | | nfv 1911 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 𝑒 ∈
ℝ+ |
22 | 20, 21 | nfan 1896 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) |
23 | 9 | adantr 483 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝜑) |
24 | | simpr 487 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
25 | 11 | adantr 483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → 𝑋 ∈ V) |
26 | | oms.o |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑄 ∈ 𝑉) |
27 | | oms.r |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑅:𝑄⟶(0[,]+∞)) |
28 | | omsf 31549 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞)) →
(toOMeas‘𝑅):𝒫
∪ dom 𝑅⟶(0[,]+∞)) |
29 | | oms.m |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑀 = (toOMeas‘𝑅) |
30 | 29 | feq1i 6500 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑀:𝒫 ∪ dom 𝑅⟶(0[,]+∞) ↔
(toOMeas‘𝑅):𝒫
∪ dom 𝑅⟶(0[,]+∞)) |
31 | 28, 30 | sylibr 236 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞)) → 𝑀:𝒫 ∪ dom 𝑅⟶(0[,]+∞)) |
32 | 26, 27, 31 | syl2anc 586 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑀:𝒫 ∪ dom
𝑅⟶(0[,]+∞)) |
33 | 32 | adantr 483 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑀:𝒫 ∪ dom
𝑅⟶(0[,]+∞)) |
34 | | omssubadd.a |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ⊆ ∪ 𝑄) |
35 | 27 | fdmd 6518 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → dom 𝑅 = 𝑄) |
36 | 35 | unieqd 4842 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ∪ dom 𝑅 = ∪ 𝑄) |
37 | 36 | adantr 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∪ dom
𝑅 = ∪ 𝑄) |
38 | 34, 37 | sseqtrrd 4008 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ⊆ ∪ dom
𝑅) |
39 | 26 | uniexd 7462 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ∪ 𝑄
∈ V) |
40 | 39 | adantr 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∪ 𝑄 ∈ V) |
41 | | ssexg 5220 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ⊆ ∪ 𝑄
∧ ∪ 𝑄 ∈ V) → 𝐴 ∈ V) |
42 | 34, 40, 41 | syl2anc 586 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ∈ V) |
43 | | elpwg 4545 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 ∪ dom 𝑅 ↔ 𝐴 ⊆ ∪ dom
𝑅)) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐴 ∈ 𝒫 ∪ dom 𝑅 ↔ 𝐴 ⊆ ∪ dom
𝑅)) |
45 | 38, 44 | mpbird 259 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ∈ 𝒫 ∪ dom 𝑅) |
46 | 33, 45 | ffvelrnd 6847 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞)) |
47 | 46 | adantlr 713 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞)) |
48 | | simpr 487 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) →
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) |
49 | 18, 25, 47, 48 | esumcvgre 31345 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ ℝ) |
50 | 49 | adantlr 713 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ ℝ) |
51 | 50 | adantlr 713 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ ℝ) |
52 | | rpssre 12390 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℝ+ ⊆ ℝ |
53 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℝ+) |
54 | | 2rp 12388 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℝ+ |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → 2 ∈
ℝ+) |
56 | | df-f1 6355 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓:𝑋–1-1→ℕ ↔ (𝑓:𝑋⟶ℕ ∧ Fun ◡𝑓)) |
57 | 56 | simplbi 500 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓:𝑋–1-1→ℕ → 𝑓:𝑋⟶ℕ) |
58 | 57 | adantl 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → 𝑓:𝑋⟶ℕ) |
59 | 58 | ffvelrnda 6846 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℕ) |
60 | 59 | nnzd 12080 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℤ) |
61 | 55, 60 | rpexpcld 13602 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈
ℝ+) |
62 | 61 | adantlr 713 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈
ℝ+) |
63 | 53, 62 | rpdivcld 12442 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈
ℝ+) |
64 | 52, 63 | sseldi 3965 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
65 | 64 | adantl3r 748 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
66 | | rexadd 12619 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀‘𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) = ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
67 | 51, 65, 66 | syl2anc 586 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) = ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
68 | 9, 46 | sylan 582 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞)) |
69 | | dfrp2 30485 |
. . . . . . . . . . . . . . . . . . . 20
⊢
ℝ+ = (0(,)+∞) |
70 | | ioossicc 12816 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(0(,)+∞) ⊆ (0[,]+∞) |
71 | 69, 70 | eqsstri 4001 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℝ+ ⊆ (0[,]+∞) |
72 | 71, 63 | sseldi 3965 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
73 | 72 | adantl3r 748 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
74 | 68, 73 | xrge0addcld 30480 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
75 | 67, 74 | eqeltrrd 2914 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
76 | 52, 53 | sseldi 3965 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℝ) |
77 | 76 | adantl3r 748 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℝ) |
78 | 52, 61 | sseldi 3965 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℝ) |
79 | 78 | adantlr 713 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℝ) |
80 | 79 | adantl3r 748 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℝ) |
81 | | simplr 767 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℝ+) |
82 | 81 | rpgt0d 12428 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 0 < 𝑒) |
83 | | 2re 11705 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℝ |
84 | 83 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 2 ∈ ℝ) |
85 | 60 | adantllr 717 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℤ) |
86 | 85 | adantlr 713 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℤ) |
87 | | 2pos 11734 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 <
2 |
88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 0 < 2) |
89 | | expgt0 13456 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℝ ∧ (𝑓‘𝑦) ∈ ℤ ∧ 0 < 2) → 0
< (2↑(𝑓‘𝑦))) |
90 | 84, 86, 88, 89 | syl3anc 1367 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 0 < (2↑(𝑓‘𝑦))) |
91 | 77, 80, 82, 90 | divgt0d 11569 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 0 < (𝑒 / (2↑(𝑓‘𝑦)))) |
92 | 65, 51 | ltaddposd 11218 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (0 < (𝑒 / (2↑(𝑓‘𝑦))) ↔ (𝑀‘𝐴) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
93 | 91, 92 | mpbid 234 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
94 | 29 | fveq1i 6666 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀‘𝐴) = ((toOMeas‘𝑅)‘𝐴) |
95 | 26 | adantr 483 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑄 ∈ 𝑉) |
96 | 27 | adantr 483 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑅:𝑄⟶(0[,]+∞)) |
97 | | omsfval 31547 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
→ ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
98 | 95, 96, 34, 97 | syl3anc 1367 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
99 | 94, 98 | syl5eq 2868 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
100 | 9, 99 | sylan 582 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
101 | 100 | eqcomd 2827 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) = (𝑀‘𝐴)) |
102 | 101 | breq1d 5069 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ (𝑀‘𝐴) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
103 | 93, 102 | mpbird 259 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
104 | 75, 103 | jca 514 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞) ∧ inf(ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
105 | | iccssxr 12813 |
. . . . . . . . . . . . . . . . . . 19
⊢
(0[,]+∞) ⊆ ℝ* |
106 | | xrltso 12528 |
. . . . . . . . . . . . . . . . . . 19
⊢ < Or
ℝ* |
107 | | soss 5488 |
. . . . . . . . . . . . . . . . . . 19
⊢
((0[,]+∞) ⊆ ℝ* → ( < Or
ℝ* → < Or (0[,]+∞))) |
108 | 105, 106,
107 | mp2 9 |
. . . . . . . . . . . . . . . . . 18
⊢ < Or
(0[,]+∞) |
109 | | biid 263 |
. . . . . . . . . . . . . . . . . 18
⊢ ( < Or
(0[,]+∞) ↔ < Or (0[,]+∞)) |
110 | 108, 109 | mpbi 232 |
. . . . . . . . . . . . . . . . 17
⊢ < Or
(0[,]+∞) |
111 | 110 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → < Or
(0[,]+∞)) |
112 | | omscl 31548 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ∈ 𝒫 ∪ dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞)) |
113 | 95, 96, 45, 112 | syl3anc 1367 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞)) |
114 | | xrge0infss 30478 |
. . . . . . . . . . . . . . . . 17
⊢ (ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞) → ∃𝑣 ∈
(0[,]+∞)(∀ℎ
∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ¬ ℎ < 𝑣 ∧ ∀ℎ ∈ (0[,]+∞)(𝑣 < ℎ → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ℎ))) |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∃𝑣 ∈ (0[,]+∞)(∀ℎ ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ¬ ℎ < 𝑣 ∧ ∀ℎ ∈ (0[,]+∞)(𝑣 < ℎ → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ℎ))) |
116 | 111, 115 | infglb 8948 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ((((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞) ∧ inf(ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
117 | 116 | imp 409 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞) ∧ inf(ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
118 | 23, 24, 104, 117 | syl21anc 835 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
119 | | eqid 2821 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) |
120 | | esumex 31283 |
. . . . . . . . . . . . . . . . . . 19
⊢
Σ*𝑤
∈ 𝑥(𝑅‘𝑤) ∈ V |
121 | 119, 120 | elrnmpti 5827 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) |
122 | 121 | anbi1i 625 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
123 | | r19.41v 3347 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑥 ∈
{𝑧 ∈ 𝒫 dom
𝑅 ∣ (𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
(𝑢 =
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
124 | 122, 123 | bitr4i 280 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
125 | 124 | exbii 1844 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ ∃𝑢∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
126 | | df-rex 3144 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑢 ∈ ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
127 | | rexcom4 3249 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑥 ∈
{𝑧 ∈ 𝒫 dom
𝑅 ∣ (𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ ∃𝑢∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
128 | 125, 126,
127 | 3bitr4i 305 |
. . . . . . . . . . . . . 14
⊢
(∃𝑢 ∈ ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
129 | | breq1 5062 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) → (𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
130 | | idd 24 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) → (Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
131 | 129, 130 | sylbid 242 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) → (𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
132 | 131 | imp 409 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
133 | 132 | exlimiv 1927 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
134 | 133 | reximi 3243 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
{𝑧 ∈ 𝒫 dom
𝑅 ∣ (𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
135 | 128, 134 | sylbi 219 |
. . . . . . . . . . . . 13
⊢
(∃𝑢 ∈ ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
136 | 118, 135 | syl 17 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
137 | | simpr 487 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)
→ 𝑧 ≼
ω) |
138 | 137 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝒫 dom 𝑅 → ((𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω) → 𝑧 ≼ ω)) |
139 | 138 | ss2rabi 4053 |
. . . . . . . . . . . . . 14
⊢ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} |
140 | | rexss 4038 |
. . . . . . . . . . . . . 14
⊢ ({𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
141 | 139, 140 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
{𝑧 ∈ 𝒫 dom
𝑅 ∣ (𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
142 | | unieq 4840 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝑥 → ∪ 𝑧 = ∪
𝑥) |
143 | 142 | sseq2d 3999 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑥 → (𝐴 ⊆ ∪ 𝑧 ↔ 𝐴 ⊆ ∪ 𝑥)) |
144 | | breq1 5062 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑥 → (𝑧 ≼ ω ↔ 𝑥 ≼ ω)) |
145 | 143, 144 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑥 → ((𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω) ↔ (𝐴 ⊆ ∪ 𝑥 ∧ 𝑥 ≼ ω))) |
146 | 145 | elrab 3680 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↔ (𝑥 ∈ 𝒫 dom 𝑅 ∧ (𝐴 ⊆ ∪ 𝑥 ∧ 𝑥 ≼ ω))) |
147 | 146 | simprbi 499 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} → (𝐴 ⊆ ∪ 𝑥 ∧ 𝑥 ≼ ω)) |
148 | 147 | simpld 497 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} → 𝐴 ⊆ ∪ 𝑥) |
149 | 148 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} → 𝐴 ⊆ ∪ 𝑥)) |
150 | 149 | anim1d 612 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ((𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
151 | 150 | reximdv 3273 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
152 | 141, 151 | syl5bi 244 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
153 | 136, 152 | mpd 15 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
154 | 153 | ex 415 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑦 ∈ 𝑋 → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
155 | 22, 154 | ralrimi 3216 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
∀𝑦 ∈ 𝑋 ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
156 | | unieq 4840 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑔‘𝑦) → ∪ 𝑥 = ∪
(𝑔‘𝑦)) |
157 | 156 | sseq2d 3999 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑔‘𝑦) → (𝐴 ⊆ ∪ 𝑥 ↔ 𝐴 ⊆ ∪ (𝑔‘𝑦))) |
158 | | esumeq1 31288 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑔‘𝑦) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) = Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
159 | 158 | breq1d 5069 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑔‘𝑦) → (Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
160 | 157, 159 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑔‘𝑦) → ((𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
161 | 160 | ac6sg 9904 |
. . . . . . . . . 10
⊢ (𝑋 ∈ V → (∀𝑦 ∈ 𝑋 ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))))) |
162 | 161 | imp 409 |
. . . . . . . . 9
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
163 | 12, 155, 162 | syl2anc 586 |
. . . . . . . 8
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
164 | 9 | ad2antrr 724 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝜑) |
165 | 38 | ralrimiva 3182 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅) |
166 | | iunss 4962 |
. . . . . . . . . . . . . . . . . 18
⊢ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅 ↔ ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅) |
167 | 165, 166 | sylibr 236 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅) |
168 | 42 | ralrimiva 3182 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑦 ∈ 𝑋 𝐴 ∈ V) |
169 | | iunexg 7658 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 𝐴 ∈ V) → ∪ 𝑦 ∈ 𝑋 𝐴 ∈ V) |
170 | 11, 168, 169 | syl2anc 586 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ∈ V) |
171 | | elpwg 4545 |
. . . . . . . . . . . . . . . . . 18
⊢ (∪ 𝑦 ∈ 𝑋 𝐴 ∈ V → (∪ 𝑦 ∈ 𝑋 𝐴 ∈ 𝒫 ∪ dom 𝑅 ↔ ∪
𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅)) |
172 | 170, 171 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (∪ 𝑦 ∈ 𝑋 𝐴 ∈ 𝒫 ∪ dom 𝑅 ↔ ∪
𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅)) |
173 | 167, 172 | mpbird 259 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ∈ 𝒫 ∪ dom 𝑅) |
174 | 32, 173 | ffvelrnd 6847 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ∈ (0[,]+∞)) |
175 | 105, 174 | sseldi 3965 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ∈
ℝ*) |
176 | 164, 175 | syl 17 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ∈
ℝ*) |
177 | | simplr 767 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
178 | 25 | ad4antr 730 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑋 ∈ V) |
179 | | fex 6983 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ 𝑋 ∈ V) → 𝑔 ∈ V) |
180 | 177, 178,
179 | syl2anc 586 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑔 ∈ V) |
181 | | rnexg 7608 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 ∈ V → ran 𝑔 ∈ V) |
182 | | uniexg 7460 |
. . . . . . . . . . . . . . . 16
⊢ (ran
𝑔 ∈ V → ∪ ran 𝑔 ∈ V) |
183 | 180, 181,
182 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪
ran 𝑔 ∈
V) |
184 | | simp-5l 783 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝜑) |
185 | 27 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑐 ∈ ∪ ran
𝑔) → 𝑅:𝑄⟶(0[,]+∞)) |
186 | | frn 6515 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
187 | | ssrab2 4056 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ⊆ 𝒫 dom 𝑅 |
188 | 186, 187 | sstrdi 3979 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ran 𝑔 ⊆ 𝒫 dom 𝑅) |
189 | 188 | unissd 4856 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∪ ran 𝑔 ⊆ ∪
𝒫 dom 𝑅) |
190 | | unipw 5335 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ∪ 𝒫 dom 𝑅 = dom 𝑅 |
191 | 189, 190 | sseqtrdi 4017 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∪ ran 𝑔 ⊆ dom 𝑅) |
192 | 191 | adantl 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∪ ran 𝑔 ⊆ dom 𝑅) |
193 | 35 | adantr 483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → dom 𝑅 = 𝑄) |
194 | 192, 193 | sseqtrd 4007 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∪ ran 𝑔 ⊆ 𝑄) |
195 | 194 | sselda 3967 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑐 ∈ ∪ ran
𝑔) → 𝑐 ∈ 𝑄) |
196 | 185, 195 | ffvelrnd 6847 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑐 ∈ ∪ ran
𝑔) → (𝑅‘𝑐) ∈ (0[,]+∞)) |
197 | 196 | ralrimiva 3182 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∀𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ (0[,]+∞)) |
198 | 184, 177,
197 | syl2anc 586 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ∈ (0[,]+∞)) |
199 | | nfcv 2977 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑐∪ ran 𝑔 |
200 | 199 | esumcl 31284 |
. . . . . . . . . . . . . . 15
⊢ ((∪ ran 𝑔 ∈ V ∧ ∀𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ∈ (0[,]+∞)) →
Σ*𝑐 ∈
∪ ran 𝑔(𝑅‘𝑐) ∈ (0[,]+∞)) |
201 | 183, 198,
200 | syl2anc 586 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ (0[,]+∞)) |
202 | 105, 201 | sseldi 3965 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈
ℝ*) |
203 | | simp-5r 784 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) |
204 | 203 | rexrd 10685 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈
ℝ*) |
205 | | simpllr 774 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑒 ∈ ℝ+) |
206 | 205 | rpxrd 12426 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑒 ∈ ℝ*) |
207 | 204, 206 | xaddcld 12688 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒) ∈
ℝ*) |
208 | 186 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
209 | | sstr 3975 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ⊆ 𝒫 dom 𝑅) → ran 𝑔 ⊆ 𝒫 dom 𝑅) |
210 | 187, 209 | mpan2 689 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ran 𝑔 ⊆ 𝒫 dom 𝑅) |
211 | | sspwuni 5015 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ran
𝑔 ⊆ 𝒫 dom
𝑅 ↔ ∪ ran 𝑔 ⊆ dom 𝑅) |
212 | 210, 211 | sylib 220 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∪ ran 𝑔 ⊆ dom 𝑅) |
213 | 208, 212 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪
ran 𝑔 ⊆ dom 𝑅) |
214 | | ffn 6509 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → 𝑔 Fn 𝑋) |
215 | 214 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑔 Fn 𝑋) |
216 | 164, 1 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑋 ≼ ω) |
217 | | fnct 9953 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑔 Fn 𝑋 ∧ 𝑋 ≼ ω) → 𝑔 ≼ ω) |
218 | | rnct 9941 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑔 ≼ ω → ran
𝑔 ≼
ω) |
219 | 217, 218 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑔 Fn 𝑋 ∧ 𝑋 ≼ ω) → ran 𝑔 ≼
ω) |
220 | | dfss3 3956 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ↔ ∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
221 | 220 | biimpi 218 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
222 | | breq1 5062 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 = 𝑤 → (𝑧 ≼ ω ↔ 𝑤 ≼ ω)) |
223 | 222 | elrab 3680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ↔ (𝑤 ∈ 𝒫 dom 𝑅 ∧ 𝑤 ≼ ω)) |
224 | 223 | simprbi 499 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → 𝑤 ≼ ω) |
225 | 224 | ralimi 3160 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∀𝑤 ∈
ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω) |
226 | 221, 225 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω) |
227 | | unictb 9991 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ran
𝑔 ≼ ω ∧
∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω) → ∪ ran 𝑔 ≼ ω) |
228 | 219, 226,
227 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑔 Fn 𝑋 ∧ 𝑋 ≼ ω) ∧ ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∪ ran 𝑔 ≼ ω) |
229 | 215, 216,
208, 228 | syl21anc 835 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪
ran 𝑔 ≼
ω) |
230 | | ctex 8518 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (∪ ran 𝑔 ≼ ω → ∪ ran 𝑔 ∈ V) |
231 | | elpwg 4545 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (∪ ran 𝑔 ∈ V → (∪ ran 𝑔 ∈ 𝒫 dom 𝑅 ↔ ∪ ran
𝑔 ⊆ dom 𝑅)) |
232 | 229, 230,
231 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (∪
ran 𝑔 ∈ 𝒫 dom
𝑅 ↔ ∪ ran 𝑔 ⊆ dom 𝑅)) |
233 | 213, 232 | mpbird 259 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪
ran 𝑔 ∈ 𝒫 dom
𝑅) |
234 | | simpl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → 𝐴 ⊆ ∪ (𝑔‘𝑦)) |
235 | 234 | ralimi 3160 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑦 ∈
𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ (𝑔‘𝑦)) |
236 | | fvssunirn 6694 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑔‘𝑦) ⊆ ∪ ran
𝑔 |
237 | 236 | unissi 4855 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ∪ (𝑔‘𝑦) ⊆ ∪ ∪ ran 𝑔 |
238 | | sstr 3975 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ ∪ (𝑔‘𝑦) ⊆ ∪ ∪ ran 𝑔) → 𝐴 ⊆ ∪ ∪ ran 𝑔) |
239 | 237, 238 | mpan2 689 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ⊆ ∪ (𝑔‘𝑦) → 𝐴 ⊆ ∪ ∪ ran 𝑔) |
240 | 239 | ralimi 3160 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∀𝑦 ∈
𝑋 𝐴 ⊆ ∪ (𝑔‘𝑦) → ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔) |
241 | | iunss 4962 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔 ↔ ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔) |
242 | 240, 241 | sylibr 236 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑦 ∈
𝑋 𝐴 ⊆ ∪ (𝑔‘𝑦) → ∪
𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔) |
243 | 235, 242 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑦 ∈
𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔) |
244 | 243 | adantl 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔) |
245 | 233, 244,
229 | jca32 518 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (∪
ran 𝑔 ∈ 𝒫 dom
𝑅 ∧ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔 ∧ ∪ ran 𝑔 ≼
ω))) |
246 | | unieq 4840 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = ∪
ran 𝑔 → ∪ 𝑧 =
∪ ∪ ran 𝑔) |
247 | 246 | sseq2d 3999 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = ∪
ran 𝑔 → (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ↔ ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔)) |
248 | | breq1 5062 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = ∪
ran 𝑔 → (𝑧 ≼ ω ↔ ∪ ran 𝑔 ≼ ω)) |
249 | 247, 248 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = ∪
ran 𝑔 → ((∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω) ↔ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔 ∧ ∪ ran 𝑔 ≼
ω))) |
250 | 249 | elrab 3680 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∪ ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↔ (∪ ran 𝑔 ∈ 𝒫 dom 𝑅 ∧ (∪
𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔 ∧ ∪ ran 𝑔 ≼
ω))) |
251 | 245, 250 | sylibr 236 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪
ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}) |
252 | | fveq2 6665 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 = 𝑤 → (𝑅‘𝑐) = (𝑅‘𝑤)) |
253 | 252 | cbvesumv 31297 |
. . . . . . . . . . . . . . . . . 18
⊢
Σ*𝑐
∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ ∪ ran
𝑔(𝑅‘𝑤) |
254 | | esumeq1 31288 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = ∪
ran 𝑔 →
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) = Σ*𝑤 ∈ ∪ ran
𝑔(𝑅‘𝑤)) |
255 | 254 | rspceeqv 3638 |
. . . . . . . . . . . . . . . . . 18
⊢ ((∪ ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧
Σ*𝑐 ∈
∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ ∪ ran
𝑔(𝑅‘𝑤)) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) |
256 | 251, 253,
255 | sylancl 588 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) |
257 | | esumex 31283 |
. . . . . . . . . . . . . . . . . 18
⊢
Σ*𝑐
∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ V |
258 | | eqid 2821 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) |
259 | 258 | elrnmpt 5823 |
. . . . . . . . . . . . . . . . . 18
⊢
(Σ*𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ∈ V → (Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤))) |
260 | 257, 259 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(Σ*𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) |
261 | 256, 260 | sylibr 236 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))) |
262 | 110 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → < Or
(0[,]+∞)) |
263 | | omscl 31548 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ ∪ 𝑦 ∈ 𝑋 𝐴 ∈ 𝒫 ∪ dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞)) |
264 | 26, 27, 173, 263 | syl3anc 1367 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞)) |
265 | | xrge0infss 30478 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞) → ∃𝑒 ∈
(0[,]+∞)(∀𝑡
∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ¬ 𝑡 < 𝑒 ∧ ∀𝑡 ∈ (0[,]+∞)(𝑒 < 𝑡 → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < 𝑡))) |
266 | 264, 265 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∃𝑒 ∈ (0[,]+∞)(∀𝑡 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ¬ 𝑡 < 𝑒 ∧ ∀𝑡 ∈ (0[,]+∞)(𝑒 < 𝑡 → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < 𝑡))) |
267 | 262, 266 | inflb 8947 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) → ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ))) |
268 | 29 | fveq1i 6666 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) = ((toOMeas‘𝑅)‘∪
𝑦 ∈ 𝑋 𝐴) |
269 | 167, 36 | sseqtrd 4007 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑄) |
270 | | omsfval 31547 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑄) → ((toOMeas‘𝑅)‘∪ 𝑦 ∈ 𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
271 | 26, 27, 269, 270 | syl3anc 1367 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((toOMeas‘𝑅)‘∪ 𝑦 ∈ 𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
272 | 268, 271 | syl5eq 2868 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
273 | 272 | breq2d 5071 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ↔ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ))) |
274 | 273 | notbid 320 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (¬
Σ*𝑐 ∈
∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ↔ ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ))) |
275 | 267, 274 | sylibrd 261 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) → ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴))) |
276 | 164, 261,
275 | sylc 65 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴)) |
277 | | biid 263 |
. . . . . . . . . . . . . . 15
⊢ (¬
Σ*𝑐 ∈
∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ↔ ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴)) |
278 | 276, 277 | sylib 220 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴)) |
279 | | xrlenlt 10700 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ∈ ℝ* ∧
Σ*𝑐 ∈
∪ ran 𝑔(𝑅‘𝑐) ∈ ℝ*) → ((𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ↔ ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴))) |
280 | 176, 202,
279 | syl2anc 586 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ((𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ↔ ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴))) |
281 | 278, 280 | mpbird 259 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐)) |
282 | | nfv 1911 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑦 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} |
283 | 22, 282 | nfan 1896 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑦((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
284 | | nfra1 3219 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑦∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
285 | 283, 284 | nfan 1896 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑦(((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
286 | | simp-6l 785 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → 𝜑) |
287 | | simpllr 774 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
288 | | simpr 487 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
289 | 27 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑅:𝑄⟶(0[,]+∞)) |
290 | | simpllr 774 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
291 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑦 ∈ 𝑋) |
292 | 290, 291 | ffvelrnd 6847 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
293 | 187, 292 | sseldi 3965 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ∈ 𝒫 dom 𝑅) |
294 | 293 | elpwid 4553 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ⊆ dom 𝑅) |
295 | 289, 294 | fssdmd 6524 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ⊆ 𝑄) |
296 | | simpr 487 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑤 ∈ (𝑔‘𝑦)) |
297 | 295, 296 | sseldd 3968 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑤 ∈ 𝑄) |
298 | 289, 297 | ffvelrnd 6847 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑅‘𝑤) ∈ (0[,]+∞)) |
299 | 298 | ralrimiva 3182 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → ∀𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
300 | | fvex 6678 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔‘𝑦) ∈ V |
301 | | nfcv 2977 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑤(𝑔‘𝑦) |
302 | 301 | esumcl 31284 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑔‘𝑦) ∈ V ∧ ∀𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) →
Σ*𝑤 ∈
(𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
303 | 300, 302 | mpan 688 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑤 ∈
(𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞) →
Σ*𝑤 ∈
(𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
304 | 299, 303 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
305 | 286, 287,
288, 304 | syl21anc 835 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
306 | 305 | ex 415 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑦 ∈ 𝑋 → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞))) |
307 | 285, 306 | ralrimi 3216 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
308 | 14 | esumcl 31284 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) →
Σ*𝑦 ∈
𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
309 | 178, 307,
308 | syl2anc 586 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
310 | 105, 309 | sseldi 3965 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈
ℝ*) |
311 | | nfv 1911 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑤(𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
312 | | simpr 487 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
313 | | fniunfv 7000 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 Fn 𝑋 → ∪
𝑦 ∈ 𝑋 (𝑔‘𝑦) = ∪ ran 𝑔) |
314 | 312, 214,
313 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∪ 𝑦 ∈ 𝑋 (𝑔‘𝑦) = ∪ ran 𝑔) |
315 | 311, 314 | esumeq1d 31289 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) →
Σ*𝑤 ∈
∪ 𝑦 ∈ 𝑋 (𝑔‘𝑦)(𝑅‘𝑤) = Σ*𝑤 ∈ ∪ ran
𝑔(𝑅‘𝑤)) |
316 | 11 | adantr 483 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → 𝑋 ∈ V) |
317 | 300 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑔‘𝑦) ∈ V) |
318 | 316, 317,
298 | esumiun 31348 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) →
Σ*𝑤 ∈
∪ 𝑦 ∈ 𝑋 (𝑔‘𝑦)(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
319 | 315, 318 | eqbrtrrd 5083 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) →
Σ*𝑤 ∈
∪ ran 𝑔(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
320 | 9, 319 | sylan 582 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) →
Σ*𝑤 ∈
∪ ran 𝑔(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
321 | 320 | adantr 483 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑤 ∈ ∪ ran 𝑔(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
322 | 253, 321 | eqbrtrid 5094 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
323 | 286, 288,
46 | syl2anc 586 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞)) |
324 | | simplll 773 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈
ℝ+)) |
325 | 324, 288,
73 | syl2anc 586 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
326 | 323, 325 | xrge0addcld 30480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
327 | 326 | ex 415 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑦 ∈ 𝑋 → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞))) |
328 | 285, 327 | ralrimi 3216 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
329 | 14 | esumcl 31284 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) →
Σ*𝑦 ∈
𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
330 | 178, 328,
329 | syl2anc 586 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
331 | 105, 330 | sseldi 3965 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈
ℝ*) |
332 | 216, 10 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑋 ∈ V) |
333 | | simp-4l 781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ)) |
334 | | simpr 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
335 | 333, 334,
49 | syl2anc 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ ℝ) |
336 | 335 | adantr 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → (𝑀‘𝐴) ∈ ℝ) |
337 | 65 | adantlr 713 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
338 | 337 | adantr 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
339 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
340 | 339 | adantl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
341 | 66 | breq2d 5071 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑀‘𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) →
(Σ*𝑤
∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ↔ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
342 | 341 | biimpar 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑀‘𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) ∧
Σ*𝑤 ∈
(𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) |
343 | 336, 338,
340, 342 | syl21anc 835 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) |
344 | 343 | ex 415 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
345 | 333 | simpld 497 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → 𝜑) |
346 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
347 | 345, 346,
334, 304 | syl21anc 835 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
348 | 105, 347 | sseldi 3965 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈
ℝ*) |
349 | 335 | rexrd 10685 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈
ℝ*) |
350 | 337 | rexrd 10685 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈
ℝ*) |
351 | 349, 350 | xaddcld 12688 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈
ℝ*) |
352 | | xrltle 12536 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ ℝ* ∧ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ ℝ*) →
(Σ*𝑤
∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
353 | 348, 351,
352 | syl2anc 586 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
354 | 344, 353 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
355 | 354 | adantld 493 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
356 | 355 | ex 415 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → (𝑦 ∈ 𝑋 → ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))))) |
357 | 283, 356 | ralrimi 3216 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∀𝑦 ∈ 𝑋 ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
358 | | ralim 3162 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑦 ∈
𝑋 ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) → (∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
359 | 357, 358 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → (∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
360 | 359 | imp 409 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) |
361 | 360 | r19.21bi 3208 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) |
362 | 285, 14, 332, 305, 326, 361 | esumlef 31316 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) |
363 | 164, 46 | sylan 582 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞)) |
364 | 285, 14, 332, 363, 325 | esumaddf 31315 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) = (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦))))) |
365 | 325 | ex 415 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑦 ∈ 𝑋 → (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞))) |
366 | 285, 365 | ralrimi 3216 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
367 | 14 | esumcl 31284 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) →
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
368 | 178, 366,
367 | syl2anc 586 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
369 | 105, 368 | sseldi 3965 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈
ℝ*) |
370 | | simp-4r 782 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑓:𝑋–1-1→ℕ) |
371 | | vex 3498 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑓 ∈ V |
372 | 371 | rnex 7611 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ran 𝑓 ∈ V |
373 | 372 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ran 𝑓 ∈ V) |
374 | 58 | frnd 6516 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → ran 𝑓 ⊆ ℕ) |
375 | 374 | adantr 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ran 𝑓 ⊆
ℕ) |
376 | 375 | sselda 3967 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ ℕ) |
377 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 2 ∈
ℝ+) |
378 | | simpr 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 𝑧 ∈ ℕ) |
379 | 378 | nnzd 12080 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 𝑧 ∈ ℤ) |
380 | 377, 379 | rpexpcld 13602 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (2↑𝑧) ∈
ℝ+) |
381 | 380 | rpreccld 12435 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈
ℝ+) |
382 | 71, 381 | sseldi 3965 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈
(0[,]+∞)) |
383 | 382 | adantlr 713 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ℕ) → (1 /
(2↑𝑧)) ∈
(0[,]+∞)) |
384 | 376, 383 | syldan 593 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ran 𝑓) → (1 / (2↑𝑧)) ∈ (0[,]+∞)) |
385 | 384 | ralrimiva 3182 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
∀𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞)) |
386 | | nfcv 2977 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑧ran
𝑓 |
387 | 386 | esumcl 31284 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ran
𝑓 ∈ V ∧
∀𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞)) →
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)) ∈
(0[,]+∞)) |
388 | 373, 385,
387 | syl2anc 586 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)) ∈
(0[,]+∞)) |
389 | 105, 388 | sseldi 3965 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)) ∈
ℝ*) |
390 | | 1xr 10694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℝ* |
391 | 390 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 1 ∈
ℝ*) |
392 | 71 | sseli 3963 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑒 ∈ ℝ+
→ 𝑒 ∈
(0[,]+∞)) |
393 | 392 | adantl 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈
(0[,]+∞)) |
394 | | elxrge0 12839 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑒 ∈ (0[,]+∞) ↔
(𝑒 ∈
ℝ* ∧ 0 ≤ 𝑒)) |
395 | 393, 394 | sylib 220 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ∈ ℝ*
∧ 0 ≤ 𝑒)) |
396 | | nfv 1911 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑧(𝜑 ∧ 𝑓:𝑋–1-1→ℕ) |
397 | | nnex 11638 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ℕ
∈ V |
398 | 397 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → ℕ ∈
V) |
399 | 396, 398,
382, 374 | esummono 31308 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ Σ*𝑧 ∈ ℕ(1 / (2↑𝑧))) |
400 | | oveq2 7158 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = 𝑤 → (2↑𝑧) = (2↑𝑤)) |
401 | 400 | oveq2d 7166 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = 𝑤 → (1 / (2↑𝑧)) = (1 / (2↑𝑤))) |
402 | | ioossico 12820 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(0(,)+∞) ⊆ (0[,)+∞) |
403 | 69, 402 | eqsstri 4001 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
ℝ+ ⊆ (0[,)+∞) |
404 | 403, 381 | sseldi 3965 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈
(0[,)+∞)) |
405 | | eqidd 2822 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ ℕ → (𝑤 ∈ ℕ ↦ (1 /
(2↑𝑤))) = (𝑤 ∈ ℕ ↦ (1 /
(2↑𝑤)))) |
406 | | simpr 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → 𝑤 = 𝑧) |
407 | 406 | oveq2d 7166 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → (2↑𝑤) = (2↑𝑧)) |
408 | 407 | oveq2d 7166 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → (1 / (2↑𝑤)) = (1 / (2↑𝑧))) |
409 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℕ) |
410 | | ovexd 7185 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ ℕ → (1 /
(2↑𝑧)) ∈
V) |
411 | 405, 408,
409, 410 | fvmptd 6770 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 ∈ ℕ → ((𝑤 ∈ ℕ ↦ (1 /
(2↑𝑤)))‘𝑧) = (1 / (2↑𝑧))) |
412 | 411 | adantl 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → ((𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))‘𝑧) = (1 / (2↑𝑧))) |
413 | | ax-1cn 10589 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 1 ∈
ℂ |
414 | | eqid 2821 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ ℕ ↦ (1 /
(2↑𝑤))) = (𝑤 ∈ ℕ ↦ (1 /
(2↑𝑤))) |
415 | 414 | geo2lim 15225 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (1 ∈
ℂ → seq1( + , (𝑤
∈ ℕ ↦ (1 / (2↑𝑤)))) ⇝ 1) |
416 | 413, 415 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ seq1( + ,
(𝑤 ∈ ℕ ↦
(1 / (2↑𝑤)))) ⇝
1 |
417 | 416 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → seq1( + , (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))) ⇝ 1) |
418 | | 1re 10635 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 ∈
ℝ |
419 | 418 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → 1 ∈
ℝ) |
420 | 401, 404,
412, 417, 419 | esumcvgsum 31342 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ℕ(1 /
(2↑𝑧)) = Σ𝑧 ∈ ℕ (1 /
(2↑𝑧))) |
421 | | geoihalfsum 15232 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Σ𝑧 ∈
ℕ (1 / (2↑𝑧)) =
1 |
422 | 420, 421 | syl6eq 2872 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ℕ(1 /
(2↑𝑧)) =
1) |
423 | 399, 422 | breqtrd 5085 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1) |
424 | 423 | adantr 483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)) ≤ 1) |
425 | | xlemul2a 12676 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ ℝ* ∧ 1 ∈
ℝ* ∧ (𝑒 ∈ ℝ* ∧ 0 ≤
𝑒)) ∧
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)) ≤ 1) → (𝑒 ·e
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧))) ≤ (𝑒 ·e 1)) |
426 | 389, 391,
395, 424, 425 | syl31anc 1369 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧))) ≤ (𝑒 ·e 1)) |
427 | 13, 19 | nfan 1896 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑦(𝜑 ∧ 𝑓:𝑋–1-1→ℕ) |
428 | 427, 21 | nfan 1896 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑦((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) |
429 | 76 | recnd 10663 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℂ) |
430 | 78 | recnd 10663 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℂ) |
431 | 430 | adantlr 713 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℂ) |
432 | | 2cn 11706 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 2 ∈
ℂ |
433 | 432 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → 2 ∈ ℂ) |
434 | | 2ne0 11735 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 2 ≠
0 |
435 | 434 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → 2 ≠ 0) |
436 | 433, 435,
60 | expne0d 13510 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ≠ 0) |
437 | 436 | adantlr 713 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ≠ 0) |
438 | 429, 431,
437 | divrecd 11413 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) = (𝑒 · (1 / (2↑(𝑓‘𝑦))))) |
439 | | 1rp 12387 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 1 ∈
ℝ+ |
440 | 439 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → 1 ∈
ℝ+) |
441 | 440, 61 | rpdivcld 12442 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈
ℝ+) |
442 | 52, 441 | sseldi 3965 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
443 | 442 | adantlr 713 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
444 | | rexmul 12658 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑒 ∈ ℝ ∧ (1 /
(2↑(𝑓‘𝑦))) ∈ ℝ) →
(𝑒 ·e (1
/ (2↑(𝑓‘𝑦)))) = (𝑒 · (1 / (2↑(𝑓‘𝑦))))) |
445 | 76, 443, 444 | syl2anc 586 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 ·e (1 / (2↑(𝑓‘𝑦)))) = (𝑒 · (1 / (2↑(𝑓‘𝑦))))) |
446 | 438, 445 | eqtr4d 2859 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) = (𝑒 ·e (1 / (2↑(𝑓‘𝑦))))) |
447 | 446 | ralrimiva 3182 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
∀𝑦 ∈ 𝑋 (𝑒 / (2↑(𝑓‘𝑦))) = (𝑒 ·e (1 / (2↑(𝑓‘𝑦))))) |
448 | 428, 447 | esumeq2d 31291 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦))) = Σ*𝑦 ∈ 𝑋(𝑒 ·e (1 / (2↑(𝑓‘𝑦))))) |
449 | 11 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑋 ∈ V) |
450 | 71, 441 | sseldi 3965 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
451 | 450 | adantlr 713 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
452 | 403 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → ℝ+ ⊆
(0[,)+∞)) |
453 | 452 | sselda 3967 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈
(0[,)+∞)) |
454 | 449, 451,
453 | esummulc2 31336 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e
Σ*𝑦 ∈
𝑋(1 / (2↑(𝑓‘𝑦)))) = Σ*𝑦 ∈ 𝑋(𝑒 ·e (1 / (2↑(𝑓‘𝑦))))) |
455 | | nfcv 2977 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑦(1 /
(2↑𝑧)) |
456 | | oveq2 7158 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = (𝑓‘𝑦) → (2↑𝑧) = (2↑(𝑓‘𝑦))) |
457 | 456 | oveq2d 7166 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = (𝑓‘𝑦) → (1 / (2↑𝑧)) = (1 / (2↑(𝑓‘𝑦)))) |
458 | 11 | adantr 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → 𝑋 ∈ V) |
459 | 56 | simprbi 499 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓:𝑋–1-1→ℕ → Fun ◡𝑓) |
460 | 57 | feqmptd 6728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓:𝑋–1-1→ℕ → 𝑓 = (𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦))) |
461 | 460 | cnveqd 5741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓:𝑋–1-1→ℕ → ◡𝑓 = ◡(𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦))) |
462 | 461 | funeqd 6372 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓:𝑋–1-1→ℕ → (Fun ◡𝑓 ↔ Fun ◡(𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦)))) |
463 | 459, 462 | mpbid 234 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓:𝑋–1-1→ℕ → Fun ◡(𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦))) |
464 | 463 | adantl 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Fun ◡(𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦))) |
465 | 455, 427,
14, 457, 458, 464, 450, 59 | esumc 31305 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑦 ∈ 𝑋(1 / (2↑(𝑓‘𝑦))) = Σ*𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)} (1 / (2↑𝑧))) |
466 | | ffn 6509 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓:𝑋⟶ℕ → 𝑓 Fn 𝑋) |
467 | | fnrnfv 6720 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 Fn 𝑋 → ran 𝑓 = {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)}) |
468 | 58, 466, 467 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → ran 𝑓 = {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)}) |
469 | 396, 468 | esumeq1d 31289 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) = Σ*𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)} (1 / (2↑𝑧))) |
470 | 465, 469 | eqtr4d 2859 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑦 ∈ 𝑋(1 / (2↑(𝑓‘𝑦))) = Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) |
471 | 470 | adantr 483 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑦 ∈
𝑋(1 / (2↑(𝑓‘𝑦))) = Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) |
472 | 471 | oveq2d 7166 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e
Σ*𝑦 ∈
𝑋(1 / (2↑(𝑓‘𝑦)))) = (𝑒 ·e
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)))) |
473 | 448, 454,
472 | 3eqtr2rd 2863 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧))) = Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦)))) |
474 | 395 | simpld 497 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈
ℝ*) |
475 | | xmulid1 12666 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑒 ∈ ℝ*
→ (𝑒
·e 1) = 𝑒) |
476 | 474, 475 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e 1) = 𝑒) |
477 | 426, 473,
476 | 3brtr3d 5090 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦))) ≤ 𝑒) |
478 | 164, 370,
205, 477 | syl21anc 835 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ≤ 𝑒) |
479 | | xleadd2a 12641 |
. . . . . . . . . . . . . . . . 17
⊢
(((Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ* ∧ 𝑒 ∈ ℝ*
∧ Σ*𝑦
∈ 𝑋(𝑀‘𝐴) ∈ ℝ*) ∧
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦))) ≤ 𝑒) → (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦)))) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
480 | 369, 206,
204, 478, 479 | syl31anc 1369 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦)))) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
481 | 364, 480 | eqbrtrd 5081 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
482 | 310, 331,
207, 362, 481 | xrletrd 12549 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
483 | 202, 310,
207, 322, 482 | xrletrd 12549 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
484 | 176, 202,
207, 281, 483 | xrletrd 12549 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
485 | 205 | rpred 12425 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑒 ∈ ℝ) |
486 | | rexadd 12619 |
. . . . . . . . . . . . 13
⊢
((Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ ∧ 𝑒 ∈ ℝ) →
(Σ*𝑦
∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒) = (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
487 | 203, 485,
486 | syl2anc 586 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒) = (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
488 | 484, 487 | breqtrd 5085 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
489 | 488 | anasss 469 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
490 | 489 | ex 415 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ((𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))) |
491 | 490 | exlimdv 1930 |
. . . . . . . 8
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
(∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))) |
492 | 163, 491 | mpd 15 |
. . . . . . 7
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
493 | 492 | ralrimiva 3182 |
. . . . . 6
⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) → ∀𝑒 ∈ ℝ+ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
494 | | xralrple 12592 |
. . . . . . . 8
⊢ (((𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ∈ ℝ* ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) → ((𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))) |
495 | 175, 494 | sylan 582 |
. . . . . . 7
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → ((𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))) |
496 | 495 | adantr 483 |
. . . . . 6
⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) → ((𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))) |
497 | 493, 496 | mpbird 259 |
. . . . 5
⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴)) |
498 | 497 | ex 415 |
. . . 4
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑓:𝑋–1-1→ℕ → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴))) |
499 | 498 | exlimdv 1930 |
. . 3
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → (∃𝑓 𝑓:𝑋–1-1→ℕ → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴))) |
500 | 8, 499 | mpd 15 |
. 2
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴)) |
501 | 175 | adantr 483 |
. . . 4
⊢ ((𝜑 ∧ ¬
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ∈
ℝ*) |
502 | | pnfge 12519 |
. . . 4
⊢ ((𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ∈ ℝ* → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ +∞) |
503 | 501, 502 | syl 17 |
. . 3
⊢ ((𝜑 ∧ ¬
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ +∞) |
504 | 46 | ralrimiva 3182 |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ 𝑋 (𝑀‘𝐴) ∈ (0[,]+∞)) |
505 | 14 | esumcl 31284 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 (𝑀‘𝐴) ∈ (0[,]+∞)) →
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ (0[,]+∞)) |
506 | 11, 504, 505 | syl2anc 586 |
. . . 4
⊢ (𝜑 → Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ (0[,]+∞)) |
507 | | xrge0nre 12835 |
. . . 4
⊢
((Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ (0[,]+∞) ∧ ¬
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) →
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) = +∞) |
508 | 506, 507 | sylan 582 |
. . 3
⊢ ((𝜑 ∧ ¬
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) →
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) = +∞) |
509 | 503, 508 | breqtrrd 5087 |
. 2
⊢ ((𝜑 ∧ ¬
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴)) |
510 | 500, 509 | pm2.61dan 811 |
1
⊢ (𝜑 → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴)) |