Step | Hyp | Ref
| Expression |
1 | | ovnovollem3.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
2 | | snnzg 4308 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → {𝐴} ≠ ∅) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → {𝐴} ≠ ∅) |
4 | 3 | neneqd 2799 |
. . 3
⊢ (𝜑 → ¬ {𝐴} = ∅) |
5 | 4 | iffalsed 4097 |
. 2
⊢ (𝜑 → if({𝐴} = ∅, 0, inf(𝑀, ℝ*, < )) = inf(𝑀, ℝ*, <
)) |
6 | | snfi 8038 |
. . . 4
⊢ {𝐴} ∈ Fin |
7 | 6 | a1i 11 |
. . 3
⊢ (𝜑 → {𝐴} ∈ Fin) |
8 | | reex 10027 |
. . . . 5
⊢ ℝ
∈ V |
9 | 8 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ ∈
V) |
10 | | ovnovollem3.b |
. . . 4
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
11 | | mapss 7900 |
. . . 4
⊢ ((ℝ
∈ V ∧ 𝐵 ⊆
ℝ) → (𝐵
↑𝑚 {𝐴}) ⊆ (ℝ
↑𝑚 {𝐴})) |
12 | 9, 10, 11 | syl2anc 693 |
. . 3
⊢ (𝜑 → (𝐵 ↑𝑚 {𝐴}) ⊆ (ℝ
↑𝑚 {𝐴})) |
13 | | ovnovollem3.m |
. . 3
⊢ 𝑀 = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 {𝐴}) ↑𝑚
ℕ)((𝐵
↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} |
14 | 7, 12, 13 | ovnval2 40759 |
. 2
⊢ (𝜑 → ((voln*‘{𝐴})‘(𝐵 ↑𝑚 {𝐴})) = if({𝐴} = ∅, 0, inf(𝑀, ℝ*, <
))) |
15 | | ovnovollem3.n |
. . . 4
⊢ 𝑁 = {𝑧 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ)(𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))} |
16 | 10, 15 | ovolval5 40869 |
. . 3
⊢ (𝜑 → (vol*‘𝐵) = inf(𝑁, ℝ*, <
)) |
17 | 1 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ((ℝ × ℝ)
↑𝑚 ℕ)) ∧ (𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝐴 ∈ 𝑉) |
18 | | simplr 792 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ((ℝ × ℝ)
↑𝑚 ℕ)) ∧ (𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝑓 ∈ ((ℝ × ℝ)
↑𝑚 ℕ)) |
19 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑗 → (𝑓‘𝑛) = (𝑓‘𝑗)) |
20 | 19 | opeq2d 4409 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑗 → 〈𝐴, (𝑓‘𝑛)〉 = 〈𝐴, (𝑓‘𝑗)〉) |
21 | 20 | sneqd 4189 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑗 → {〈𝐴, (𝑓‘𝑛)〉} = {〈𝐴, (𝑓‘𝑗)〉}) |
22 | 21 | cbvmptv 4750 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦
{〈𝐴, (𝑓‘𝑛)〉}) = (𝑗 ∈ ℕ ↦ {〈𝐴, (𝑓‘𝑗)〉}) |
23 | | simprl 794 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ((ℝ × ℝ)
↑𝑚 ℕ)) ∧ (𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝐵 ⊆ ∪ ran
([,) ∘ 𝑓)) |
24 | 9, 10 | ssexd 4805 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ V) |
25 | 24 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ ((ℝ × ℝ)
↑𝑚 ℕ)) → 𝐵 ∈ V) |
26 | 25 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ((ℝ × ℝ)
↑𝑚 ℕ)) ∧ (𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝐵 ∈ V) |
27 | | simprr 796 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ ((ℝ × ℝ)
↑𝑚 ℕ)) ∧ (𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) |
28 | 17, 18, 22, 23, 26, 27 | ovnovollem1 40870 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ ((ℝ × ℝ)
↑𝑚 ℕ)) ∧ (𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → ∃𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 {𝐴}) ↑𝑚
ℕ)((𝐵
↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
29 | 28 | 3impa 1259 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ ((ℝ × ℝ)
↑𝑚 ℕ) ∧ (𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → ∃𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 {𝐴}) ↑𝑚
ℕ)((𝐵
↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) |
30 | 29 | 3exp 1264 |
. . . . . . . 8
⊢ (𝜑 → (𝑓 ∈ ((ℝ × ℝ)
↑𝑚 ℕ) → ((𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) → ∃𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 {𝐴}) ↑𝑚
ℕ)((𝐵
↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))))) |
31 | 30 | rexlimdv 3030 |
. . . . . . 7
⊢ (𝜑 → (∃𝑓 ∈ ((ℝ × ℝ)
↑𝑚 ℕ)(𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) → ∃𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 {𝐴}) ↑𝑚
ℕ)((𝐵
↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
32 | 1 | 3ad2ant1 1082 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 {𝐴}) ↑𝑚 ℕ) ∧
((𝐵
↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝐴 ∈ 𝑉) |
33 | 24 | 3ad2ant1 1082 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 {𝐴}) ↑𝑚 ℕ) ∧
((𝐵
↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝐵 ∈ V) |
34 | | simp2 1062 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 {𝐴}) ↑𝑚 ℕ) ∧
((𝐵
↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 {𝐴}) ↑𝑚
ℕ)) |
35 | | simp3l 1089 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 {𝐴}) ↑𝑚 ℕ) ∧
((𝐵
↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → (𝐵 ↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘)) |
36 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑛 → (𝑖‘𝑗) = (𝑖‘𝑛)) |
37 | 36 | coeq2d 5284 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑛 → ([,) ∘ (𝑖‘𝑗)) = ([,) ∘ (𝑖‘𝑛))) |
38 | 37 | fveq1d 6193 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑛 → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ (𝑖‘𝑛))‘𝑘)) |
39 | 38 | ixpeq2dv 7924 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑛 → X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) = X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑛))‘𝑘)) |
40 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑙 → (([,) ∘ (𝑖‘𝑛))‘𝑘) = (([,) ∘ (𝑖‘𝑛))‘𝑙)) |
41 | 40 | cbvixpv 7926 |
. . . . . . . . . . . . . . . 16
⊢ X𝑘 ∈
{𝐴} (([,) ∘ (𝑖‘𝑛))‘𝑘) = X𝑙 ∈ {𝐴} (([,) ∘ (𝑖‘𝑛))‘𝑙) |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑛 → X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑛))‘𝑘) = X𝑙 ∈ {𝐴} (([,) ∘ (𝑖‘𝑛))‘𝑙)) |
43 | 39, 42 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑛 → X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) = X𝑙 ∈ {𝐴} (([,) ∘ (𝑖‘𝑛))‘𝑙)) |
44 | 43 | cbviunv 4559 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) = ∪ 𝑛 ∈ ℕ X𝑙 ∈
{𝐴} (([,) ∘ (𝑖‘𝑛))‘𝑙) |
45 | 44 | sseq2i 3630 |
. . . . . . . . . . . 12
⊢ ((𝐵 ↑𝑚
{𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ↔ (𝐵 ↑𝑚 {𝐴}) ⊆ ∪ 𝑛 ∈ ℕ X𝑙 ∈ {𝐴} (([,) ∘ (𝑖‘𝑛))‘𝑙)) |
46 | 45 | biimpi 206 |
. . . . . . . . . . 11
⊢ ((𝐵 ↑𝑚
{𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) → (𝐵 ↑𝑚 {𝐴}) ⊆ ∪ 𝑛 ∈ ℕ X𝑙 ∈ {𝐴} (([,) ∘ (𝑖‘𝑛))‘𝑙)) |
47 | 35, 46 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 {𝐴}) ↑𝑚 ℕ) ∧
((𝐵
↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → (𝐵 ↑𝑚 {𝐴}) ⊆ ∪ 𝑛 ∈ ℕ X𝑙 ∈ {𝐴} (([,) ∘ (𝑖‘𝑛))‘𝑙)) |
48 | | simp3r 1090 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 {𝐴}) ↑𝑚 ℕ) ∧
((𝐵
↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) |
49 | 38 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑛 → (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑘))) |
50 | 49 | prodeq2ad 39824 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑛 → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑘))) |
51 | 40 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑙 → (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑘)) = (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑙))) |
52 | 51 | cbvprodv 14646 |
. . . . . . . . . . . . . . . . 17
⊢
∏𝑘 ∈
{𝐴} (vol‘(([,)
∘ (𝑖‘𝑛))‘𝑘)) = ∏𝑙 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑙)) |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑛 → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑘)) = ∏𝑙 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑙))) |
54 | 50, 53 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑛 → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = ∏𝑙 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑙))) |
55 | 54 | cbvmptv 4750 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ ↦
∏𝑘 ∈ {𝐴} (vol‘(([,) ∘
(𝑖‘𝑗))‘𝑘))) = (𝑛 ∈ ℕ ↦ ∏𝑙 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑙))) |
56 | 55 | fveq2i 6194 |
. . . . . . . . . . . . 13
⊢
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) =
(Σ^‘(𝑛 ∈ ℕ ↦ ∏𝑙 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑙)))) |
57 | 56 | eqeq2i 2634 |
. . . . . . . . . . . 12
⊢ (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔ 𝑧 =
(Σ^‘(𝑛 ∈ ℕ ↦ ∏𝑙 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑙))))) |
58 | 57 | biimpi 206 |
. . . . . . . . . . 11
⊢ (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) → 𝑧 =
(Σ^‘(𝑛 ∈ ℕ ↦ ∏𝑙 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑙))))) |
59 | 48, 58 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 {𝐴}) ↑𝑚 ℕ) ∧
((𝐵
↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝑧 =
(Σ^‘(𝑛 ∈ ℕ ↦ ∏𝑙 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑙))))) |
60 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (𝑖‘𝑚) = (𝑖‘𝑛)) |
61 | 60 | fveq1d 6193 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → ((𝑖‘𝑚)‘𝐴) = ((𝑖‘𝑛)‘𝐴)) |
62 | 61 | cbvmptv 4750 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ ↦ ((𝑖‘𝑚)‘𝐴)) = (𝑛 ∈ ℕ ↦ ((𝑖‘𝑛)‘𝐴)) |
63 | 32, 33, 34, 47, 59, 62 | ovnovollem2 40871 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑𝑚 {𝐴}) ↑𝑚 ℕ) ∧
((𝐵
↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → ∃𝑓 ∈ ((ℝ × ℝ)
↑𝑚 ℕ)(𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) |
64 | 63 | 3exp 1264 |
. . . . . . . 8
⊢ (𝜑 → (𝑖 ∈ (((ℝ × ℝ)
↑𝑚 {𝐴}) ↑𝑚 ℕ)
→ (((𝐵
↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) → ∃𝑓 ∈ ((ℝ × ℝ)
↑𝑚 ℕ)(𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))))) |
65 | 64 | rexlimdv 3030 |
. . . . . . 7
⊢ (𝜑 → (∃𝑖 ∈ (((ℝ × ℝ)
↑𝑚 {𝐴}) ↑𝑚
ℕ)((𝐵
↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) → ∃𝑓 ∈ ((ℝ × ℝ)
↑𝑚 ℕ)(𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))))) |
66 | 31, 65 | impbid 202 |
. . . . . 6
⊢ (𝜑 → (∃𝑓 ∈ ((ℝ × ℝ)
↑𝑚 ℕ)(𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) ↔ ∃𝑖 ∈ (((ℝ ×
ℝ) ↑𝑚 {𝐴}) ↑𝑚
ℕ)((𝐵
↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) |
67 | 66 | rabbidv 3189 |
. . . . 5
⊢ (𝜑 → {𝑧 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ)(𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))} = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 {𝐴}) ↑𝑚
ℕ)((𝐵
↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) |
68 | 15 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝑁 = {𝑧 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑𝑚 ℕ)(𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))}) |
69 | 13 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝑀 = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑𝑚 {𝐴}) ↑𝑚
ℕ)((𝐵
↑𝑚 {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) |
70 | 67, 68, 69 | 3eqtr4d 2666 |
. . . 4
⊢ (𝜑 → 𝑁 = 𝑀) |
71 | 70 | infeq1d 8383 |
. . 3
⊢ (𝜑 → inf(𝑁, ℝ*, < ) = inf(𝑀, ℝ*, <
)) |
72 | 16, 71 | eqtrd 2656 |
. 2
⊢ (𝜑 → (vol*‘𝐵) = inf(𝑀, ℝ*, <
)) |
73 | 5, 14, 72 | 3eqtr4d 2666 |
1
⊢ (𝜑 → ((voln*‘{𝐴})‘(𝐵 ↑𝑚 {𝐴})) = (vol*‘𝐵)) |