Proof of Theorem elovolm
Step | Hyp | Ref
| Expression |
1 | | eqeq1 2655 |
. . . . 5
⊢ (𝑦 = 𝐵 → (𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ) ↔ 𝐵 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))) |
2 | 1 | anbi2d 740 |
. . . 4
⊢ (𝑦 = 𝐵 → ((𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < )) ↔
(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )))) |
3 | 2 | rexbidv 3081 |
. . 3
⊢ (𝑦 = 𝐵 → (∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < )) ↔
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )))) |
4 | | ovolval.1 |
. . 3
⊢ 𝑀 = {𝑦 ∈ ℝ* ∣
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝑦 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ))} |
5 | 3, 4 | elrab2 3399 |
. 2
⊢ (𝐵 ∈ 𝑀 ↔ (𝐵 ∈ ℝ* ∧
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )))) |
6 | | reex 10065 |
. . . . . . . . . . . . 13
⊢ ℝ
∈ V |
7 | 6, 6 | xpex 7004 |
. . . . . . . . . . . 12
⊢ (ℝ
× ℝ) ∈ V |
8 | 7 | inex2 4833 |
. . . . . . . . . . 11
⊢ ( ≤
∩ (ℝ × ℝ)) ∈ V |
9 | | nnex 11064 |
. . . . . . . . . . 11
⊢ ℕ
∈ V |
10 | 8, 9 | elmap 7928 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ↔ 𝑓:ℕ⟶( ≤ ∩ (ℝ ×
ℝ))) |
11 | | eqid 2651 |
. . . . . . . . . . 11
⊢ ((abs
∘ − ) ∘ 𝑓) = ((abs ∘ − ) ∘ 𝑓) |
12 | | eqid 2651 |
. . . . . . . . . . 11
⊢ seq1( + ,
((abs ∘ − ) ∘ 𝑓)) = seq1( + , ((abs ∘ − )
∘ 𝑓)) |
13 | 11, 12 | ovolsf 23287 |
. . . . . . . . . 10
⊢ (𝑓:ℕ⟶( ≤ ∩
(ℝ × ℝ)) → seq1( + , ((abs ∘ − ) ∘
𝑓)):ℕ⟶(0[,)+∞)) |
14 | 10, 13 | sylbi 207 |
. . . . . . . . 9
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) → seq1( + , ((abs
∘ − ) ∘ 𝑓)):ℕ⟶(0[,)+∞)) |
15 | | icossxr 12296 |
. . . . . . . . 9
⊢
(0[,)+∞) ⊆ ℝ* |
16 | | fss 6094 |
. . . . . . . . 9
⊢ ((seq1( +
, ((abs ∘ − ) ∘ 𝑓)):ℕ⟶(0[,)+∞) ∧
(0[,)+∞) ⊆ ℝ*) → seq1( + , ((abs ∘
− ) ∘ 𝑓)):ℕ⟶ℝ*) |
17 | 14, 15, 16 | sylancl 695 |
. . . . . . . 8
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) → seq1( + , ((abs
∘ − ) ∘ 𝑓)):ℕ⟶ℝ*) |
18 | | frn 6091 |
. . . . . . . 8
⊢ (seq1( +
, ((abs ∘ − ) ∘ 𝑓)):ℕ⟶ℝ* →
ran seq1( + , ((abs ∘ − ) ∘ 𝑓)) ⊆
ℝ*) |
19 | | supxrcl 12183 |
. . . . . . . 8
⊢ (ran
seq1( + , ((abs ∘ − ) ∘ 𝑓)) ⊆ ℝ* → sup(ran
seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ∈
ℝ*) |
20 | 17, 18, 19 | 3syl 18 |
. . . . . . 7
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) → sup(ran seq1( + ,
((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ∈
ℝ*) |
21 | | eleq1 2718 |
. . . . . . 7
⊢ (𝐵 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < ) → (𝐵 ∈ ℝ*
↔ sup(ran seq1( + , ((abs ∘ − ) ∘ 𝑓)), ℝ*, < ) ∈
ℝ*)) |
22 | 20, 21 | syl5ibrcom 237 |
. . . . . 6
⊢ (𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) → (𝐵 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < ) → 𝐵 ∈
ℝ*)) |
23 | 22 | imp 444 |
. . . . 5
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ∧ 𝐵 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )) → 𝐵 ∈
ℝ*) |
24 | 23 | adantrl 752 |
. . . 4
⊢ ((𝑓 ∈ (( ≤ ∩ (ℝ
× ℝ)) ↑𝑚 ℕ) ∧ (𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, < ))) →
𝐵 ∈
ℝ*) |
25 | 24 | rexlimiva 3057 |
. . 3
⊢
(∃𝑓 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )) → 𝐵 ∈
ℝ*) |
26 | 25 | pm4.71ri 666 |
. 2
⊢
(∃𝑓 ∈ ((
≤ ∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )) ↔ (𝐵 ∈ ℝ* ∧
∃𝑓 ∈ (( ≤
∩ (ℝ × ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran ((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs ∘ − )
∘ 𝑓)),
ℝ*, < )))) |
27 | 5, 26 | bitr4i 267 |
1
⊢ (𝐵 ∈ 𝑀 ↔ ∃𝑓 ∈ (( ≤ ∩ (ℝ ×
ℝ)) ↑𝑚 ℕ)(𝐴 ⊆ ∪ ran
((,) ∘ 𝑓) ∧ 𝐵 = sup(ran seq1( + , ((abs
∘ − ) ∘ 𝑓)), ℝ*, <
))) |