Step | Hyp | Ref
| Expression |
1 | | ovn0.1 |
. . 3
⊢ (𝜑 → 𝑋 ∈ Fin) |
2 | | 0ss 4282 |
. . . 4
⊢ ∅
⊆ (ℝ ↑m 𝑋) |
3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → ∅ ⊆ (ℝ
↑m 𝑋)) |
4 | | 0ss 4282 |
. . . . . . . . 9
⊢ ∅
⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) |
5 | 4 | a1i 11 |
. . . . . . . 8
⊢ (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) → ∅ ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) |
6 | | id 22 |
. . . . . . . 8
⊢ (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) → 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) |
7 | 5, 6 | jca 515 |
. . . . . . 7
⊢ (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) → (∅ ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
8 | | simpr 488 |
. . . . . . 7
⊢ ((∅
⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) → 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) |
9 | 7, 8 | impbii 212 |
. . . . . 6
⊢ (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔ (∅ ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
10 | 9 | rexbii 3160 |
. . . . 5
⊢
(∃𝑖 ∈
(((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔ ∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(∅ ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
11 | 10 | rgenw 3065 |
. . . 4
⊢
∀𝑧 ∈
ℝ* (∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔ ∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(∅ ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
12 | | rabbi 3285 |
. . . 4
⊢
(∀𝑧 ∈
ℝ* (∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔ ∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(∅ ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) ↔ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))} = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(∅
⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) |
13 | 11, 12 | mpbi 233 |
. . 3
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))} = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(∅
⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} |
14 | 1, 3, 13 | ovnval2 43609 |
. 2
⊢ (𝜑 → ((voln*‘𝑋)‘∅) = if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))}, ℝ*, <
))) |
15 | | simpr 488 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 = ∅) → 𝑋 = ∅) |
16 | 15 | iftrued 4419 |
. . 3
⊢ ((𝜑 ∧ 𝑋 = ∅) → if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))}, ℝ*, < )) =
0) |
17 | | iffalse 4420 |
. . . . 5
⊢ (¬
𝑋 = ∅ → if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))}, ℝ*, < )) =
inf({𝑧 ∈
ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))}, ℝ*, <
)) |
18 | 17 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))}, ℝ*, < )) =
inf({𝑧 ∈
ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))}, ℝ*, <
)) |
19 | 1 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ∈ Fin) |
20 | | neqne 2942 |
. . . . . 6
⊢ (¬
𝑋 = ∅ → 𝑋 ≠ ∅) |
21 | 20 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → 𝑋 ≠ ∅) |
22 | | eqid 2738 |
. . . . 5
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))} = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))} |
23 | 14, 17 | sylan9eq 2793 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ((voln*‘𝑋)‘∅) = inf({𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))}, ℝ*, <
)) |
24 | 23 | eqcomd 2744 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))}, ℝ*, < ) =
((voln*‘𝑋)‘∅)) |
25 | 1 | ovnf 43627 |
. . . . . . . 8
⊢ (𝜑 → (voln*‘𝑋):𝒫 (ℝ
↑m 𝑋)⟶(0[,]+∞)) |
26 | | 0elpw 5219 |
. . . . . . . . 9
⊢ ∅
∈ 𝒫 (ℝ ↑m 𝑋) |
27 | 26 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ∅ ∈ 𝒫
(ℝ ↑m 𝑋)) |
28 | 25, 27 | ffvelrnd 6856 |
. . . . . . 7
⊢ (𝜑 → ((voln*‘𝑋)‘∅) ∈
(0[,]+∞)) |
29 | 28 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → ((voln*‘𝑋)‘∅) ∈
(0[,]+∞)) |
30 | 24, 29 | eqeltrd 2833 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))}, ℝ*, < ) ∈
(0[,]+∞)) |
31 | | eqidd 2739 |
. . . . . . . 8
⊢ (𝑚 = 𝑙 → 〈1, 0〉 = 〈1,
0〉) |
32 | 31 | cbvmptv 5130 |
. . . . . . 7
⊢ (𝑚 ∈ 𝑋 ↦ 〈1, 0〉) = (𝑙 ∈ 𝑋 ↦ 〈1, 0〉) |
33 | 32 | a1i 11 |
. . . . . 6
⊢ (ℎ = 𝑗 → (𝑚 ∈ 𝑋 ↦ 〈1, 0〉) = (𝑙 ∈ 𝑋 ↦ 〈1, 0〉)) |
34 | 33 | cbvmptv 5130 |
. . . . 5
⊢ (ℎ ∈ ℕ ↦ (𝑚 ∈ 𝑋 ↦ 〈1, 0〉)) = (𝑗 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ 〈1, 0〉)) |
35 | 19, 21, 22, 30, 34 | ovn0lem 43629 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))}, ℝ*, < ) =
0) |
36 | 18, 35 | eqtrd 2773 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = ∅) → if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))}, ℝ*, < )) =
0) |
37 | 16, 36 | pm2.61dan 813 |
. 2
⊢ (𝜑 → if(𝑋 = ∅, 0, inf({𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))}, ℝ*, < )) =
0) |
38 | 14, 37 | eqtrd 2773 |
1
⊢ (𝜑 → ((voln*‘𝑋)‘∅) =
0) |