Step | Hyp | Ref
| Expression |
1 | | omssubadd.b |
. . . . . 6
⊢ (𝜑 → 𝑋 ≼ ω) |
2 | | nnenom 13074 |
. . . . . . 7
⊢ ℕ
≈ ω |
3 | 2 | ensymi 8272 |
. . . . . 6
⊢ ω
≈ ℕ |
4 | | domentr 8281 |
. . . . . 6
⊢ ((𝑋 ≼ ω ∧ ω
≈ ℕ) → 𝑋
≼ ℕ) |
5 | 1, 3, 4 | sylancl 580 |
. . . . 5
⊢ (𝜑 → 𝑋 ≼ ℕ) |
6 | | brdomi 8233 |
. . . . 5
⊢ (𝑋 ≼ ℕ →
∃𝑓 𝑓:𝑋–1-1→ℕ) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝜑 → ∃𝑓 𝑓:𝑋–1-1→ℕ) |
8 | 7 | adantr 474 |
. . 3
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → ∃𝑓 𝑓:𝑋–1-1→ℕ) |
9 | | simplll 791 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝜑) |
10 | | ctex 8237 |
. . . . . . . . . . 11
⊢ (𝑋 ≼ ω → 𝑋 ∈ V) |
11 | 1, 10 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ V) |
12 | 9, 11 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑋 ∈ V) |
13 | | nfv 2013 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦𝜑 |
14 | | nfcv 2969 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦𝑋 |
15 | 14 | nfesum1 30636 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) |
16 | | nfcv 2969 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦ℝ |
17 | 15, 16 | nfel 2982 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ |
18 | 13, 17 | nfan 2002 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) |
19 | | nfv 2013 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦 𝑓:𝑋–1-1→ℕ |
20 | 18, 19 | nfan 2002 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) |
21 | | nfv 2013 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 𝑒 ∈
ℝ+ |
22 | 20, 21 | nfan 2002 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) |
23 | 9 | adantr 474 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝜑) |
24 | | simpr 479 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
25 | 11 | adantr 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → 𝑋 ∈ V) |
26 | | oms.o |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑄 ∈ 𝑉) |
27 | | oms.r |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑅:𝑄⟶(0[,]+∞)) |
28 | | omsf 30892 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞)) →
(toOMeas‘𝑅):𝒫
∪ dom 𝑅⟶(0[,]+∞)) |
29 | | oms.m |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑀 = (toOMeas‘𝑅) |
30 | 29 | feq1i 6269 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑀:𝒫 ∪ dom 𝑅⟶(0[,]+∞) ↔
(toOMeas‘𝑅):𝒫
∪ dom 𝑅⟶(0[,]+∞)) |
31 | 28, 30 | sylibr 226 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞)) → 𝑀:𝒫 ∪ dom 𝑅⟶(0[,]+∞)) |
32 | 26, 27, 31 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑀:𝒫 ∪ dom
𝑅⟶(0[,]+∞)) |
33 | 32 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑀:𝒫 ∪ dom
𝑅⟶(0[,]+∞)) |
34 | | omssubadd.a |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ⊆ ∪ 𝑄) |
35 | 27 | fdmd 6287 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → dom 𝑅 = 𝑄) |
36 | 35 | unieqd 4668 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ∪ dom 𝑅 = ∪ 𝑄) |
37 | 36 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∪ dom
𝑅 = ∪ 𝑄) |
38 | 34, 37 | sseqtr4d 3867 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ⊆ ∪ dom
𝑅) |
39 | | uniexg 7215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑄 ∈ 𝑉 → ∪ 𝑄 ∈ V) |
40 | 26, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ∪ 𝑄
∈ V) |
41 | 40 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∪ 𝑄 ∈ V) |
42 | | ssexg 5029 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ⊆ ∪ 𝑄
∧ ∪ 𝑄 ∈ V) → 𝐴 ∈ V) |
43 | 34, 41, 42 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ∈ V) |
44 | | elpwg 4386 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 ∪ dom 𝑅 ↔ 𝐴 ⊆ ∪ dom
𝑅)) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐴 ∈ 𝒫 ∪ dom 𝑅 ↔ 𝐴 ⊆ ∪ dom
𝑅)) |
46 | 38, 45 | mpbird 249 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ∈ 𝒫 ∪ dom 𝑅) |
47 | 33, 46 | ffvelrnd 6609 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞)) |
48 | 47 | adantlr 706 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞)) |
49 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) →
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) |
50 | 18, 25, 48, 49 | esumcvgre 30687 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ ℝ) |
51 | 50 | adantlr 706 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ ℝ) |
52 | 51 | adantlr 706 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ ℝ) |
53 | | rpssre 12119 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℝ+ ⊆ ℝ |
54 | | simplr 785 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℝ+) |
55 | | 2rp 12117 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℝ+ |
56 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → 2 ∈
ℝ+) |
57 | | df-f1 6128 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓:𝑋–1-1→ℕ ↔ (𝑓:𝑋⟶ℕ ∧ Fun ◡𝑓)) |
58 | 57 | simplbi 493 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓:𝑋–1-1→ℕ → 𝑓:𝑋⟶ℕ) |
59 | 58 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → 𝑓:𝑋⟶ℕ) |
60 | 59 | ffvelrnda 6608 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℕ) |
61 | 60 | nnzd 11809 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℤ) |
62 | 56, 61 | rpexpcld 13328 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈
ℝ+) |
63 | 62 | adantlr 706 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈
ℝ+) |
64 | 54, 63 | rpdivcld 12173 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈
ℝ+) |
65 | 53, 64 | sseldi 3825 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
66 | 65 | adantl3r 756 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
67 | | rexadd 12351 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀‘𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) = ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
68 | 52, 66, 67 | syl2anc 579 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) = ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
69 | 9, 47 | sylan 575 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞)) |
70 | | dfrp2 30068 |
. . . . . . . . . . . . . . . . . . . 20
⊢
ℝ+ = (0(,)+∞) |
71 | | ioossicc 12547 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(0(,)+∞) ⊆ (0[,]+∞) |
72 | 70, 71 | eqsstri 3860 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℝ+ ⊆ (0[,]+∞) |
73 | 72, 64 | sseldi 3825 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
74 | 73 | adantl3r 756 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
75 | 69, 74 | xrge0addcld 30063 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
76 | 68, 75 | eqeltrrd 2907 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
77 | 53, 54 | sseldi 3825 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℝ) |
78 | 77 | adantl3r 756 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℝ) |
79 | 53, 62 | sseldi 3825 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℝ) |
80 | 79 | adantlr 706 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℝ) |
81 | 80 | adantl3r 756 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℝ) |
82 | | simplr 785 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℝ+) |
83 | 82 | rpgt0d 12159 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 0 < 𝑒) |
84 | | 2re 11425 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℝ |
85 | 84 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 2 ∈ ℝ) |
86 | 61 | adantllr 710 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℤ) |
87 | 86 | adantlr 706 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℤ) |
88 | | 2pos 11461 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 <
2 |
89 | 88 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 0 < 2) |
90 | | expgt0 13187 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℝ ∧ (𝑓‘𝑦) ∈ ℤ ∧ 0 < 2) → 0
< (2↑(𝑓‘𝑦))) |
91 | 85, 87, 89, 90 | syl3anc 1494 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 0 < (2↑(𝑓‘𝑦))) |
92 | 78, 81, 83, 91 | divgt0d 11289 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 0 < (𝑒 / (2↑(𝑓‘𝑦)))) |
93 | 66, 52 | ltaddposd 10936 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (0 < (𝑒 / (2↑(𝑓‘𝑦))) ↔ (𝑀‘𝐴) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
94 | 92, 93 | mpbid 224 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
95 | 29 | fveq1i 6434 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀‘𝐴) = ((toOMeas‘𝑅)‘𝐴) |
96 | 26 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑄 ∈ 𝑉) |
97 | 27 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑅:𝑄⟶(0[,]+∞)) |
98 | | omsfval 30890 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
→ ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
99 | 96, 97, 34, 98 | syl3anc 1494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
100 | 95, 99 | syl5eq 2873 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
101 | 9, 100 | sylan 575 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
102 | 101 | eqcomd 2831 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) = (𝑀‘𝐴)) |
103 | 102 | breq1d 4883 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ (𝑀‘𝐴) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
104 | 94, 103 | mpbird 249 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
105 | 76, 104 | jca 507 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞) ∧ inf(ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
106 | | iccssxr 12544 |
. . . . . . . . . . . . . . . . . . 19
⊢
(0[,]+∞) ⊆ ℝ* |
107 | | xrltso 12260 |
. . . . . . . . . . . . . . . . . . 19
⊢ < Or
ℝ* |
108 | | soss 5281 |
. . . . . . . . . . . . . . . . . . 19
⊢
((0[,]+∞) ⊆ ℝ* → ( < Or
ℝ* → < Or (0[,]+∞))) |
109 | 106, 107,
108 | mp2 9 |
. . . . . . . . . . . . . . . . . 18
⊢ < Or
(0[,]+∞) |
110 | | biid 253 |
. . . . . . . . . . . . . . . . . 18
⊢ ( < Or
(0[,]+∞) ↔ < Or (0[,]+∞)) |
111 | 109, 110 | mpbi 222 |
. . . . . . . . . . . . . . . . 17
⊢ < Or
(0[,]+∞) |
112 | 111 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → < Or
(0[,]+∞)) |
113 | | omscl 30891 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ∈ 𝒫 ∪ dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞)) |
114 | 96, 97, 46, 113 | syl3anc 1494 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞)) |
115 | | xrge0infss 30061 |
. . . . . . . . . . . . . . . . 17
⊢ (ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞) → ∃𝑣 ∈
(0[,]+∞)(∀ℎ
∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ¬ ℎ < 𝑣 ∧ ∀ℎ ∈ (0[,]+∞)(𝑣 < ℎ → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ℎ))) |
116 | 114, 115 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∃𝑣 ∈ (0[,]+∞)(∀ℎ ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ¬ ℎ < 𝑣 ∧ ∀ℎ ∈ (0[,]+∞)(𝑣 < ℎ → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ℎ))) |
117 | 112, 116 | infglb 8665 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ((((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞) ∧ inf(ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
118 | 117 | imp 397 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞) ∧ inf(ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
119 | 23, 24, 105, 118 | syl21anc 871 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
120 | | eqid 2825 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) |
121 | | esumex 30625 |
. . . . . . . . . . . . . . . . . . 19
⊢
Σ*𝑤
∈ 𝑥(𝑅‘𝑤) ∈ V |
122 | 120, 121 | elrnmpti 5609 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) |
123 | 122 | anbi1i 617 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
124 | | r19.41v 3299 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑥 ∈
{𝑧 ∈ 𝒫 dom
𝑅 ∣ (𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
(𝑢 =
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
125 | 123, 124 | bitr4i 270 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
126 | 125 | exbii 1947 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ ∃𝑢∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
127 | | df-rex 3123 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑢 ∈ ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
128 | | rexcom4 3442 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑥 ∈
{𝑧 ∈ 𝒫 dom
𝑅 ∣ (𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ ∃𝑢∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
129 | 126, 127,
128 | 3bitr4i 295 |
. . . . . . . . . . . . . 14
⊢
(∃𝑢 ∈ ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
130 | | breq1 4876 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) → (𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
131 | | idd 24 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) → (Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
132 | 130, 131 | sylbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) → (𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
133 | 132 | imp 397 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
134 | 133 | exlimiv 2029 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
135 | 134 | reximi 3219 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
{𝑧 ∈ 𝒫 dom
𝑅 ∣ (𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
136 | 129, 135 | sylbi 209 |
. . . . . . . . . . . . 13
⊢
(∃𝑢 ∈ ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
137 | 119, 136 | syl 17 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
138 | | simpr 479 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)
→ 𝑧 ≼
ω) |
139 | 138 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝒫 dom 𝑅 → ((𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω) → 𝑧 ≼ ω)) |
140 | 139 | ss2rabi 3909 |
. . . . . . . . . . . . . 14
⊢ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} |
141 | | rexss 3894 |
. . . . . . . . . . . . . 14
⊢ ({𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
142 | 140, 141 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
{𝑧 ∈ 𝒫 dom
𝑅 ∣ (𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
143 | | unieq 4666 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝑥 → ∪ 𝑧 = ∪
𝑥) |
144 | 143 | sseq2d 3858 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑥 → (𝐴 ⊆ ∪ 𝑧 ↔ 𝐴 ⊆ ∪ 𝑥)) |
145 | | breq1 4876 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑥 → (𝑧 ≼ ω ↔ 𝑥 ≼ ω)) |
146 | 144, 145 | anbi12d 624 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑥 → ((𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω) ↔ (𝐴 ⊆ ∪ 𝑥 ∧ 𝑥 ≼ ω))) |
147 | 146 | elrab 3585 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↔ (𝑥 ∈ 𝒫 dom 𝑅 ∧ (𝐴 ⊆ ∪ 𝑥 ∧ 𝑥 ≼ ω))) |
148 | 147 | simprbi 492 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} → (𝐴 ⊆ ∪ 𝑥 ∧ 𝑥 ≼ ω)) |
149 | 148 | simpld 490 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} → 𝐴 ⊆ ∪ 𝑥) |
150 | 149 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} → 𝐴 ⊆ ∪ 𝑥)) |
151 | 150 | anim1d 604 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ((𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
152 | 151 | reximdv 3224 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
153 | 142, 152 | syl5bi 234 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
154 | 137, 153 | mpd 15 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
155 | 154 | ex 403 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑦 ∈ 𝑋 → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
156 | 22, 155 | ralrimi 3166 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
∀𝑦 ∈ 𝑋 ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
157 | | unieq 4666 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑔‘𝑦) → ∪ 𝑥 = ∪
(𝑔‘𝑦)) |
158 | 157 | sseq2d 3858 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑔‘𝑦) → (𝐴 ⊆ ∪ 𝑥 ↔ 𝐴 ⊆ ∪ (𝑔‘𝑦))) |
159 | | esumeq1 30630 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑔‘𝑦) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) = Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
160 | 159 | breq1d 4883 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑔‘𝑦) → (Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
161 | 158, 160 | anbi12d 624 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑔‘𝑦) → ((𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
162 | 161 | ac6sg 9625 |
. . . . . . . . . 10
⊢ (𝑋 ∈ V → (∀𝑦 ∈ 𝑋 ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))))) |
163 | 162 | imp 397 |
. . . . . . . . 9
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
164 | 12, 156, 163 | syl2anc 579 |
. . . . . . . 8
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
165 | 9 | ad2antrr 717 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝜑) |
166 | 38 | ralrimiva 3175 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅) |
167 | | iunss 4781 |
. . . . . . . . . . . . . . . . . 18
⊢ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅 ↔ ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅) |
168 | 166, 167 | sylibr 226 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅) |
169 | 43 | ralrimiva 3175 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑦 ∈ 𝑋 𝐴 ∈ V) |
170 | | iunexg 7404 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 𝐴 ∈ V) → ∪ 𝑦 ∈ 𝑋 𝐴 ∈ V) |
171 | 11, 169, 170 | syl2anc 579 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ∈ V) |
172 | | elpwg 4386 |
. . . . . . . . . . . . . . . . . 18
⊢ (∪ 𝑦 ∈ 𝑋 𝐴 ∈ V → (∪ 𝑦 ∈ 𝑋 𝐴 ∈ 𝒫 ∪ dom 𝑅 ↔ ∪
𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅)) |
173 | 171, 172 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (∪ 𝑦 ∈ 𝑋 𝐴 ∈ 𝒫 ∪ dom 𝑅 ↔ ∪
𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅)) |
174 | 168, 173 | mpbird 249 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ∈ 𝒫 ∪ dom 𝑅) |
175 | 32, 174 | ffvelrnd 6609 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ∈ (0[,]+∞)) |
176 | 106, 175 | sseldi 3825 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ∈
ℝ*) |
177 | 165, 176 | syl 17 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ∈
ℝ*) |
178 | | simplr 785 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
179 | 25 | ad4antr 724 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑋 ∈ V) |
180 | | fex 6745 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ 𝑋 ∈ V) → 𝑔 ∈ V) |
181 | 178, 179,
180 | syl2anc 579 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑔 ∈ V) |
182 | | rnexg 7359 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 ∈ V → ran 𝑔 ∈ V) |
183 | | uniexg 7215 |
. . . . . . . . . . . . . . . 16
⊢ (ran
𝑔 ∈ V → ∪ ran 𝑔 ∈ V) |
184 | 181, 182,
183 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪
ran 𝑔 ∈
V) |
185 | | simp-5l 805 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝜑) |
186 | 27 | ad2antrr 717 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑐 ∈ ∪ ran
𝑔) → 𝑅:𝑄⟶(0[,]+∞)) |
187 | | frn 6284 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
188 | | ssrab2 3912 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ⊆ 𝒫 dom 𝑅 |
189 | 187, 188 | syl6ss 3839 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ran 𝑔 ⊆ 𝒫 dom 𝑅) |
190 | 189 | unissd 4684 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∪ ran 𝑔 ⊆ ∪
𝒫 dom 𝑅) |
191 | | unipw 5139 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ∪ 𝒫 dom 𝑅 = dom 𝑅 |
192 | 190, 191 | syl6sseq 3876 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∪ ran 𝑔 ⊆ dom 𝑅) |
193 | 192 | adantl 475 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∪ ran 𝑔 ⊆ dom 𝑅) |
194 | 35 | adantr 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → dom 𝑅 = 𝑄) |
195 | 193, 194 | sseqtrd 3866 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∪ ran 𝑔 ⊆ 𝑄) |
196 | 195 | sselda 3827 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑐 ∈ ∪ ran
𝑔) → 𝑐 ∈ 𝑄) |
197 | 186, 196 | ffvelrnd 6609 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑐 ∈ ∪ ran
𝑔) → (𝑅‘𝑐) ∈ (0[,]+∞)) |
198 | 197 | ralrimiva 3175 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∀𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ (0[,]+∞)) |
199 | 185, 178,
198 | syl2anc 579 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ∈ (0[,]+∞)) |
200 | | nfcv 2969 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑐∪ ran 𝑔 |
201 | 200 | esumcl 30626 |
. . . . . . . . . . . . . . 15
⊢ ((∪ ran 𝑔 ∈ V ∧ ∀𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ∈ (0[,]+∞)) →
Σ*𝑐 ∈
∪ ran 𝑔(𝑅‘𝑐) ∈ (0[,]+∞)) |
202 | 184, 199,
201 | syl2anc 579 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ (0[,]+∞)) |
203 | 106, 202 | sseldi 3825 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈
ℝ*) |
204 | | simp-5r 807 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) |
205 | 204 | rexrd 10406 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈
ℝ*) |
206 | | simpllr 793 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑒 ∈ ℝ+) |
207 | 206 | rpxrd 12157 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑒 ∈ ℝ*) |
208 | 205, 207 | xaddcld 12419 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒) ∈
ℝ*) |
209 | 187 | ad2antlr 718 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
210 | | sstr 3835 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ⊆ 𝒫 dom 𝑅) → ran 𝑔 ⊆ 𝒫 dom 𝑅) |
211 | 188, 210 | mpan2 682 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ran 𝑔 ⊆ 𝒫 dom 𝑅) |
212 | | sspwuni 4832 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ran
𝑔 ⊆ 𝒫 dom
𝑅 ↔ ∪ ran 𝑔 ⊆ dom 𝑅) |
213 | 211, 212 | sylib 210 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∪ ran 𝑔 ⊆ dom 𝑅) |
214 | 209, 213 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪
ran 𝑔 ⊆ dom 𝑅) |
215 | | ffn 6278 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → 𝑔 Fn 𝑋) |
216 | 215 | ad2antlr 718 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑔 Fn 𝑋) |
217 | 165, 1 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑋 ≼ ω) |
218 | | fnct 9674 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑔 Fn 𝑋 ∧ 𝑋 ≼ ω) → 𝑔 ≼ ω) |
219 | | rnct 9662 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑔 ≼ ω → ran
𝑔 ≼
ω) |
220 | 218, 219 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑔 Fn 𝑋 ∧ 𝑋 ≼ ω) → ran 𝑔 ≼
ω) |
221 | | dfss3 3816 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ↔ ∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
222 | 221 | biimpi 208 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
223 | | breq1 4876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 = 𝑤 → (𝑧 ≼ ω ↔ 𝑤 ≼ ω)) |
224 | 223 | elrab 3585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ↔ (𝑤 ∈ 𝒫 dom 𝑅 ∧ 𝑤 ≼ ω)) |
225 | 224 | simprbi 492 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → 𝑤 ≼ ω) |
226 | 225 | ralimi 3161 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∀𝑤 ∈
ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω) |
227 | 222, 226 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω) |
228 | | unictb 9712 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ran
𝑔 ≼ ω ∧
∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω) → ∪ ran 𝑔 ≼ ω) |
229 | 220, 227,
228 | syl2an 589 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑔 Fn 𝑋 ∧ 𝑋 ≼ ω) ∧ ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∪ ran 𝑔 ≼ ω) |
230 | 216, 217,
209, 229 | syl21anc 871 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪
ran 𝑔 ≼
ω) |
231 | | ctex 8237 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (∪ ran 𝑔 ≼ ω → ∪ ran 𝑔 ∈ V) |
232 | | elpwg 4386 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (∪ ran 𝑔 ∈ V → (∪ ran 𝑔 ∈ 𝒫 dom 𝑅 ↔ ∪ ran
𝑔 ⊆ dom 𝑅)) |
233 | 230, 231,
232 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (∪
ran 𝑔 ∈ 𝒫 dom
𝑅 ↔ ∪ ran 𝑔 ⊆ dom 𝑅)) |
234 | 214, 233 | mpbird 249 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪
ran 𝑔 ∈ 𝒫 dom
𝑅) |
235 | | simpl 476 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → 𝐴 ⊆ ∪ (𝑔‘𝑦)) |
236 | 235 | ralimi 3161 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑦 ∈
𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ (𝑔‘𝑦)) |
237 | | fvssunirn 6462 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑔‘𝑦) ⊆ ∪ ran
𝑔 |
238 | 237 | unissi 4683 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ∪ (𝑔‘𝑦) ⊆ ∪ ∪ ran 𝑔 |
239 | | sstr 3835 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ ∪ (𝑔‘𝑦) ⊆ ∪ ∪ ran 𝑔) → 𝐴 ⊆ ∪ ∪ ran 𝑔) |
240 | 238, 239 | mpan2 682 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ⊆ ∪ (𝑔‘𝑦) → 𝐴 ⊆ ∪ ∪ ran 𝑔) |
241 | 240 | ralimi 3161 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∀𝑦 ∈
𝑋 𝐴 ⊆ ∪ (𝑔‘𝑦) → ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔) |
242 | | iunss 4781 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔 ↔ ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔) |
243 | 241, 242 | sylibr 226 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑦 ∈
𝑋 𝐴 ⊆ ∪ (𝑔‘𝑦) → ∪
𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔) |
244 | 236, 243 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑦 ∈
𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔) |
245 | 244 | adantl 475 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔) |
246 | 234, 245,
230 | jca32 511 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (∪
ran 𝑔 ∈ 𝒫 dom
𝑅 ∧ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔 ∧ ∪ ran 𝑔 ≼
ω))) |
247 | | unieq 4666 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = ∪
ran 𝑔 → ∪ 𝑧 =
∪ ∪ ran 𝑔) |
248 | 247 | sseq2d 3858 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = ∪
ran 𝑔 → (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ↔ ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔)) |
249 | | breq1 4876 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = ∪
ran 𝑔 → (𝑧 ≼ ω ↔ ∪ ran 𝑔 ≼ ω)) |
250 | 248, 249 | anbi12d 624 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = ∪
ran 𝑔 → ((∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω) ↔ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔 ∧ ∪ ran 𝑔 ≼
ω))) |
251 | 250 | elrab 3585 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∪ ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↔ (∪ ran 𝑔 ∈ 𝒫 dom 𝑅 ∧ (∪
𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔 ∧ ∪ ran 𝑔 ≼
ω))) |
252 | 246, 251 | sylibr 226 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪
ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}) |
253 | | fveq2 6433 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 = 𝑤 → (𝑅‘𝑐) = (𝑅‘𝑤)) |
254 | 253 | cbvesumv 30639 |
. . . . . . . . . . . . . . . . . 18
⊢
Σ*𝑐
∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ ∪ ran
𝑔(𝑅‘𝑤) |
255 | | esumeq1 30630 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = ∪
ran 𝑔 →
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) = Σ*𝑤 ∈ ∪ ran
𝑔(𝑅‘𝑤)) |
256 | 255 | rspceeqv 3544 |
. . . . . . . . . . . . . . . . . 18
⊢ ((∪ ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧
Σ*𝑐 ∈
∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ ∪ ran
𝑔(𝑅‘𝑤)) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) |
257 | 252, 254,
256 | sylancl 580 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) |
258 | | esumex 30625 |
. . . . . . . . . . . . . . . . . 18
⊢
Σ*𝑐
∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ V |
259 | | eqid 2825 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) |
260 | 259 | elrnmpt 5605 |
. . . . . . . . . . . . . . . . . 18
⊢
(Σ*𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ∈ V → (Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤))) |
261 | 258, 260 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(Σ*𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) |
262 | 257, 261 | sylibr 226 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))) |
263 | 111 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → < Or
(0[,]+∞)) |
264 | | omscl 30891 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ ∪ 𝑦 ∈ 𝑋 𝐴 ∈ 𝒫 ∪ dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞)) |
265 | 26, 27, 174, 264 | syl3anc 1494 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞)) |
266 | | xrge0infss 30061 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞) → ∃𝑒 ∈
(0[,]+∞)(∀𝑡
∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ¬ 𝑡 < 𝑒 ∧ ∀𝑡 ∈ (0[,]+∞)(𝑒 < 𝑡 → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < 𝑡))) |
267 | 265, 266 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∃𝑒 ∈ (0[,]+∞)(∀𝑡 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ¬ 𝑡 < 𝑒 ∧ ∀𝑡 ∈ (0[,]+∞)(𝑒 < 𝑡 → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < 𝑡))) |
268 | 263, 267 | inflb 8664 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) → ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ))) |
269 | 29 | fveq1i 6434 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) = ((toOMeas‘𝑅)‘∪
𝑦 ∈ 𝑋 𝐴) |
270 | 168, 36 | sseqtrd 3866 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑄) |
271 | | omsfval 30890 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑄) → ((toOMeas‘𝑅)‘∪ 𝑦 ∈ 𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
272 | 26, 27, 270, 271 | syl3anc 1494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((toOMeas‘𝑅)‘∪ 𝑦 ∈ 𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
273 | 269, 272 | syl5eq 2873 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
274 | 273 | breq2d 4885 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ↔ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ))) |
275 | 274 | notbid 310 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (¬
Σ*𝑐 ∈
∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ↔ ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ))) |
276 | 268, 275 | sylibrd 251 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) → ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴))) |
277 | 165, 262,
276 | sylc 65 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴)) |
278 | | biid 253 |
. . . . . . . . . . . . . . 15
⊢ (¬
Σ*𝑐 ∈
∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ↔ ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴)) |
279 | 277, 278 | sylib 210 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴)) |
280 | | xrlenlt 10422 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ∈ ℝ* ∧
Σ*𝑐 ∈
∪ ran 𝑔(𝑅‘𝑐) ∈ ℝ*) → ((𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ↔ ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴))) |
281 | 177, 203,
280 | syl2anc 579 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ((𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ↔ ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴))) |
282 | 279, 281 | mpbird 249 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐)) |
283 | | nfv 2013 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑦 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} |
284 | 22, 283 | nfan 2002 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑦((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
285 | | nfra1 3150 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑦∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
286 | 284, 285 | nfan 2002 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑦(((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
287 | | simp-6l 809 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → 𝜑) |
288 | | simpllr 793 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
289 | | simpr 479 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
290 | 27 | ad3antrrr 721 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑅:𝑄⟶(0[,]+∞)) |
291 | | simpllr 793 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
292 | | simplr 785 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑦 ∈ 𝑋) |
293 | 291, 292 | ffvelrnd 6609 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
294 | 188, 293 | sseldi 3825 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ∈ 𝒫 dom 𝑅) |
295 | 294 | elpwid 4390 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ⊆ dom 𝑅) |
296 | 290, 295 | fssdmd 6293 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ⊆ 𝑄) |
297 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑤 ∈ (𝑔‘𝑦)) |
298 | 296, 297 | sseldd 3828 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑤 ∈ 𝑄) |
299 | 290, 298 | ffvelrnd 6609 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑅‘𝑤) ∈ (0[,]+∞)) |
300 | 299 | ralrimiva 3175 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → ∀𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
301 | | fvex 6446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔‘𝑦) ∈ V |
302 | | nfcv 2969 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑤(𝑔‘𝑦) |
303 | 302 | esumcl 30626 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑔‘𝑦) ∈ V ∧ ∀𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) →
Σ*𝑤 ∈
(𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
304 | 301, 303 | mpan 681 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑤 ∈
(𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞) →
Σ*𝑤 ∈
(𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
305 | 300, 304 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
306 | 287, 288,
289, 305 | syl21anc 871 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
307 | 306 | ex 403 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑦 ∈ 𝑋 → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞))) |
308 | 286, 307 | ralrimi 3166 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
309 | 14 | esumcl 30626 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) →
Σ*𝑦 ∈
𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
310 | 179, 308,
309 | syl2anc 579 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
311 | 106, 310 | sseldi 3825 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈
ℝ*) |
312 | | nfv 2013 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑤(𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
313 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
314 | | fniunfv 6760 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 Fn 𝑋 → ∪
𝑦 ∈ 𝑋 (𝑔‘𝑦) = ∪ ran 𝑔) |
315 | 313, 215,
314 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∪ 𝑦 ∈ 𝑋 (𝑔‘𝑦) = ∪ ran 𝑔) |
316 | 312, 315 | esumeq1d 30631 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) →
Σ*𝑤 ∈
∪ 𝑦 ∈ 𝑋 (𝑔‘𝑦)(𝑅‘𝑤) = Σ*𝑤 ∈ ∪ ran
𝑔(𝑅‘𝑤)) |
317 | 11 | adantr 474 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → 𝑋 ∈ V) |
318 | 301 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑔‘𝑦) ∈ V) |
319 | 317, 318,
299 | esumiun 30690 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) →
Σ*𝑤 ∈
∪ 𝑦 ∈ 𝑋 (𝑔‘𝑦)(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
320 | 316, 319 | eqbrtrrd 4897 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) →
Σ*𝑤 ∈
∪ ran 𝑔(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
321 | 9, 320 | sylan 575 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) →
Σ*𝑤 ∈
∪ ran 𝑔(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
322 | 321 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑤 ∈ ∪ ran 𝑔(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
323 | 254, 322 | syl5eqbr 4908 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
324 | 287, 289,
47 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞)) |
325 | | simplll 791 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈
ℝ+)) |
326 | 325, 289,
74 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
327 | 324, 326 | xrge0addcld 30063 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
328 | 327 | ex 403 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑦 ∈ 𝑋 → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞))) |
329 | 286, 328 | ralrimi 3166 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
330 | 14 | esumcl 30626 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) →
Σ*𝑦 ∈
𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
331 | 179, 329,
330 | syl2anc 579 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
332 | 106, 331 | sseldi 3825 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈
ℝ*) |
333 | 217, 10 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑋 ∈ V) |
334 | | simp-4l 801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ)) |
335 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
336 | 334, 335,
50 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ ℝ) |
337 | 336 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → (𝑀‘𝐴) ∈ ℝ) |
338 | 66 | adantlr 706 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
339 | 338 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
340 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
341 | 340 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
342 | 67 | breq2d 4885 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑀‘𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) →
(Σ*𝑤
∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ↔ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
343 | 342 | biimpar 471 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑀‘𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) ∧
Σ*𝑤 ∈
(𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) |
344 | 337, 339,
341, 343 | syl21anc 871 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) |
345 | 344 | ex 403 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
346 | 334 | simpld 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → 𝜑) |
347 | | simplr 785 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
348 | 346, 347,
335, 305 | syl21anc 871 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
349 | 106, 348 | sseldi 3825 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈
ℝ*) |
350 | 336 | rexrd 10406 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈
ℝ*) |
351 | 338 | rexrd 10406 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈
ℝ*) |
352 | 350, 351 | xaddcld 12419 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈
ℝ*) |
353 | | xrltle 12268 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ ℝ* ∧ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ ℝ*) →
(Σ*𝑤
∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
354 | 349, 352,
353 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
355 | 345, 354 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
356 | 355 | adantld 486 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
357 | 356 | ex 403 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → (𝑦 ∈ 𝑋 → ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))))) |
358 | 284, 357 | ralrimi 3166 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∀𝑦 ∈ 𝑋 ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
359 | | ralim 3157 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑦 ∈
𝑋 ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) → (∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
360 | 358, 359 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → (∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
361 | 360 | imp 397 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) |
362 | 361 | r19.21bi 3141 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) |
363 | 286, 14, 333, 306, 327, 362 | esumlef 30658 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) |
364 | 165, 47 | sylan 575 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞)) |
365 | 286, 14, 333, 364, 326 | esumaddf 30657 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) = (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦))))) |
366 | 326 | ex 403 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑦 ∈ 𝑋 → (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞))) |
367 | 286, 366 | ralrimi 3166 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
368 | 14 | esumcl 30626 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) →
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
369 | 179, 367,
368 | syl2anc 579 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
370 | 106, 369 | sseldi 3825 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈
ℝ*) |
371 | | simp-4r 803 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑓:𝑋–1-1→ℕ) |
372 | | vex 3417 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑓 ∈ V |
373 | 372 | rnex 7362 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ran 𝑓 ∈ V |
374 | 373 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ran 𝑓 ∈ V) |
375 | 59 | frnd 6285 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → ran 𝑓 ⊆ ℕ) |
376 | 375 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ran 𝑓 ⊆
ℕ) |
377 | 376 | sselda 3827 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ ℕ) |
378 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 2 ∈
ℝ+) |
379 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 𝑧 ∈ ℕ) |
380 | 379 | nnzd 11809 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 𝑧 ∈ ℤ) |
381 | 378, 380 | rpexpcld 13328 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (2↑𝑧) ∈
ℝ+) |
382 | 381 | rpreccld 12166 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈
ℝ+) |
383 | 72, 382 | sseldi 3825 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈
(0[,]+∞)) |
384 | 383 | adantlr 706 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ℕ) → (1 /
(2↑𝑧)) ∈
(0[,]+∞)) |
385 | 377, 384 | syldan 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ran 𝑓) → (1 / (2↑𝑧)) ∈ (0[,]+∞)) |
386 | 385 | ralrimiva 3175 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
∀𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞)) |
387 | | nfcv 2969 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑧ran
𝑓 |
388 | 387 | esumcl 30626 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ran
𝑓 ∈ V ∧
∀𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞)) →
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)) ∈
(0[,]+∞)) |
389 | 374, 386,
388 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)) ∈
(0[,]+∞)) |
390 | 106, 389 | sseldi 3825 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)) ∈
ℝ*) |
391 | | 1xr 10416 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℝ* |
392 | 391 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 1 ∈
ℝ*) |
393 | 72 | sseli 3823 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑒 ∈ ℝ+
→ 𝑒 ∈
(0[,]+∞)) |
394 | 393 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈
(0[,]+∞)) |
395 | | elxrge0 12571 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑒 ∈ (0[,]+∞) ↔
(𝑒 ∈
ℝ* ∧ 0 ≤ 𝑒)) |
396 | 394, 395 | sylib 210 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ∈ ℝ*
∧ 0 ≤ 𝑒)) |
397 | | nfv 2013 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑧(𝜑 ∧ 𝑓:𝑋–1-1→ℕ) |
398 | | nnex 11357 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ℕ
∈ V |
399 | 398 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → ℕ ∈
V) |
400 | 397, 399,
383, 375 | esummono 30650 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ Σ*𝑧 ∈ ℕ(1 / (2↑𝑧))) |
401 | | oveq2 6913 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = 𝑤 → (2↑𝑧) = (2↑𝑤)) |
402 | 401 | oveq2d 6921 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = 𝑤 → (1 / (2↑𝑧)) = (1 / (2↑𝑤))) |
403 | | ioossico 12551 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(0(,)+∞) ⊆ (0[,)+∞) |
404 | 70, 403 | eqsstri 3860 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
ℝ+ ⊆ (0[,)+∞) |
405 | 404, 382 | sseldi 3825 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈
(0[,)+∞)) |
406 | | eqidd 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ ℕ → (𝑤 ∈ ℕ ↦ (1 /
(2↑𝑤))) = (𝑤 ∈ ℕ ↦ (1 /
(2↑𝑤)))) |
407 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → 𝑤 = 𝑧) |
408 | 407 | oveq2d 6921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → (2↑𝑤) = (2↑𝑧)) |
409 | 408 | oveq2d 6921 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → (1 / (2↑𝑤)) = (1 / (2↑𝑧))) |
410 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℕ) |
411 | | ovexd 6939 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ ℕ → (1 /
(2↑𝑧)) ∈
V) |
412 | 406, 409,
410, 411 | fvmptd 6535 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 ∈ ℕ → ((𝑤 ∈ ℕ ↦ (1 /
(2↑𝑤)))‘𝑧) = (1 / (2↑𝑧))) |
413 | 412 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → ((𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))‘𝑧) = (1 / (2↑𝑧))) |
414 | | ax-1cn 10310 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 1 ∈
ℂ |
415 | | eqid 2825 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ ℕ ↦ (1 /
(2↑𝑤))) = (𝑤 ∈ ℕ ↦ (1 /
(2↑𝑤))) |
416 | 415 | geo2lim 14980 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (1 ∈
ℂ → seq1( + , (𝑤
∈ ℕ ↦ (1 / (2↑𝑤)))) ⇝ 1) |
417 | 414, 416 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ seq1( + ,
(𝑤 ∈ ℕ ↦
(1 / (2↑𝑤)))) ⇝
1 |
418 | 417 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → seq1( + , (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))) ⇝ 1) |
419 | | 1re 10356 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 ∈
ℝ |
420 | 419 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → 1 ∈
ℝ) |
421 | 402, 405,
413, 418, 420 | esumcvgsum 30684 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ℕ(1 /
(2↑𝑧)) = Σ𝑧 ∈ ℕ (1 /
(2↑𝑧))) |
422 | | geoihalfsum 14987 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Σ𝑧 ∈
ℕ (1 / (2↑𝑧)) =
1 |
423 | 421, 422 | syl6eq 2877 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ℕ(1 /
(2↑𝑧)) =
1) |
424 | 400, 423 | breqtrd 4899 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1) |
425 | 424 | adantr 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)) ≤ 1) |
426 | | xlemul2a 12407 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ ℝ* ∧ 1 ∈
ℝ* ∧ (𝑒 ∈ ℝ* ∧ 0 ≤
𝑒)) ∧
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)) ≤ 1) → (𝑒 ·e
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧))) ≤ (𝑒 ·e 1)) |
427 | 390, 392,
396, 425, 426 | syl31anc 1496 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧))) ≤ (𝑒 ·e 1)) |
428 | 13, 19 | nfan 2002 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑦(𝜑 ∧ 𝑓:𝑋–1-1→ℕ) |
429 | 428, 21 | nfan 2002 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑦((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) |
430 | 77 | recnd 10385 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℂ) |
431 | 79 | recnd 10385 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℂ) |
432 | 431 | adantlr 706 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℂ) |
433 | | 2cn 11426 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 2 ∈
ℂ |
434 | 433 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → 2 ∈ ℂ) |
435 | | 2ne0 11462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 2 ≠
0 |
436 | 435 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → 2 ≠ 0) |
437 | 434, 436,
61 | expne0d 13308 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ≠ 0) |
438 | 437 | adantlr 706 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ≠ 0) |
439 | 430, 432,
438 | divrecd 11130 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) = (𝑒 · (1 / (2↑(𝑓‘𝑦))))) |
440 | | 1rp 12116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 1 ∈
ℝ+ |
441 | 440 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → 1 ∈
ℝ+) |
442 | 441, 62 | rpdivcld 12173 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈
ℝ+) |
443 | 53, 442 | sseldi 3825 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
444 | 443 | adantlr 706 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
445 | | rexmul 12389 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑒 ∈ ℝ ∧ (1 /
(2↑(𝑓‘𝑦))) ∈ ℝ) →
(𝑒 ·e (1
/ (2↑(𝑓‘𝑦)))) = (𝑒 · (1 / (2↑(𝑓‘𝑦))))) |
446 | 77, 444, 445 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 ·e (1 / (2↑(𝑓‘𝑦)))) = (𝑒 · (1 / (2↑(𝑓‘𝑦))))) |
447 | 439, 446 | eqtr4d 2864 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) = (𝑒 ·e (1 / (2↑(𝑓‘𝑦))))) |
448 | 447 | ralrimiva 3175 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
∀𝑦 ∈ 𝑋 (𝑒 / (2↑(𝑓‘𝑦))) = (𝑒 ·e (1 / (2↑(𝑓‘𝑦))))) |
449 | 429, 448 | esumeq2d 30633 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦))) = Σ*𝑦 ∈ 𝑋(𝑒 ·e (1 / (2↑(𝑓‘𝑦))))) |
450 | 11 | ad2antrr 717 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑋 ∈ V) |
451 | 72, 442 | sseldi 3825 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
452 | 451 | adantlr 706 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
453 | 404 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → ℝ+ ⊆
(0[,)+∞)) |
454 | 453 | sselda 3827 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈
(0[,)+∞)) |
455 | 450, 452,
454 | esummulc2 30678 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e
Σ*𝑦 ∈
𝑋(1 / (2↑(𝑓‘𝑦)))) = Σ*𝑦 ∈ 𝑋(𝑒 ·e (1 / (2↑(𝑓‘𝑦))))) |
456 | | nfcv 2969 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑦(1 /
(2↑𝑧)) |
457 | | oveq2 6913 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = (𝑓‘𝑦) → (2↑𝑧) = (2↑(𝑓‘𝑦))) |
458 | 457 | oveq2d 6921 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = (𝑓‘𝑦) → (1 / (2↑𝑧)) = (1 / (2↑(𝑓‘𝑦)))) |
459 | 11 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → 𝑋 ∈ V) |
460 | 57 | simprbi 492 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓:𝑋–1-1→ℕ → Fun ◡𝑓) |
461 | 58 | feqmptd 6496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓:𝑋–1-1→ℕ → 𝑓 = (𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦))) |
462 | 461 | cnveqd 5530 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓:𝑋–1-1→ℕ → ◡𝑓 = ◡(𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦))) |
463 | 462 | funeqd 6145 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓:𝑋–1-1→ℕ → (Fun ◡𝑓 ↔ Fun ◡(𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦)))) |
464 | 460, 463 | mpbid 224 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓:𝑋–1-1→ℕ → Fun ◡(𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦))) |
465 | 464 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Fun ◡(𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦))) |
466 | 456, 428,
14, 458, 459, 465, 451, 60 | esumc 30647 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑦 ∈ 𝑋(1 / (2↑(𝑓‘𝑦))) = Σ*𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)} (1 / (2↑𝑧))) |
467 | | ffn 6278 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓:𝑋⟶ℕ → 𝑓 Fn 𝑋) |
468 | | fnrnfv 6489 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 Fn 𝑋 → ran 𝑓 = {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)}) |
469 | 59, 467, 468 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → ran 𝑓 = {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)}) |
470 | 397, 469 | esumeq1d 30631 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) = Σ*𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)} (1 / (2↑𝑧))) |
471 | 466, 470 | eqtr4d 2864 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑦 ∈ 𝑋(1 / (2↑(𝑓‘𝑦))) = Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) |
472 | 471 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑦 ∈
𝑋(1 / (2↑(𝑓‘𝑦))) = Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) |
473 | 472 | oveq2d 6921 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e
Σ*𝑦 ∈
𝑋(1 / (2↑(𝑓‘𝑦)))) = (𝑒 ·e
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)))) |
474 | 449, 455,
473 | 3eqtr2rd 2868 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧))) = Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦)))) |
475 | 396 | simpld 490 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈
ℝ*) |
476 | | xmulid1 12397 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑒 ∈ ℝ*
→ (𝑒
·e 1) = 𝑒) |
477 | 475, 476 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e 1) = 𝑒) |
478 | 427, 474,
477 | 3brtr3d 4904 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦))) ≤ 𝑒) |
479 | 165, 371,
206, 478 | syl21anc 871 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ≤ 𝑒) |
480 | | xleadd2a 12372 |
. . . . . . . . . . . . . . . . 17
⊢
(((Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ* ∧ 𝑒 ∈ ℝ*
∧ Σ*𝑦
∈ 𝑋(𝑀‘𝐴) ∈ ℝ*) ∧
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦))) ≤ 𝑒) → (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦)))) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
481 | 370, 207,
205, 479, 480 | syl31anc 1496 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦)))) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
482 | 365, 481 | eqbrtrd 4895 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
483 | 311, 332,
208, 363, 482 | xrletrd 12281 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
484 | 203, 311,
208, 323, 483 | xrletrd 12281 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
485 | 177, 203,
208, 282, 484 | xrletrd 12281 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
486 | 206 | rpred 12156 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑒 ∈ ℝ) |
487 | | rexadd 12351 |
. . . . . . . . . . . . 13
⊢
((Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ ∧ 𝑒 ∈ ℝ) →
(Σ*𝑦
∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒) = (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
488 | 204, 486,
487 | syl2anc 579 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒) = (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
489 | 485, 488 | breqtrd 4899 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
490 | 489 | anasss 460 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
491 | 490 | ex 403 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ((𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))) |
492 | 491 | exlimdv 2032 |
. . . . . . . 8
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
(∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))) |
493 | 164, 492 | mpd 15 |
. . . . . . 7
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
494 | 493 | ralrimiva 3175 |
. . . . . 6
⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) → ∀𝑒 ∈ ℝ+ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
495 | | xralrple 12324 |
. . . . . . . 8
⊢ (((𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ∈ ℝ* ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) → ((𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))) |
496 | 176, 495 | sylan 575 |
. . . . . . 7
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → ((𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))) |
497 | 496 | adantr 474 |
. . . . . 6
⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) → ((𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))) |
498 | 494, 497 | mpbird 249 |
. . . . 5
⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴)) |
499 | 498 | ex 403 |
. . . 4
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑓:𝑋–1-1→ℕ → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴))) |
500 | 499 | exlimdv 2032 |
. . 3
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → (∃𝑓 𝑓:𝑋–1-1→ℕ → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴))) |
501 | 8, 500 | mpd 15 |
. 2
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴)) |
502 | 176 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ ¬
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ∈
ℝ*) |
503 | | pnfge 12250 |
. . . 4
⊢ ((𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ∈ ℝ* → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ +∞) |
504 | 502, 503 | syl 17 |
. . 3
⊢ ((𝜑 ∧ ¬
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ +∞) |
505 | 47 | ralrimiva 3175 |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ 𝑋 (𝑀‘𝐴) ∈ (0[,]+∞)) |
506 | 14 | esumcl 30626 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 (𝑀‘𝐴) ∈ (0[,]+∞)) →
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ (0[,]+∞)) |
507 | 11, 505, 506 | syl2anc 579 |
. . . 4
⊢ (𝜑 → Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ (0[,]+∞)) |
508 | | xrge0nre 12567 |
. . . 4
⊢
((Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ (0[,]+∞) ∧ ¬
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) →
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) = +∞) |
509 | 507, 508 | sylan 575 |
. . 3
⊢ ((𝜑 ∧ ¬
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) →
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) = +∞) |
510 | 504, 509 | breqtrrd 4901 |
. 2
⊢ ((𝜑 ∧ ¬
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴)) |
511 | 501, 510 | pm2.61dan 847 |
1
⊢ (𝜑 → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴)) |