| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ovnovollem3.a | . . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) | 
| 2 | 1 | snn0d 4774 | . . . 4
⊢ (𝜑 → {𝐴} ≠ ∅) | 
| 3 | 2 | neneqd 2944 | . . 3
⊢ (𝜑 → ¬ {𝐴} = ∅) | 
| 4 | 3 | iffalsed 4535 | . 2
⊢ (𝜑 → if({𝐴} = ∅, 0, inf(𝑀, ℝ*, < )) = inf(𝑀, ℝ*, <
)) | 
| 5 |  | snfi 9084 | . . . 4
⊢ {𝐴} ∈ Fin | 
| 6 | 5 | a1i 11 | . . 3
⊢ (𝜑 → {𝐴} ∈ Fin) | 
| 7 |  | reex 11247 | . . . . 5
⊢ ℝ
∈ V | 
| 8 | 7 | a1i 11 | . . . 4
⊢ (𝜑 → ℝ ∈
V) | 
| 9 |  | ovnovollem3.b | . . . 4
⊢ (𝜑 → 𝐵 ⊆ ℝ) | 
| 10 |  | mapss 8930 | . . . 4
⊢ ((ℝ
∈ V ∧ 𝐵 ⊆
ℝ) → (𝐵
↑m {𝐴})
⊆ (ℝ ↑m {𝐴})) | 
| 11 | 8, 9, 10 | syl2anc 584 | . . 3
⊢ (𝜑 → (𝐵 ↑m {𝐴}) ⊆ (ℝ ↑m
{𝐴})) | 
| 12 |  | ovnovollem3.m | . . 3
⊢ 𝑀 = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m {𝐴}) ↑m ℕ)((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} | 
| 13 | 6, 11, 12 | ovnval2 46565 | . 2
⊢ (𝜑 → ((voln*‘{𝐴})‘(𝐵 ↑m {𝐴})) = if({𝐴} = ∅, 0, inf(𝑀, ℝ*, <
))) | 
| 14 |  | ovnovollem3.n | . . . 4
⊢ 𝑁 = {𝑧 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))} | 
| 15 | 9, 14 | ovolval5 46675 | . . 3
⊢ (𝜑 → (vol*‘𝐵) = inf(𝑁, ℝ*, <
)) | 
| 16 | 1 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ ((ℝ × ℝ)
↑m ℕ)) ∧ (𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝐴 ∈ 𝑉) | 
| 17 |  | simplr 768 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ ((ℝ × ℝ)
↑m ℕ)) ∧ (𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝑓 ∈ ((ℝ × ℝ)
↑m ℕ)) | 
| 18 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑛 = 𝑗 → (𝑓‘𝑛) = (𝑓‘𝑗)) | 
| 19 | 18 | opeq2d 4879 | . . . . . . . . . . 11
⊢ (𝑛 = 𝑗 → 〈𝐴, (𝑓‘𝑛)〉 = 〈𝐴, (𝑓‘𝑗)〉) | 
| 20 | 19 | sneqd 4637 | . . . . . . . . . 10
⊢ (𝑛 = 𝑗 → {〈𝐴, (𝑓‘𝑛)〉} = {〈𝐴, (𝑓‘𝑗)〉}) | 
| 21 | 20 | cbvmptv 5254 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ ↦
{〈𝐴, (𝑓‘𝑛)〉}) = (𝑗 ∈ ℕ ↦ {〈𝐴, (𝑓‘𝑗)〉}) | 
| 22 |  | simprl 770 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ ((ℝ × ℝ)
↑m ℕ)) ∧ (𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝐵 ⊆ ∪ ran
([,) ∘ 𝑓)) | 
| 23 | 8, 9 | ssexd 5323 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ V) | 
| 24 | 23 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ ((ℝ × ℝ)
↑m ℕ)) → 𝐵 ∈ V) | 
| 25 | 24 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ ((ℝ × ℝ)
↑m ℕ)) ∧ (𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝐵 ∈ V) | 
| 26 |  | simprr 772 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ ((ℝ × ℝ)
↑m ℕ)) ∧ (𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) | 
| 27 | 16, 17, 21, 22, 25, 26 | ovnovollem1 46676 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ ((ℝ × ℝ)
↑m ℕ)) ∧ (𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) → ∃𝑖 ∈ (((ℝ ×
ℝ) ↑m {𝐴}) ↑m ℕ)((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) | 
| 28 | 27 | rexlimdva2 3156 | . . . . . . 7
⊢ (𝜑 → (∃𝑓 ∈ ((ℝ × ℝ)
↑m ℕ)(𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) → ∃𝑖 ∈ (((ℝ ×
ℝ) ↑m {𝐴}) ↑m ℕ)((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) | 
| 29 | 1 | 3ad2ant1 1133 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m {𝐴})
↑m ℕ) ∧ ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝐴 ∈ 𝑉) | 
| 30 | 23 | 3ad2ant1 1133 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m {𝐴})
↑m ℕ) ∧ ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝐵 ∈ V) | 
| 31 |  | simp2 1137 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m {𝐴})
↑m ℕ) ∧ ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝑖 ∈ (((ℝ × ℝ)
↑m {𝐴})
↑m ℕ)) | 
| 32 |  | simp3l 1201 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m {𝐴})
↑m ℕ) ∧ ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → (𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘)) | 
| 33 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑛 → (𝑖‘𝑗) = (𝑖‘𝑛)) | 
| 34 | 33 | coeq2d 5872 | . . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑛 → ([,) ∘ (𝑖‘𝑗)) = ([,) ∘ (𝑖‘𝑛))) | 
| 35 | 34 | fveq1d 6907 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑛 → (([,) ∘ (𝑖‘𝑗))‘𝑘) = (([,) ∘ (𝑖‘𝑛))‘𝑘)) | 
| 36 | 35 | ixpeq2dv 8954 | . . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑛 → X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) = X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑛))‘𝑘)) | 
| 37 |  | fveq2 6905 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑙 → (([,) ∘ (𝑖‘𝑛))‘𝑘) = (([,) ∘ (𝑖‘𝑛))‘𝑙)) | 
| 38 | 37 | cbvixpv 8956 | . . . . . . . . . . . . . . . 16
⊢ X𝑘 ∈
{𝐴} (([,) ∘ (𝑖‘𝑛))‘𝑘) = X𝑙 ∈ {𝐴} (([,) ∘ (𝑖‘𝑛))‘𝑙) | 
| 39 | 38 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑛 → X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑛))‘𝑘) = X𝑙 ∈ {𝐴} (([,) ∘ (𝑖‘𝑛))‘𝑙)) | 
| 40 | 36, 39 | eqtrd 2776 | . . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑛 → X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) = X𝑙 ∈ {𝐴} (([,) ∘ (𝑖‘𝑛))‘𝑙)) | 
| 41 | 40 | cbviunv 5039 | . . . . . . . . . . . . 13
⊢ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) = ∪ 𝑛 ∈ ℕ X𝑙 ∈
{𝐴} (([,) ∘ (𝑖‘𝑛))‘𝑙) | 
| 42 | 41 | sseq2i 4012 | . . . . . . . . . . . 12
⊢ ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ↔ (𝐵 ↑m {𝐴}) ⊆ ∪ 𝑛 ∈ ℕ X𝑙 ∈ {𝐴} (([,) ∘ (𝑖‘𝑛))‘𝑙)) | 
| 43 | 42 | biimpi 216 | . . . . . . . . . . 11
⊢ ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) → (𝐵 ↑m {𝐴}) ⊆ ∪ 𝑛 ∈ ℕ X𝑙 ∈ {𝐴} (([,) ∘ (𝑖‘𝑛))‘𝑙)) | 
| 44 | 32, 43 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m {𝐴})
↑m ℕ) ∧ ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → (𝐵 ↑m {𝐴}) ⊆ ∪ 𝑛 ∈ ℕ X𝑙 ∈ {𝐴} (([,) ∘ (𝑖‘𝑛))‘𝑙)) | 
| 45 |  | simp3r 1202 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m {𝐴})
↑m ℕ) ∧ ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) | 
| 46 | 35 | fveq2d 6909 | . . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑛 → (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑘))) | 
| 47 | 46 | prodeq2ad 45612 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑛 → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑘))) | 
| 48 | 37 | fveq2d 6909 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑙 → (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑘)) = (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑙))) | 
| 49 | 48 | cbvprodv 15951 | . . . . . . . . . . . . . . . . 17
⊢
∏𝑘 ∈
{𝐴} (vol‘(([,)
∘ (𝑖‘𝑛))‘𝑘)) = ∏𝑙 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑙)) | 
| 50 | 49 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑛 → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑘)) = ∏𝑙 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑙))) | 
| 51 | 47, 50 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑛 → ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)) = ∏𝑙 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑙))) | 
| 52 | 51 | cbvmptv 5254 | . . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ ↦
∏𝑘 ∈ {𝐴} (vol‘(([,) ∘
(𝑖‘𝑗))‘𝑘))) = (𝑛 ∈ ℕ ↦ ∏𝑙 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑙))) | 
| 53 | 52 | fveq2i 6908 | . . . . . . . . . . . . 13
⊢
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) =
(Σ^‘(𝑛 ∈ ℕ ↦ ∏𝑙 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑙)))) | 
| 54 | 53 | eqeq2i 2749 | . . . . . . . . . . . 12
⊢ (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) ↔ 𝑧 =
(Σ^‘(𝑛 ∈ ℕ ↦ ∏𝑙 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑙))))) | 
| 55 | 54 | biimpi 216 | . . . . . . . . . . 11
⊢ (𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) → 𝑧 =
(Σ^‘(𝑛 ∈ ℕ ↦ ∏𝑙 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑙))))) | 
| 56 | 45, 55 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m {𝐴})
↑m ℕ) ∧ ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝑧 =
(Σ^‘(𝑛 ∈ ℕ ↦ ∏𝑙 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑛))‘𝑙))))) | 
| 57 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (𝑖‘𝑚) = (𝑖‘𝑛)) | 
| 58 | 57 | fveq1d 6907 | . . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → ((𝑖‘𝑚)‘𝐴) = ((𝑖‘𝑛)‘𝐴)) | 
| 59 | 58 | cbvmptv 5254 | . . . . . . . . . 10
⊢ (𝑚 ∈ ℕ ↦ ((𝑖‘𝑚)‘𝐴)) = (𝑛 ∈ ℕ ↦ ((𝑖‘𝑛)‘𝐴)) | 
| 60 | 29, 30, 31, 44, 56, 59 | ovnovollem2 46677 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m {𝐴})
↑m ℕ) ∧ ((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → ∃𝑓 ∈ ((ℝ × ℝ)
↑m ℕ)(𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))) | 
| 61 | 60 | 3exp 1119 | . . . . . . . 8
⊢ (𝜑 → (𝑖 ∈ (((ℝ × ℝ)
↑m {𝐴})
↑m ℕ) → (((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) → ∃𝑓 ∈ ((ℝ × ℝ)
↑m ℕ)(𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))))) | 
| 62 | 61 | rexlimdv 3152 | . . . . . . 7
⊢ (𝜑 → (∃𝑖 ∈ (((ℝ × ℝ)
↑m {𝐴})
↑m ℕ)((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) → ∃𝑓 ∈ ((ℝ × ℝ)
↑m ℕ)(𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))))) | 
| 63 | 28, 62 | impbid 212 | . . . . . 6
⊢ (𝜑 → (∃𝑓 ∈ ((ℝ × ℝ)
↑m ℕ)(𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓))) ↔ ∃𝑖 ∈ (((ℝ ×
ℝ) ↑m {𝐴}) ↑m ℕ)((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) | 
| 64 | 63 | rabbidv 3443 | . . . . 5
⊢ (𝜑 → {𝑧 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))} = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m {𝐴}) ↑m ℕ)((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) | 
| 65 | 14 | a1i 11 | . . . . 5
⊢ (𝜑 → 𝑁 = {𝑧 ∈ ℝ* ∣
∃𝑓 ∈ ((ℝ
× ℝ) ↑m ℕ)(𝐵 ⊆ ∪ ran
([,) ∘ 𝑓) ∧ 𝑧 =
(Σ^‘((vol ∘ [,)) ∘ 𝑓)))}) | 
| 66 | 12 | a1i 11 | . . . . 5
⊢ (𝜑 → 𝑀 = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m {𝐴}) ↑m ℕ)((𝐵 ↑m {𝐴}) ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ {𝐴} (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ {𝐴} (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) | 
| 67 | 64, 65, 66 | 3eqtr4d 2786 | . . . 4
⊢ (𝜑 → 𝑁 = 𝑀) | 
| 68 | 67 | infeq1d 9518 | . . 3
⊢ (𝜑 → inf(𝑁, ℝ*, < ) = inf(𝑀, ℝ*, <
)) | 
| 69 | 15, 68 | eqtrd 2776 | . 2
⊢ (𝜑 → (vol*‘𝐵) = inf(𝑀, ℝ*, <
)) | 
| 70 | 4, 13, 69 | 3eqtr4d 2786 | 1
⊢ (𝜑 → ((voln*‘{𝐴})‘(𝐵 ↑m {𝐴})) = (vol*‘𝐵)) |