Proof of Theorem elovolm
Step | Hyp | Ref
| Expression |
1 | | eqeq1 2614 |
. . . . 5
⊢ (𝑦 = 𝐵 → (𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ) ↔ 𝐵 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))) |
2 | 1 | anbi2d 736 |
. . . 4
⊢ (𝑦 = 𝐵 → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < )) ↔
(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )))) |
3 | 2 | rexbidv 3034 |
. . 3
⊢ (𝑦 = 𝐵 → (∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < )) ↔
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )))) |
4 | | ovolval.1 |
. . 3
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))} |
5 | 3, 4 | elrab2 3333 |
. 2
⊢ (𝐵 ∈ 𝑀 ↔ (𝐵 ∈ ℝ* ∧
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )))) |
6 | | reex 9906 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ V |
7 | 6, 6 | xpex 6860 |
. . . . . . . . . . . 12
⊢ (ℝ
× ℝ) ∈ V |
8 | 7 | inex2 4728 |
. . . . . . . . . . 11
⊢ ( ≤
∩ (ℝ × ℝ)) ∈ V |
9 | | nnex 10903 |
. . . . . . . . . . 11
⊢ ℕ
∈ V |
10 | 8, 9 | elmap 7772 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ↔ 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) |
11 | | eqid 2610 |
. . . . . . . . . . 11
⊢ ((abs
∘ − ) ∘ 𝑓) = ((abs ∘ − ) ∘ 𝑓) |
12 | | eqid 2610 |
. . . . . . . . . . 11
⊢ seq1( + ,
((abs ∘ − ) ∘ 𝑓)) = seq1( + , ((abs ∘ − )
∘ 𝑓)) |
13 | 11, 12 | ovolsf 23048 |
. . . . . . . . . 10
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → seq1( + , ((abs ∘ − ) ∘
𝑓)):ℕ⟶(0[,)+∞)) |
14 | 10, 13 | sylbi 206 |
. . . . . . . . 9
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) → seq1( + , ((abs
∘ − ) ∘ 𝑓)):ℕ⟶(0[,)+∞)) |
15 | | icossxr 12129 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ ℝ* |
16 | | fss 5969 |
. . . . . . . . 9
⊢ ((seq1( +
, ((abs ∘ − ) ∘ 𝑓)):ℕ⟶(0[,)+∞) ∧
(0[,)+∞) ⊆ ℝ*) → seq1( + , ((abs ∘
− ) ∘ 𝑓)):ℕ⟶ℝ*) |
17 | 14, 15, 16 | sylancl 693 |
. . . . . . . 8
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) → seq1( + , ((abs
∘ − ) ∘ 𝑓)):ℕ⟶ℝ*) |
18 | | frn 5966 |
. . . . . . . 8
⊢ (seq1( +
, ((abs ∘ − ) ∘ 𝑓)):ℕ⟶ℝ* →
ran seq1( + , ((abs ∘ − ) ∘ 𝑓)) ⊆
ℝ*) |
19 | | supxrcl 12017 |
. . . . . . . 8
⊢ (ran
seq1( + , ((abs ∘ − ) ∘ 𝑓)) ⊆ ℝ* → sup(ran
seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ∈
ℝ*) |
20 | 17, 18, 19 | 3syl 18 |
. . . . . . 7
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) → sup(ran seq1( + ,
((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ∈
ℝ*) |
21 | | eleq1 2676 |
. . . . . . 7
⊢ (𝐵 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < ) → (𝐵 ∈ ℝ*
↔ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ∈
ℝ*)) |
22 | 20, 21 | syl5ibrcom 236 |
. . . . . 6
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) → (𝐵 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ) → 𝐵 ∈
ℝ*)) |
23 | 22 | imp 444 |
. . . . 5
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ∧ 𝐵 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )) → 𝐵 ∈
ℝ*) |
24 | 23 | adantrl 748 |
. . . 4
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < ))) →
𝐵 ∈
ℝ*) |
25 | 24 | rexlimiva 3010 |
. . 3
⊢
(∃𝑓 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )) → 𝐵 ∈
ℝ*) |
26 | 25 | pm4.71ri 663 |
. 2
⊢
(∃𝑓 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )) ↔ (𝐵 ∈ ℝ* ∧
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )))) |
27 | 5, 26 | bitr4i 266 |
1
⊢ (𝐵 ∈ 𝑀 ↔ ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, <
))) |