Step | Hyp | Ref
| Expression |
1 | | ovnval2.1 |
. . 3
⊢ (𝜑 → 𝑋 ∈ Fin) |
2 | 1 | ovnval 39431 |
. 2
⊢ (𝜑 → (voln*‘𝑋) = (𝑦 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↦ if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, <
)))) |
3 | | biidd 251 |
. . . 4
⊢ (𝑦 = 𝐴 → (𝑋 = ∅ ↔ 𝑋 = ∅)) |
4 | | sseq1 3589 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → (𝑦 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ↔ 𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘))) |
5 | 4 | anbi1d 737 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → ((𝑦 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ (𝐴 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
6 | 5 | rexbidv 3034 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) ↔ ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
7 | 6 | rabbidv 3164 |
. . . . . 6
⊢ (𝑦 = 𝐴 → {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) |
8 | | ovnval2.3 |
. . . . . 6
⊢ 𝑀 = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} |
9 | 7, 8 | syl6eqr 2662 |
. . . . 5
⊢ (𝑦 = 𝐴 → {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} = 𝑀) |
10 | 9 | infeq1d 8266 |
. . . 4
⊢ (𝑦 = 𝐴 → inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < ) =
inf(𝑀, ℝ*,
< )) |
11 | 3, 10 | ifbieq2d 4061 |
. . 3
⊢ (𝑦 = 𝐴 → if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < )) =
if(𝑋 = ∅, 0,
inf(𝑀, ℝ*,
< ))) |
12 | 11 | adantl 481 |
. 2
⊢ ((𝜑 ∧ 𝑦 = 𝐴) → if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < )) =
if(𝑋 = ∅, 0,
inf(𝑀, ℝ*,
< ))) |
13 | | ovnval2.2 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ (ℝ ↑𝑚
𝑋)) |
14 | | ovex 6577 |
. . . . . 6
⊢ (ℝ
↑𝑚 𝑋) ∈ V |
15 | 14 | a1i 11 |
. . . . 5
⊢ (𝜑 → (ℝ
↑𝑚 𝑋) ∈ V) |
16 | 15, 13 | ssexd 4733 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ V) |
17 | | elpwg 4116 |
. . . 4
⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↔ 𝐴 ⊆ (ℝ ↑𝑚
𝑋))) |
18 | 16, 17 | syl 17 |
. . 3
⊢ (𝜑 → (𝐴 ∈ 𝒫 (ℝ
↑𝑚 𝑋) ↔ 𝐴 ⊆ (ℝ ↑𝑚
𝑋))) |
19 | 13, 18 | mpbird 246 |
. 2
⊢ (𝜑 → 𝐴 ∈ 𝒫 (ℝ
↑𝑚 𝑋)) |
20 | | c0ex 9913 |
. . . 4
⊢ 0 ∈
V |
21 | 20 | a1i 11 |
. . 3
⊢ (𝜑 → 0 ∈
V) |
22 | 8 | infeq1i 8267 |
. . . 4
⊢ inf(𝑀, ℝ*, < ) =
inf({𝑧 ∈
ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, <
) |
23 | | xrltso 11850 |
. . . . . 6
⊢ < Or
ℝ* |
24 | 23 | infex 8282 |
. . . . 5
⊢
inf({𝑧 ∈
ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < ) ∈
V |
25 | 24 | a1i 11 |
. . . 4
⊢ (𝜑 → inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 𝑋) ↑𝑚 ℕ)(𝐴 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < ) ∈
V) |
26 | 22, 25 | syl5eqel 2692 |
. . 3
⊢ (𝜑 → inf(𝑀, ℝ*, < ) ∈
V) |
27 | 21, 26 | ifcld 4081 |
. 2
⊢ (𝜑 → if(𝑋 = ∅, 0, inf(𝑀, ℝ*, < )) ∈
V) |
28 | 2, 12, 19, 27 | fvmptd 6197 |
1
⊢ (𝜑 → ((voln*‘𝑋)‘𝐴) = if(𝑋 = ∅, 0, inf(𝑀, ℝ*, <
))) |