Step |
Hyp |
Ref |
Expression |
1 |
|
ovolval.1 |
⊢ 𝑀 = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } |
2 |
|
reex |
⊢ ℝ ∈ V |
3 |
2
|
elpw2 |
⊢ ( 𝐴 ∈ 𝒫 ℝ ↔ 𝐴 ⊆ ℝ ) |
4 |
|
cleq1lem |
⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) ) ) |
5 |
4
|
rexbidv |
⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) ↔ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) ) ) |
6 |
5
|
rabbidv |
⊢ ( 𝑥 = 𝐴 → { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } ) |
7 |
6 1
|
eqtr4di |
⊢ ( 𝑥 = 𝐴 → { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } = 𝑀 ) |
8 |
7
|
infeq1d |
⊢ ( 𝑥 = 𝐴 → inf ( { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } , ℝ* , < ) = inf ( 𝑀 , ℝ* , < ) ) |
9 |
|
df-ovol |
⊢ vol* = ( 𝑥 ∈ 𝒫 ℝ ↦ inf ( { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝑥 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) } , ℝ* , < ) ) |
10 |
|
xrltso |
⊢ < Or ℝ* |
11 |
10
|
infex |
⊢ inf ( 𝑀 , ℝ* , < ) ∈ V |
12 |
8 9 11
|
fvmpt |
⊢ ( 𝐴 ∈ 𝒫 ℝ → ( vol* ‘ 𝐴 ) = inf ( 𝑀 , ℝ* , < ) ) |
13 |
3 12
|
sylbir |
⊢ ( 𝐴 ⊆ ℝ → ( vol* ‘ 𝐴 ) = inf ( 𝑀 , ℝ* , < ) ) |