| Step | Hyp | Ref
| Expression |
| 1 | | omssubadd.b |
. . . . . 6
⊢ (𝜑 → 𝑋 ≼ ω) |
| 2 | | nnenom 14021 |
. . . . . . 7
⊢ ℕ
≈ ω |
| 3 | 2 | ensymi 9044 |
. . . . . 6
⊢ ω
≈ ℕ |
| 4 | | domentr 9053 |
. . . . . 6
⊢ ((𝑋 ≼ ω ∧ ω
≈ ℕ) → 𝑋
≼ ℕ) |
| 5 | 1, 3, 4 | sylancl 586 |
. . . . 5
⊢ (𝜑 → 𝑋 ≼ ℕ) |
| 6 | | brdomi 8999 |
. . . . 5
⊢ (𝑋 ≼ ℕ →
∃𝑓 𝑓:𝑋–1-1→ℕ) |
| 7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝜑 → ∃𝑓 𝑓:𝑋–1-1→ℕ) |
| 8 | 7 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → ∃𝑓 𝑓:𝑋–1-1→ℕ) |
| 9 | | simplll 775 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝜑) |
| 10 | | ctex 9004 |
. . . . . . . . . . 11
⊢ (𝑋 ≼ ω → 𝑋 ∈ V) |
| 11 | 1, 10 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ V) |
| 12 | 9, 11 | syl 17 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑋 ∈ V) |
| 13 | | nfv 1914 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦𝜑 |
| 14 | | nfcv 2905 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦𝑋 |
| 15 | 14 | nfesum1 34041 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) |
| 16 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦ℝ |
| 17 | 15, 16 | nfel 2920 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ |
| 18 | 13, 17 | nfan 1899 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) |
| 19 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦 𝑓:𝑋–1-1→ℕ |
| 20 | 18, 19 | nfan 1899 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) |
| 21 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 𝑒 ∈
ℝ+ |
| 22 | 20, 21 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) |
| 23 | 9 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝜑) |
| 24 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
| 25 | 11 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → 𝑋 ∈ V) |
| 26 | | oms.o |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑄 ∈ 𝑉) |
| 27 | | oms.r |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑅:𝑄⟶(0[,]+∞)) |
| 28 | | omsf 34298 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞)) →
(toOMeas‘𝑅):𝒫
∪ dom 𝑅⟶(0[,]+∞)) |
| 29 | | oms.m |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑀 = (toOMeas‘𝑅) |
| 30 | 29 | feq1i 6727 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑀:𝒫 ∪ dom 𝑅⟶(0[,]+∞) ↔
(toOMeas‘𝑅):𝒫
∪ dom 𝑅⟶(0[,]+∞)) |
| 31 | 28, 30 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞)) → 𝑀:𝒫 ∪ dom 𝑅⟶(0[,]+∞)) |
| 32 | 26, 27, 31 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑀:𝒫 ∪ dom
𝑅⟶(0[,]+∞)) |
| 33 | 32 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑀:𝒫 ∪ dom
𝑅⟶(0[,]+∞)) |
| 34 | | omssubadd.a |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ⊆ ∪ 𝑄) |
| 35 | 27 | fdmd 6746 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → dom 𝑅 = 𝑄) |
| 36 | 35 | unieqd 4920 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ∪ dom 𝑅 = ∪ 𝑄) |
| 37 | 36 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∪ dom
𝑅 = ∪ 𝑄) |
| 38 | 34, 37 | sseqtrrd 4021 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ⊆ ∪ dom
𝑅) |
| 39 | 26 | uniexd 7762 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ∪ 𝑄
∈ V) |
| 40 | 39 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ∪ 𝑄 ∈ V) |
| 41 | | ssexg 5323 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ⊆ ∪ 𝑄
∧ ∪ 𝑄 ∈ V) → 𝐴 ∈ V) |
| 42 | 34, 40, 41 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ∈ V) |
| 43 | | elpwg 4603 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 ∪ dom 𝑅 ↔ 𝐴 ⊆ ∪ dom
𝑅)) |
| 44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐴 ∈ 𝒫 ∪ dom 𝑅 ↔ 𝐴 ⊆ ∪ dom
𝑅)) |
| 45 | 38, 44 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐴 ∈ 𝒫 ∪ dom 𝑅) |
| 46 | 33, 45 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞)) |
| 47 | 46 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞)) |
| 48 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) →
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) |
| 49 | 18, 25, 47, 48 | esumcvgre 34092 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ ℝ) |
| 50 | 49 | adantlr 715 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ ℝ) |
| 51 | 50 | adantlr 715 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ ℝ) |
| 52 | | rpssre 13042 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℝ+ ⊆ ℝ |
| 53 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℝ+) |
| 54 | | 2rp 13039 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℝ+ |
| 55 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → 2 ∈
ℝ+) |
| 56 | | df-f1 6566 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓:𝑋–1-1→ℕ ↔ (𝑓:𝑋⟶ℕ ∧ Fun ◡𝑓)) |
| 57 | 56 | simplbi 497 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓:𝑋–1-1→ℕ → 𝑓:𝑋⟶ℕ) |
| 58 | 57 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → 𝑓:𝑋⟶ℕ) |
| 59 | 58 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℕ) |
| 60 | 59 | nnzd 12640 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℤ) |
| 61 | 55, 60 | rpexpcld 14286 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈
ℝ+) |
| 62 | 61 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈
ℝ+) |
| 63 | 53, 62 | rpdivcld 13094 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈
ℝ+) |
| 64 | 52, 63 | sselid 3981 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
| 65 | 64 | adantl3r 750 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
| 66 | | rexadd 13274 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀‘𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) = ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
| 67 | 51, 65, 66 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) = ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
| 68 | 9, 46 | sylan 580 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞)) |
| 69 | | dfrp2 13436 |
. . . . . . . . . . . . . . . . . . . 20
⊢
ℝ+ = (0(,)+∞) |
| 70 | | ioossicc 13473 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(0(,)+∞) ⊆ (0[,]+∞) |
| 71 | 69, 70 | eqsstri 4030 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℝ+ ⊆ (0[,]+∞) |
| 72 | 71, 63 | sselid 3981 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
| 73 | 72 | adantl3r 750 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
| 74 | 68, 73 | xrge0addcld 32766 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
| 75 | 67, 74 | eqeltrrd 2842 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
| 76 | 52, 53 | sselid 3981 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℝ) |
| 77 | 76 | adantl3r 750 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℝ) |
| 78 | 52, 61 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℝ) |
| 79 | 78 | adantlr 715 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℝ) |
| 80 | 79 | adantl3r 750 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℝ) |
| 81 | | simplr 769 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℝ+) |
| 82 | 81 | rpgt0d 13080 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 0 < 𝑒) |
| 83 | | 2re 12340 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℝ |
| 84 | 83 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 2 ∈ ℝ) |
| 85 | 60 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℤ) |
| 86 | 85 | adantlr 715 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑓‘𝑦) ∈ ℤ) |
| 87 | | 2pos 12369 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 <
2 |
| 88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 0 < 2) |
| 89 | | expgt0 14136 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℝ ∧ (𝑓‘𝑦) ∈ ℤ ∧ 0 < 2) → 0
< (2↑(𝑓‘𝑦))) |
| 90 | 84, 86, 88, 89 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 0 < (2↑(𝑓‘𝑦))) |
| 91 | 77, 80, 82, 90 | divgt0d 12203 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 0 < (𝑒 / (2↑(𝑓‘𝑦)))) |
| 92 | 65, 51 | ltaddposd 11847 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (0 < (𝑒 / (2↑(𝑓‘𝑦))) ↔ (𝑀‘𝐴) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 93 | 91, 92 | mpbid 232 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
| 94 | 29 | fveq1i 6907 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀‘𝐴) = ((toOMeas‘𝑅)‘𝐴) |
| 95 | 26 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑄 ∈ 𝑉) |
| 96 | 27 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝑅:𝑄⟶(0[,]+∞)) |
| 97 | | omsfval 34296 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ⊆ ∪ 𝑄)
→ ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
| 98 | 95, 96, 34, 97 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ((toOMeas‘𝑅)‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
| 99 | 94, 98 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
| 100 | 9, 99 | sylan 580 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
| 101 | 100 | eqcomd 2743 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) = (𝑀‘𝐴)) |
| 102 | 101 | breq1d 5153 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ (𝑀‘𝐴) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 103 | 93, 102 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
| 104 | 75, 103 | jca 511 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞) ∧ inf(ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 105 | | iccssxr 13470 |
. . . . . . . . . . . . . . . . . . 19
⊢
(0[,]+∞) ⊆ ℝ* |
| 106 | | xrltso 13183 |
. . . . . . . . . . . . . . . . . . 19
⊢ < Or
ℝ* |
| 107 | | soss 5612 |
. . . . . . . . . . . . . . . . . . 19
⊢
((0[,]+∞) ⊆ ℝ* → ( < Or
ℝ* → < Or (0[,]+∞))) |
| 108 | 105, 106,
107 | mp2 9 |
. . . . . . . . . . . . . . . . . 18
⊢ < Or
(0[,]+∞) |
| 109 | | biid 261 |
. . . . . . . . . . . . . . . . . 18
⊢ ( < Or
(0[,]+∞) ↔ < Or (0[,]+∞)) |
| 110 | 108, 109 | mpbi 230 |
. . . . . . . . . . . . . . . . 17
⊢ < Or
(0[,]+∞) |
| 111 | 110 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → < Or
(0[,]+∞)) |
| 112 | | omscl 34297 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ 𝐴 ∈ 𝒫 ∪ dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞)) |
| 113 | 95, 96, 45, 112 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞)) |
| 114 | | xrge0infss 32764 |
. . . . . . . . . . . . . . . . 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 9530 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ((((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞) ∧ inf(ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 117 | 116 | imp 406 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ (((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞) ∧ inf(ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
| 118 | 23, 24, 104, 117 | syl21anc 838 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
| 119 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) |
| 120 | | esumex 34030 |
. . . . . . . . . . . . . . . . . . 19
⊢
Σ*𝑤
∈ 𝑥(𝑅‘𝑤) ∈ V |
| 121 | 119, 120 | elrnmpti 5973 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) |
| 122 | 121 | anbi1i 624 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 123 | | r19.41v 3189 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑥 ∈
{𝑧 ∈ 𝒫 dom
𝑅 ∣ (𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)}
(𝑢 =
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 124 | 122, 123 | bitr4i 278 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 125 | 124 | exbii 1848 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ ∃𝑢∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 126 | | df-rex 3071 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑢 ∈ ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑢(𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 127 | | rexcom4 3288 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑥 ∈
{𝑧 ∈ 𝒫 dom
𝑅 ∣ (𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ ∃𝑢∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 128 | 125, 126,
127 | 3bitr4i 303 |
. . . . . . . . . . . . . 14
⊢
(∃𝑢 ∈ ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 129 | | breq1 5146 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) → (𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 130 | | idd 24 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) → (Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 131 | 129, 130 | sylbid 240 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) → (𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 132 | 131 | imp 406 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
| 133 | 132 | exlimiv 1930 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
| 134 | 133 | reximi 3084 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
{𝑧 ∈ 𝒫 dom
𝑅 ∣ (𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}∃𝑢(𝑢 = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) ∧ 𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
| 135 | 128, 134 | sylbi 217 |
. . . . . . . . . . . . 13
⊢
(∃𝑢 ∈ ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
| 136 | 118, 135 | syl 17 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
| 137 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼ ω)
→ 𝑧 ≼
ω) |
| 138 | 137 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝒫 dom 𝑅 → ((𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω) → 𝑧 ≼ ω)) |
| 139 | 138 | ss2rabi 4077 |
. . . . . . . . . . . . . 14
⊢ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} |
| 140 | | rexss 4059 |
. . . . . . . . . . . . . 14
⊢ ({𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
| 141 | 139, 140 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
{𝑧 ∈ 𝒫 dom
𝑅 ∣ (𝐴 ⊆ ∪ 𝑧
∧ 𝑧 ≼
ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 142 | | unieq 4918 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝑥 → ∪ 𝑧 = ∪
𝑥) |
| 143 | 142 | sseq2d 4016 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑥 → (𝐴 ⊆ ∪ 𝑧 ↔ 𝐴 ⊆ ∪ 𝑥)) |
| 144 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑥 → (𝑧 ≼ ω ↔ 𝑥 ≼ ω)) |
| 145 | 143, 144 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑥 → ((𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω) ↔ (𝐴 ⊆ ∪ 𝑥 ∧ 𝑥 ≼ ω))) |
| 146 | 145 | elrab 3692 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↔ (𝑥 ∈ 𝒫 dom 𝑅 ∧ (𝐴 ⊆ ∪ 𝑥 ∧ 𝑥 ≼ ω))) |
| 147 | 146 | simprbi 496 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} → (𝐴 ⊆ ∪ 𝑥 ∧ 𝑥 ≼ ω)) |
| 148 | 147 | simpld 494 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} → 𝐴 ⊆ ∪ 𝑥) |
| 149 | 148 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} → 𝐴 ⊆ ∪ 𝑥)) |
| 150 | 149 | anim1d 611 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ((𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
| 151 | 150 | reximdv 3170 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
| 152 | 141, 151 | biimtrid 242 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
| 153 | 136, 152 | mpd 15 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 154 | 153 | ex 412 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑦 ∈ 𝑋 → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
| 155 | 22, 154 | ralrimi 3257 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
∀𝑦 ∈ 𝑋 ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 156 | | unieq 4918 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑔‘𝑦) → ∪ 𝑥 = ∪
(𝑔‘𝑦)) |
| 157 | 156 | sseq2d 4016 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑔‘𝑦) → (𝐴 ⊆ ∪ 𝑥 ↔ 𝐴 ⊆ ∪ (𝑔‘𝑦))) |
| 158 | | esumeq1 34035 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑔‘𝑦) → Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) = Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
| 159 | 158 | breq1d 5153 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑔‘𝑦) → (Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) ↔ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 160 | 157, 159 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑔‘𝑦) → ((𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) ↔ (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
| 161 | 160 | ac6sg 10528 |
. . . . . . . . . 10
⊢ (𝑋 ∈ V → (∀𝑦 ∈ 𝑋 ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))))) |
| 162 | 161 | imp 406 |
. . . . . . . . 9
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} (𝐴 ⊆ ∪ 𝑥 ∧ Σ*𝑤 ∈ 𝑥(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
| 163 | 12, 155, 162 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) |
| 164 | 9 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝜑) |
| 165 | 38 | ralrimiva 3146 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅) |
| 166 | | iunss 5045 |
. . . . . . . . . . . . . . . . . 18
⊢ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅 ↔ ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅) |
| 167 | 165, 166 | sylibr 234 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅) |
| 168 | 42 | ralrimiva 3146 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑦 ∈ 𝑋 𝐴 ∈ V) |
| 169 | | iunexg 7988 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 𝐴 ∈ V) → ∪ 𝑦 ∈ 𝑋 𝐴 ∈ V) |
| 170 | 11, 168, 169 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ∈ V) |
| 171 | | elpwg 4603 |
. . . . . . . . . . . . . . . . . 18
⊢ (∪ 𝑦 ∈ 𝑋 𝐴 ∈ V → (∪ 𝑦 ∈ 𝑋 𝐴 ∈ 𝒫 ∪ dom 𝑅 ↔ ∪
𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅)) |
| 172 | 170, 171 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (∪ 𝑦 ∈ 𝑋 𝐴 ∈ 𝒫 ∪ dom 𝑅 ↔ ∪
𝑦 ∈ 𝑋 𝐴 ⊆ ∪ dom
𝑅)) |
| 173 | 167, 172 | mpbird 257 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ∈ 𝒫 ∪ dom 𝑅) |
| 174 | 32, 173 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ∈ (0[,]+∞)) |
| 175 | 105, 174 | sselid 3981 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ∈
ℝ*) |
| 176 | 164, 175 | syl 17 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ∈
ℝ*) |
| 177 | | simplr 769 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
| 178 | 25 | ad4antr 732 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑋 ∈ V) |
| 179 | 177, 178 | fexd 7247 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑔 ∈ V) |
| 180 | | rnexg 7924 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 ∈ V → ran 𝑔 ∈ V) |
| 181 | | uniexg 7760 |
. . . . . . . . . . . . . . . 16
⊢ (ran
𝑔 ∈ V → ∪ ran 𝑔 ∈ V) |
| 182 | 179, 180,
181 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪
ran 𝑔 ∈
V) |
| 183 | | simp-5l 785 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝜑) |
| 184 | 27 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑐 ∈ ∪ ran
𝑔) → 𝑅:𝑄⟶(0[,]+∞)) |
| 185 | | frn 6743 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
| 186 | | ssrab2 4080 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ⊆ 𝒫 dom 𝑅 |
| 187 | 185, 186 | sstrdi 3996 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ran 𝑔 ⊆ 𝒫 dom 𝑅) |
| 188 | 187 | unissd 4917 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∪ ran 𝑔 ⊆ ∪
𝒫 dom 𝑅) |
| 189 | | unipw 5455 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ∪ 𝒫 dom 𝑅 = dom 𝑅 |
| 190 | 188, 189 | sseqtrdi 4024 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∪ ran 𝑔 ⊆ dom 𝑅) |
| 191 | 190 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∪ ran 𝑔 ⊆ dom 𝑅) |
| 192 | 35 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → dom 𝑅 = 𝑄) |
| 193 | 191, 192 | sseqtrd 4020 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∪ ran 𝑔 ⊆ 𝑄) |
| 194 | 193 | sselda 3983 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑐 ∈ ∪ ran
𝑔) → 𝑐 ∈ 𝑄) |
| 195 | 184, 194 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑐 ∈ ∪ ran
𝑔) → (𝑅‘𝑐) ∈ (0[,]+∞)) |
| 196 | 195 | ralrimiva 3146 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∀𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ (0[,]+∞)) |
| 197 | 183, 177,
196 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ∈ (0[,]+∞)) |
| 198 | | nfcv 2905 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑐∪ ran 𝑔 |
| 199 | 198 | esumcl 34031 |
. . . . . . . . . . . . . . 15
⊢ ((∪ ran 𝑔 ∈ V ∧ ∀𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ∈ (0[,]+∞)) →
Σ*𝑐 ∈
∪ ran 𝑔(𝑅‘𝑐) ∈ (0[,]+∞)) |
| 200 | 182, 197,
199 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ (0[,]+∞)) |
| 201 | 105, 200 | sselid 3981 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈
ℝ*) |
| 202 | | simp-5r 786 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) |
| 203 | 202 | rexrd 11311 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈
ℝ*) |
| 204 | | simpllr 776 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑒 ∈ ℝ+) |
| 205 | 204 | rpxrd 13078 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑒 ∈ ℝ*) |
| 206 | 203, 205 | xaddcld 13343 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒) ∈
ℝ*) |
| 207 | 185 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
| 208 | | sstr 3992 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ⊆ 𝒫 dom 𝑅) → ran 𝑔 ⊆ 𝒫 dom 𝑅) |
| 209 | 186, 208 | mpan2 691 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ran 𝑔 ⊆ 𝒫 dom 𝑅) |
| 210 | | sspwuni 5100 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ran
𝑔 ⊆ 𝒫 dom
𝑅 ↔ ∪ ran 𝑔 ⊆ dom 𝑅) |
| 211 | 209, 210 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∪ ran 𝑔 ⊆ dom 𝑅) |
| 212 | 207, 211 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪
ran 𝑔 ⊆ dom 𝑅) |
| 213 | | ffn 6736 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → 𝑔 Fn 𝑋) |
| 214 | 213 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑔 Fn 𝑋) |
| 215 | 164, 1 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑋 ≼ ω) |
| 216 | | fnct 10577 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑔 Fn 𝑋 ∧ 𝑋 ≼ ω) → 𝑔 ≼ ω) |
| 217 | | rnct 10565 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑔 ≼ ω → ran
𝑔 ≼
ω) |
| 218 | 216, 217 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑔 Fn 𝑋 ∧ 𝑋 ≼ ω) → ran 𝑔 ≼
ω) |
| 219 | | dfss3 3972 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ↔ ∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
| 220 | 219 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
| 221 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 = 𝑤 → (𝑧 ≼ ω ↔ 𝑤 ≼ ω)) |
| 222 | 221 | elrab 3692 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ↔ (𝑤 ∈ 𝒫 dom 𝑅 ∧ 𝑤 ≼ ω)) |
| 223 | 222 | simprbi 496 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → 𝑤 ≼ ω) |
| 224 | 223 | ralimi 3083 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∀𝑤 ∈
ran 𝑔 𝑤 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω) |
| 225 | 220, 224 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ran
𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} → ∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω) |
| 226 | | unictb 10615 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ran
𝑔 ≼ ω ∧
∀𝑤 ∈ ran 𝑔 𝑤 ≼ ω) → ∪ ran 𝑔 ≼ ω) |
| 227 | 218, 225,
226 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑔 Fn 𝑋 ∧ 𝑋 ≼ ω) ∧ ran 𝑔 ⊆ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∪ ran 𝑔 ≼ ω) |
| 228 | 214, 215,
207, 227 | syl21anc 838 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪
ran 𝑔 ≼
ω) |
| 229 | | ctex 9004 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (∪ ran 𝑔 ≼ ω → ∪ ran 𝑔 ∈ V) |
| 230 | | elpwg 4603 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (∪ ran 𝑔 ∈ V → (∪ ran 𝑔 ∈ 𝒫 dom 𝑅 ↔ ∪ ran
𝑔 ⊆ dom 𝑅)) |
| 231 | 228, 229,
230 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (∪
ran 𝑔 ∈ 𝒫 dom
𝑅 ↔ ∪ ran 𝑔 ⊆ dom 𝑅)) |
| 232 | 212, 231 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪
ran 𝑔 ∈ 𝒫 dom
𝑅) |
| 233 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → 𝐴 ⊆ ∪ (𝑔‘𝑦)) |
| 234 | 233 | ralimi 3083 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑦 ∈
𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ (𝑔‘𝑦)) |
| 235 | | fvssunirn 6939 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑔‘𝑦) ⊆ ∪ ran
𝑔 |
| 236 | 235 | unissi 4916 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ∪ (𝑔‘𝑦) ⊆ ∪ ∪ ran 𝑔 |
| 237 | | sstr 3992 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ ∪ (𝑔‘𝑦) ⊆ ∪ ∪ ran 𝑔) → 𝐴 ⊆ ∪ ∪ ran 𝑔) |
| 238 | 236, 237 | mpan2 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ⊆ ∪ (𝑔‘𝑦) → 𝐴 ⊆ ∪ ∪ ran 𝑔) |
| 239 | 238 | ralimi 3083 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∀𝑦 ∈
𝑋 𝐴 ⊆ ∪ (𝑔‘𝑦) → ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔) |
| 240 | | iunss 5045 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔 ↔ ∀𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔) |
| 241 | 239, 240 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑦 ∈
𝑋 𝐴 ⊆ ∪ (𝑔‘𝑦) → ∪
𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔) |
| 242 | 234, 241 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑦 ∈
𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔) |
| 243 | 242 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔) |
| 244 | 232, 243,
228 | jca32 515 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (∪
ran 𝑔 ∈ 𝒫 dom
𝑅 ∧ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔 ∧ ∪ ran 𝑔 ≼
ω))) |
| 245 | | unieq 4918 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = ∪
ran 𝑔 → ∪ 𝑧 =
∪ ∪ ran 𝑔) |
| 246 | 245 | sseq2d 4016 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = ∪
ran 𝑔 → (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ↔ ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔)) |
| 247 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = ∪
ran 𝑔 → (𝑧 ≼ ω ↔ ∪ ran 𝑔 ≼ ω)) |
| 248 | 246, 247 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = ∪
ran 𝑔 → ((∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω) ↔ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔 ∧ ∪ ran 𝑔 ≼
ω))) |
| 249 | 248 | elrab 3692 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∪ ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↔ (∪ ran 𝑔 ∈ 𝒫 dom 𝑅 ∧ (∪
𝑦 ∈ 𝑋 𝐴 ⊆ ∪ ∪ ran 𝑔 ∧ ∪ ran 𝑔 ≼
ω))) |
| 250 | 244, 249 | sylibr 234 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∪
ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}) |
| 251 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 = 𝑤 → (𝑅‘𝑐) = (𝑅‘𝑤)) |
| 252 | 251 | cbvesumv 34044 |
. . . . . . . . . . . . . . . . . 18
⊢
Σ*𝑐
∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ ∪ ran
𝑔(𝑅‘𝑤) |
| 253 | | esumeq1 34035 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = ∪
ran 𝑔 →
Σ*𝑤 ∈
𝑥(𝑅‘𝑤) = Σ*𝑤 ∈ ∪ ran
𝑔(𝑅‘𝑤)) |
| 254 | 253 | rspceeqv 3645 |
. . . . . . . . . . . . . . . . . 18
⊢ ((∪ ran 𝑔 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ∧
Σ*𝑐 ∈
∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ ∪ ran
𝑔(𝑅‘𝑤)) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) |
| 255 | 250, 252,
254 | sylancl 586 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) |
| 256 | | esumex 34030 |
. . . . . . . . . . . . . . . . . 18
⊢
Σ*𝑐
∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ V |
| 257 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) = (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) |
| 258 | 257 | elrnmpt 5969 |
. . . . . . . . . . . . . . . . . 18
⊢
(Σ*𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ∈ V → (Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤))) |
| 259 | 256, 258 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(Σ*𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ↔ ∃𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) = Σ*𝑤 ∈ 𝑥(𝑅‘𝑤)) |
| 260 | 255, 259 | sylibr 234 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))) |
| 261 | 110 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → < Or
(0[,]+∞)) |
| 262 | | omscl 34297 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ ∪ 𝑦 ∈ 𝑋 𝐴 ∈ 𝒫 ∪ dom 𝑅) → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞)) |
| 263 | 26, 27, 173, 262 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞)) |
| 264 | | xrge0infss 32764 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ran
(𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ⊆ (0[,]+∞) → ∃𝑒 ∈
(0[,]+∞)(∀𝑡
∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ¬ 𝑡 < 𝑒 ∧ ∀𝑡 ∈ (0[,]+∞)(𝑒 < 𝑡 → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < 𝑡))) |
| 265 | 263, 264 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∃𝑒 ∈ (0[,]+∞)(∀𝑡 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) ¬ 𝑡 < 𝑒 ∧ ∀𝑡 ∈ (0[,]+∞)(𝑒 < 𝑡 → ∃𝑢 ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤))𝑢 < 𝑡))) |
| 266 | 261, 265 | inflb 9529 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) → ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ))) |
| 267 | 29 | fveq1i 6907 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) = ((toOMeas‘𝑅)‘∪
𝑦 ∈ 𝑋 𝐴) |
| 268 | 167, 36 | sseqtrd 4020 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑄) |
| 269 | | omsfval 34296 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑄 ∈ 𝑉 ∧ 𝑅:𝑄⟶(0[,]+∞) ∧ ∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑄) → ((toOMeas‘𝑅)‘∪ 𝑦 ∈ 𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
| 270 | 26, 27, 268, 269 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((toOMeas‘𝑅)‘∪ 𝑦 ∈ 𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
| 271 | 267, 270 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) = inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < )) |
| 272 | 271 | breq2d 5155 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ↔ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ))) |
| 273 | 272 | notbid 318 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (¬
Σ*𝑐 ∈
∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ↔ ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)), (0[,]+∞), < ))) |
| 274 | 266, 273 | sylibrd 259 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ∈ ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ (∪ 𝑦 ∈ 𝑋 𝐴 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦
Σ*𝑤 ∈
𝑥(𝑅‘𝑤)) → ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴))) |
| 275 | 164, 260,
274 | sylc 65 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴)) |
| 276 | | biid 261 |
. . . . . . . . . . . . . . 15
⊢ (¬
Σ*𝑐 ∈
∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ↔ ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴)) |
| 277 | 275, 276 | sylib 218 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴)) |
| 278 | | xrlenlt 11326 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ∈ ℝ* ∧
Σ*𝑐 ∈
∪ ran 𝑔(𝑅‘𝑐) ∈ ℝ*) → ((𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ↔ ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴))) |
| 279 | 176, 201,
278 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ((𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐) ↔ ¬ Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) < (𝑀‘∪
𝑦 ∈ 𝑋 𝐴))) |
| 280 | 277, 279 | mpbird 257 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑐 ∈ ∪ ran
𝑔(𝑅‘𝑐)) |
| 281 | | nfv 1914 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑦 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} |
| 282 | 22, 281 | nfan 1899 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑦((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
| 283 | | nfra1 3284 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑦∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
| 284 | 282, 283 | nfan 1899 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑦(((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 285 | | simp-6l 787 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → 𝜑) |
| 286 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
| 287 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
| 288 | 27 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑅:𝑄⟶(0[,]+∞)) |
| 289 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
| 290 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑦 ∈ 𝑋) |
| 291 | 289, 290 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ∈ {𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
| 292 | 186, 291 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ∈ 𝒫 dom 𝑅) |
| 293 | 292 | elpwid 4609 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ⊆ dom 𝑅) |
| 294 | 288, 293 | fssdmd 6754 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑔‘𝑦) ⊆ 𝑄) |
| 295 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑤 ∈ (𝑔‘𝑦)) |
| 296 | 294, 295 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → 𝑤 ∈ 𝑄) |
| 297 | 288, 296 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ 𝑤 ∈ (𝑔‘𝑦)) → (𝑅‘𝑤) ∈ (0[,]+∞)) |
| 298 | 297 | ralrimiva 3146 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → ∀𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
| 299 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔‘𝑦) ∈ V |
| 300 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑤(𝑔‘𝑦) |
| 301 | 300 | esumcl 34031 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑔‘𝑦) ∈ V ∧ ∀𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) →
Σ*𝑤 ∈
(𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
| 302 | 299, 301 | mpan 690 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑤 ∈
(𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞) →
Σ*𝑤 ∈
(𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
| 303 | 298, 302 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
| 304 | 285, 286,
287, 303 | syl21anc 838 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
| 305 | 304 | ex 412 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑦 ∈ 𝑋 → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞))) |
| 306 | 284, 305 | ralrimi 3257 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
| 307 | 14 | esumcl 34031 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) →
Σ*𝑦 ∈
𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
| 308 | 178, 306,
307 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
| 309 | 105, 308 | sselid 3981 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈
ℝ*) |
| 310 | | nfv 1914 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑤(𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
| 311 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
| 312 | | fniunfv 7267 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 Fn 𝑋 → ∪
𝑦 ∈ 𝑋 (𝑔‘𝑦) = ∪ ran 𝑔) |
| 313 | 311, 213,
312 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∪ 𝑦 ∈ 𝑋 (𝑔‘𝑦) = ∪ ran 𝑔) |
| 314 | 310, 313 | esumeq1d 34036 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) →
Σ*𝑤 ∈
∪ 𝑦 ∈ 𝑋 (𝑔‘𝑦)(𝑅‘𝑤) = Σ*𝑤 ∈ ∪ ran
𝑔(𝑅‘𝑤)) |
| 315 | 11 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → 𝑋 ∈ V) |
| 316 | 299 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑔‘𝑦) ∈ V) |
| 317 | 315, 316,
297 | esumiun 34095 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) →
Σ*𝑤 ∈
∪ 𝑦 ∈ 𝑋 (𝑔‘𝑦)(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
| 318 | 314, 317 | eqbrtrrd 5167 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) →
Σ*𝑤 ∈
∪ ran 𝑔(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
| 319 | 9, 318 | sylan 580 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) →
Σ*𝑤 ∈
∪ ran 𝑔(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
| 320 | 319 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑤 ∈ ∪ ran 𝑔(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
| 321 | 252, 320 | eqbrtrid 5178 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ≤ Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤)) |
| 322 | 285, 287,
46 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞)) |
| 323 | | simplll 775 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈
ℝ+)) |
| 324 | 323, 287,
73 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
| 325 | 322, 324 | xrge0addcld 32766 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
| 326 | 325 | ex 412 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑦 ∈ 𝑋 → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞))) |
| 327 | 284, 326 | ralrimi 3257 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
| 328 | 14 | esumcl 34031 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) →
Σ*𝑦 ∈
𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
| 329 | 178, 327,
328 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ (0[,]+∞)) |
| 330 | 105, 329 | sselid 3981 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈
ℝ*) |
| 331 | 215, 10 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑋 ∈ V) |
| 332 | | simp-4l 783 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ)) |
| 333 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
| 334 | 332, 333,
49 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ ℝ) |
| 335 | 334 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → (𝑀‘𝐴) ∈ ℝ) |
| 336 | 65 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
| 337 | 336 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
| 338 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
| 339 | 338 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) |
| 340 | 66 | breq2d 5155 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑀‘𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) →
(Σ*𝑤
∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ↔ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 341 | 340 | biimpar 477 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑀‘𝐴) ∈ ℝ ∧ (𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ) ∧
Σ*𝑤 ∈
(𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) |
| 342 | 335, 337,
339, 341 | syl21anc 838 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) |
| 343 | 342 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 344 | 332 | simpld 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → 𝜑) |
| 345 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) |
| 346 | 344, 345,
333, 303 | syl21anc 838 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ (0[,]+∞)) |
| 347 | 105, 346 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈
ℝ*) |
| 348 | 334 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈
ℝ*) |
| 349 | 336 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) ∈
ℝ*) |
| 350 | 348, 349 | xaddcld 13343 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈
ℝ*) |
| 351 | | xrltle 13191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ∈ ℝ* ∧ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ∈ ℝ*) →
(Σ*𝑤
∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 352 | 347, 350,
351 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 353 | 343, 352 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → (Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 354 | 353 | adantld 490 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ 𝑦 ∈ 𝑋) → ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 355 | 354 | ex 412 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → (𝑦 ∈ 𝑋 → ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))))) |
| 356 | 282, 355 | ralrimi 3257 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → ∀𝑦 ∈ 𝑋 ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 357 | | ralim 3086 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑦 ∈
𝑋 ((𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) → (∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 358 | 356, 357 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) → (∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))) → ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))))) |
| 359 | 358 | imp 406 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) |
| 360 | 359 | r19.21bi 3251 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ ((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) |
| 361 | 284, 14, 331, 304, 325, 360 | esumlef 34063 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦))))) |
| 362 | 164, 46 | sylan 580 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) ∧ 𝑦 ∈ 𝑋) → (𝑀‘𝐴) ∈ (0[,]+∞)) |
| 363 | 284, 14, 331, 362, 324 | esumaddf 34062 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) = (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦))))) |
| 364 | 324 | ex 412 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑦 ∈ 𝑋 → (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞))) |
| 365 | 284, 364 | ralrimi 3257 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → ∀𝑦 ∈ 𝑋 (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
| 366 | 14 | esumcl 34031 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 (𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) →
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
| 367 | 178, 365,
366 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
| 368 | 105, 367 | sselid 3981 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈
ℝ*) |
| 369 | | simp-4r 784 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑓:𝑋–1-1→ℕ) |
| 370 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑓 ∈ V |
| 371 | 370 | rnex 7932 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ran 𝑓 ∈ V |
| 372 | 371 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ran 𝑓 ∈ V) |
| 373 | 58 | frnd 6744 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → ran 𝑓 ⊆ ℕ) |
| 374 | 373 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ran 𝑓 ⊆
ℕ) |
| 375 | 374 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ ℕ) |
| 376 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 2 ∈
ℝ+) |
| 377 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 𝑧 ∈ ℕ) |
| 378 | 377 | nnzd 12640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → 𝑧 ∈ ℤ) |
| 379 | 376, 378 | rpexpcld 14286 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (2↑𝑧) ∈
ℝ+) |
| 380 | 379 | rpreccld 13087 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈
ℝ+) |
| 381 | 71, 380 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈
(0[,]+∞)) |
| 382 | 381 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ℕ) → (1 /
(2↑𝑧)) ∈
(0[,]+∞)) |
| 383 | 375, 382 | syldan 591 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑧 ∈ ran 𝑓) → (1 / (2↑𝑧)) ∈ (0[,]+∞)) |
| 384 | 383 | ralrimiva 3146 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
∀𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞)) |
| 385 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑧ran
𝑓 |
| 386 | 385 | esumcl 34031 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ran
𝑓 ∈ V ∧
∀𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ (0[,]+∞)) →
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)) ∈
(0[,]+∞)) |
| 387 | 372, 384,
386 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)) ∈
(0[,]+∞)) |
| 388 | 105, 387 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)) ∈
ℝ*) |
| 389 | | 1xr 11320 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℝ* |
| 390 | 389 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 1 ∈
ℝ*) |
| 391 | 71 | sseli 3979 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑒 ∈ ℝ+
→ 𝑒 ∈
(0[,]+∞)) |
| 392 | 391 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈
(0[,]+∞)) |
| 393 | | elxrge0 13497 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑒 ∈ (0[,]+∞) ↔
(𝑒 ∈
ℝ* ∧ 0 ≤ 𝑒)) |
| 394 | 392, 393 | sylib 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ∈ ℝ*
∧ 0 ≤ 𝑒)) |
| 395 | | nfv 1914 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑧(𝜑 ∧ 𝑓:𝑋–1-1→ℕ) |
| 396 | | nnex 12272 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ℕ
∈ V |
| 397 | 396 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → ℕ ∈
V) |
| 398 | 395, 397,
381, 373 | esummono 34055 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ Σ*𝑧 ∈ ℕ(1 / (2↑𝑧))) |
| 399 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = 𝑤 → (2↑𝑧) = (2↑𝑤)) |
| 400 | 399 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = 𝑤 → (1 / (2↑𝑧)) = (1 / (2↑𝑤))) |
| 401 | | ioossico 13478 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(0(,)+∞) ⊆ (0[,)+∞) |
| 402 | 69, 401 | eqsstri 4030 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
ℝ+ ⊆ (0[,)+∞) |
| 403 | 402, 380 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → (1 / (2↑𝑧)) ∈
(0[,)+∞)) |
| 404 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ ℕ → (𝑤 ∈ ℕ ↦ (1 /
(2↑𝑤))) = (𝑤 ∈ ℕ ↦ (1 /
(2↑𝑤)))) |
| 405 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → 𝑤 = 𝑧) |
| 406 | 405 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → (2↑𝑤) = (2↑𝑧)) |
| 407 | 406 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑧 ∈ ℕ ∧ 𝑤 = 𝑧) → (1 / (2↑𝑤)) = (1 / (2↑𝑧))) |
| 408 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℕ) |
| 409 | | ovexd 7466 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ ℕ → (1 /
(2↑𝑧)) ∈
V) |
| 410 | 404, 407,
408, 409 | fvmptd 7023 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 ∈ ℕ → ((𝑤 ∈ ℕ ↦ (1 /
(2↑𝑤)))‘𝑧) = (1 / (2↑𝑧))) |
| 411 | 410 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑧 ∈ ℕ) → ((𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))‘𝑧) = (1 / (2↑𝑧))) |
| 412 | | ax-1cn 11213 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 1 ∈
ℂ |
| 413 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑤 ∈ ℕ ↦ (1 /
(2↑𝑤))) = (𝑤 ∈ ℕ ↦ (1 /
(2↑𝑤))) |
| 414 | 413 | geo2lim 15911 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (1 ∈
ℂ → seq1( + , (𝑤
∈ ℕ ↦ (1 / (2↑𝑤)))) ⇝ 1) |
| 415 | 412, 414 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ seq1( + ,
(𝑤 ∈ ℕ ↦
(1 / (2↑𝑤)))) ⇝
1 |
| 416 | 415 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → seq1( + , (𝑤 ∈ ℕ ↦ (1 / (2↑𝑤)))) ⇝ 1) |
| 417 | | 1re 11261 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 ∈
ℝ |
| 418 | 417 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → 1 ∈
ℝ) |
| 419 | 400, 403,
411, 416, 418 | esumcvgsum 34089 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ℕ(1 /
(2↑𝑧)) = Σ𝑧 ∈ ℕ (1 /
(2↑𝑧))) |
| 420 | | geoihalfsum 15918 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Σ𝑧 ∈
ℕ (1 / (2↑𝑧)) =
1 |
| 421 | 419, 420 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ℕ(1 /
(2↑𝑧)) =
1) |
| 422 | 398, 421 | breqtrd 5169 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ≤ 1) |
| 423 | 422 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)) ≤ 1) |
| 424 | | xlemul2a 13331 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) ∈ ℝ* ∧ 1 ∈
ℝ* ∧ (𝑒 ∈ ℝ* ∧ 0 ≤
𝑒)) ∧
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)) ≤ 1) → (𝑒 ·e
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧))) ≤ (𝑒 ·e 1)) |
| 425 | 388, 390,
394, 423, 424 | syl31anc 1375 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧))) ≤ (𝑒 ·e 1)) |
| 426 | 13, 19 | nfan 1899 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑦(𝜑 ∧ 𝑓:𝑋–1-1→ℕ) |
| 427 | 426, 21 | nfan 1899 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑦((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) |
| 428 | 76 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → 𝑒 ∈ ℂ) |
| 429 | 78 | recnd 11289 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℂ) |
| 430 | 429 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ∈ ℂ) |
| 431 | | 2cn 12341 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 2 ∈
ℂ |
| 432 | 431 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → 2 ∈ ℂ) |
| 433 | | 2ne0 12370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 2 ≠
0 |
| 434 | 433 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → 2 ≠ 0) |
| 435 | 432, 434,
60 | expne0d 14192 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ≠ 0) |
| 436 | 435 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (2↑(𝑓‘𝑦)) ≠ 0) |
| 437 | 428, 430,
436 | divrecd 12046 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) = (𝑒 · (1 / (2↑(𝑓‘𝑦))))) |
| 438 | | 1rp 13038 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 1 ∈
ℝ+ |
| 439 | 438 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → 1 ∈
ℝ+) |
| 440 | 439, 61 | rpdivcld 13094 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈
ℝ+) |
| 441 | 52, 440 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
| 442 | 441 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ ℝ) |
| 443 | | rexmul 13313 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑒 ∈ ℝ ∧ (1 /
(2↑(𝑓‘𝑦))) ∈ ℝ) →
(𝑒 ·e (1
/ (2↑(𝑓‘𝑦)))) = (𝑒 · (1 / (2↑(𝑓‘𝑦))))) |
| 444 | 76, 442, 443 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 ·e (1 / (2↑(𝑓‘𝑦)))) = (𝑒 · (1 / (2↑(𝑓‘𝑦))))) |
| 445 | 437, 444 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (𝑒 / (2↑(𝑓‘𝑦))) = (𝑒 ·e (1 / (2↑(𝑓‘𝑦))))) |
| 446 | 445 | ralrimiva 3146 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
∀𝑦 ∈ 𝑋 (𝑒 / (2↑(𝑓‘𝑦))) = (𝑒 ·e (1 / (2↑(𝑓‘𝑦))))) |
| 447 | 427, 446 | esumeq2d 34038 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦))) = Σ*𝑦 ∈ 𝑋(𝑒 ·e (1 / (2↑(𝑓‘𝑦))))) |
| 448 | 11 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑋 ∈ V) |
| 449 | 71, 440 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
| 450 | 449 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝑋) → (1 / (2↑(𝑓‘𝑦))) ∈ (0[,]+∞)) |
| 451 | 402 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → ℝ+ ⊆
(0[,)+∞)) |
| 452 | 451 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈
(0[,)+∞)) |
| 453 | 448, 450,
452 | esummulc2 34083 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e
Σ*𝑦 ∈
𝑋(1 / (2↑(𝑓‘𝑦)))) = Σ*𝑦 ∈ 𝑋(𝑒 ·e (1 / (2↑(𝑓‘𝑦))))) |
| 454 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑦(1 /
(2↑𝑧)) |
| 455 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = (𝑓‘𝑦) → (2↑𝑧) = (2↑(𝑓‘𝑦))) |
| 456 | 455 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = (𝑓‘𝑦) → (1 / (2↑𝑧)) = (1 / (2↑(𝑓‘𝑦)))) |
| 457 | 11 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → 𝑋 ∈ V) |
| 458 | 56 | simprbi 496 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓:𝑋–1-1→ℕ → Fun ◡𝑓) |
| 459 | 57 | feqmptd 6977 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓:𝑋–1-1→ℕ → 𝑓 = (𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦))) |
| 460 | 459 | cnveqd 5886 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓:𝑋–1-1→ℕ → ◡𝑓 = ◡(𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦))) |
| 461 | 460 | funeqd 6588 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓:𝑋–1-1→ℕ → (Fun ◡𝑓 ↔ Fun ◡(𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦)))) |
| 462 | 458, 461 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓:𝑋–1-1→ℕ → Fun ◡(𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦))) |
| 463 | 462 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Fun ◡(𝑦 ∈ 𝑋 ↦ (𝑓‘𝑦))) |
| 464 | 454, 426,
14, 456, 457, 463, 449, 59 | esumc 34052 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑦 ∈ 𝑋(1 / (2↑(𝑓‘𝑦))) = Σ*𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)} (1 / (2↑𝑧))) |
| 465 | | ffn 6736 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓:𝑋⟶ℕ → 𝑓 Fn 𝑋) |
| 466 | | fnrnfv 6968 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 Fn 𝑋 → ran 𝑓 = {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)}) |
| 467 | 58, 465, 466 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → ran 𝑓 = {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)}) |
| 468 | 395, 467 | esumeq1d 34036 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧)) = Σ*𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑓‘𝑦)} (1 / (2↑𝑧))) |
| 469 | 464, 468 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) → Σ*𝑦 ∈ 𝑋(1 / (2↑(𝑓‘𝑦))) = Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) |
| 470 | 469 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑦 ∈
𝑋(1 / (2↑(𝑓‘𝑦))) = Σ*𝑧 ∈ ran 𝑓(1 / (2↑𝑧))) |
| 471 | 470 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e
Σ*𝑦 ∈
𝑋(1 / (2↑(𝑓‘𝑦)))) = (𝑒 ·e
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧)))) |
| 472 | 447, 453,
471 | 3eqtr2rd 2784 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e
Σ*𝑧 ∈
ran 𝑓(1 / (2↑𝑧))) = Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦)))) |
| 473 | 394 | simpld 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈
ℝ*) |
| 474 | | xmulrid 13321 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑒 ∈ ℝ*
→ (𝑒
·e 1) = 𝑒) |
| 475 | 473, 474 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑒 ·e 1) = 𝑒) |
| 476 | 425, 472,
475 | 3brtr3d 5174 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦))) ≤ 𝑒) |
| 477 | 164, 369,
204, 476 | syl21anc 838 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ≤ 𝑒) |
| 478 | | xleadd2a 13296 |
. . . . . . . . . . . . . . . . 17
⊢
(((Σ*𝑦 ∈ 𝑋(𝑒 / (2↑(𝑓‘𝑦))) ∈ ℝ* ∧ 𝑒 ∈ ℝ*
∧ Σ*𝑦
∈ 𝑋(𝑀‘𝐴) ∈ ℝ*) ∧
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦))) ≤ 𝑒) → (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦)))) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
| 479 | 368, 205,
203, 477, 478 | syl31anc 1375 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒
Σ*𝑦 ∈
𝑋(𝑒 / (2↑(𝑓‘𝑦)))) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
| 480 | 363, 479 | eqbrtrd 5165 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋((𝑀‘𝐴) +𝑒 (𝑒 / (2↑(𝑓‘𝑦)))) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
| 481 | 309, 330,
206, 361, 480 | xrletrd 13204 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑦 ∈ 𝑋Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
| 482 | 201, 309,
206, 321, 481 | xrletrd 13204 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → Σ*𝑐 ∈ ∪ ran 𝑔(𝑅‘𝑐) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
| 483 | 176, 201,
206, 280, 482 | xrletrd 13204 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒)) |
| 484 | 204 | rpred 13077 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → 𝑒 ∈ ℝ) |
| 485 | | rexadd 13274 |
. . . . . . . . . . . . 13
⊢
((Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ ∧ 𝑒 ∈ ℝ) →
(Σ*𝑦
∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒) = (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
| 486 | 202, 484,
485 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) +𝑒 𝑒) = (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
| 487 | 483, 486 | breqtrd 5169 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ 𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω}) ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
| 488 | 487 | anasss 466 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) ∧ (𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦))))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
| 489 | 488 | ex 412 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → ((𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))) |
| 490 | 489 | exlimdv 1933 |
. . . . . . . 8
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) →
(∃𝑔(𝑔:𝑋⟶{𝑧 ∈ 𝒫 dom 𝑅 ∣ 𝑧 ≼ ω} ∧ ∀𝑦 ∈ 𝑋 (𝐴 ⊆ ∪ (𝑔‘𝑦) ∧ Σ*𝑤 ∈ (𝑔‘𝑦)(𝑅‘𝑤) < ((𝑀‘𝐴) + (𝑒 / (2↑(𝑓‘𝑦)))))) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))) |
| 491 | 163, 490 | mpd 15 |
. . . . . . 7
⊢ ((((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) ∧ 𝑒 ∈ ℝ+) → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
| 492 | 491 | ralrimiva 3146 |
. . . . . 6
⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) → ∀𝑒 ∈ ℝ+ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒)) |
| 493 | | xralrple 13247 |
. . . . . . . 8
⊢ (((𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ∈ ℝ* ∧
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) → ((𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))) |
| 494 | 175, 493 | sylan 580 |
. . . . . . 7
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → ((𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))) |
| 495 | 494 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) → ((𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ↔ ∀𝑒 ∈ ℝ+ (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ (Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) + 𝑒))) |
| 496 | 492, 495 | mpbird 257 |
. . . . 5
⊢ (((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) ∧ 𝑓:𝑋–1-1→ℕ) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴)) |
| 497 | 496 | ex 412 |
. . . 4
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑓:𝑋–1-1→ℕ → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴))) |
| 498 | 497 | exlimdv 1933 |
. . 3
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → (∃𝑓 𝑓:𝑋–1-1→ℕ → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴))) |
| 499 | 8, 498 | mpd 15 |
. 2
⊢ ((𝜑 ∧ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴)) |
| 500 | 175 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ¬
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ∈
ℝ*) |
| 501 | | pnfge 13172 |
. . . 4
⊢ ((𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ∈ ℝ* → (𝑀‘∪ 𝑦 ∈ 𝑋 𝐴) ≤ +∞) |
| 502 | 500, 501 | syl 17 |
. . 3
⊢ ((𝜑 ∧ ¬
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ +∞) |
| 503 | 46 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑦 ∈ 𝑋 (𝑀‘𝐴) ∈ (0[,]+∞)) |
| 504 | 14 | esumcl 34031 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ ∀𝑦 ∈ 𝑋 (𝑀‘𝐴) ∈ (0[,]+∞)) →
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ (0[,]+∞)) |
| 505 | 11, 503, 504 | syl2anc 584 |
. . . 4
⊢ (𝜑 → Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ (0[,]+∞)) |
| 506 | | xrge0nre 13493 |
. . . 4
⊢
((Σ*𝑦 ∈ 𝑋(𝑀‘𝐴) ∈ (0[,]+∞) ∧ ¬
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) →
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) = +∞) |
| 507 | 505, 506 | sylan 580 |
. . 3
⊢ ((𝜑 ∧ ¬
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) →
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) = +∞) |
| 508 | 502, 507 | breqtrrd 5171 |
. 2
⊢ ((𝜑 ∧ ¬
Σ*𝑦 ∈
𝑋(𝑀‘𝐴) ∈ ℝ) → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴)) |
| 509 | 499, 508 | pm2.61dan 813 |
1
⊢ (𝜑 → (𝑀‘∪
𝑦 ∈ 𝑋 𝐴) ≤ Σ*𝑦 ∈ 𝑋(𝑀‘𝐴)) |