Proof of Theorem ovnhoilem2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ovnhoilem2.m | . . . . . . . . . 10
⊢ 𝑀 = {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} | 
| 2 | 1 | eleq2i 2833 | . . . . . . . . 9
⊢ (𝑧 ∈ 𝑀 ↔ 𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}) | 
| 3 |  | rabid 3458 | . . . . . . . . 9
⊢ (𝑧 ∈ {𝑧 ∈ ℝ* ∣
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ↔ (𝑧 ∈ ℝ* ∧
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) | 
| 4 | 2, 3 | bitri 275 | . . . . . . . 8
⊢ (𝑧 ∈ 𝑀 ↔ (𝑧 ∈ ℝ* ∧
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) | 
| 5 | 4 | biimpi 216 | . . . . . . 7
⊢ (𝑧 ∈ 𝑀 → (𝑧 ∈ ℝ* ∧
∃𝑖 ∈ (((ℝ
× ℝ) ↑m 𝑋) ↑m ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))))) | 
| 6 | 5 | simprd 495 | . . . . . 6
⊢ (𝑧 ∈ 𝑀 → ∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) | 
| 7 | 6 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑀) → ∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) | 
| 8 |  | ovnhoilem2.l | . . . . . . . . . 10
⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑m 𝑥), 𝑏 ∈ (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘)))))) | 
| 9 |  | ovnhoilem2.x | . . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ Fin) | 
| 10 | 9 | 3ad2ant1 1134 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ (𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝑋 ∈ Fin) | 
| 11 |  | ovnhoilem2.a | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴:𝑋⟶ℝ) | 
| 12 | 11 | 3ad2ant1 1134 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ (𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝐴:𝑋⟶ℝ) | 
| 13 |  | ovnhoilem2.b | . . . . . . . . . . 11
⊢ (𝜑 → 𝐵:𝑋⟶ℝ) | 
| 14 | 13 | 3ad2ant1 1134 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ (𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → 𝐵:𝑋⟶ℝ) | 
| 15 |  | elmapi 8889 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) → 𝑖:ℕ⟶((ℝ
× ℝ) ↑m 𝑋)) | 
| 16 | 15 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (𝑖‘𝑛) ∈ ((ℝ × ℝ)
↑m 𝑋)) | 
| 17 |  | elmapi 8889 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑖‘𝑛) ∈ ((ℝ × ℝ)
↑m 𝑋)
→ (𝑖‘𝑛):𝑋⟶(ℝ ×
ℝ)) | 
| 18 | 16, 17 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (𝑖‘𝑛):𝑋⟶(ℝ ×
ℝ)) | 
| 19 | 18 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) ∧ 𝑙 ∈ 𝑋) → ((𝑖‘𝑛)‘𝑙) ∈ (ℝ ×
ℝ)) | 
| 20 |  | xp1st 8046 | . . . . . . . . . . . . . . . 16
⊢ (((𝑖‘𝑛)‘𝑙) ∈ (ℝ × ℝ) →
(1st ‘((𝑖‘𝑛)‘𝑙)) ∈ ℝ) | 
| 21 | 19, 20 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) ∧ 𝑙 ∈ 𝑋) → (1st ‘((𝑖‘𝑛)‘𝑙)) ∈ ℝ) | 
| 22 | 21 | fmpttd 7135 | . . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙))):𝑋⟶ℝ) | 
| 23 |  | reex 11246 | . . . . . . . . . . . . . . . 16
⊢ ℝ
∈ V | 
| 24 | 23 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ℝ
∈ V) | 
| 25 |  | 1nn 12277 | . . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℕ | 
| 26 | 25 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) → 1
∈ ℕ) | 
| 27 | 15, 26 | ffvelcdmd 7105 | . . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) → (𝑖‘1) ∈ ((ℝ
× ℝ) ↑m 𝑋)) | 
| 28 |  | elmapex 8888 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑖‘1) ∈ ((ℝ
× ℝ) ↑m 𝑋) → ((ℝ × ℝ) ∈ V
∧ 𝑋 ∈
V)) | 
| 29 | 28 | simprd 495 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑖‘1) ∈ ((ℝ
× ℝ) ↑m 𝑋) → 𝑋 ∈ V) | 
| 30 | 27, 29 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) → 𝑋 ∈ V) | 
| 31 | 30 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → 𝑋 ∈ V) | 
| 32 |  | elmapg 8879 | . . . . . . . . . . . . . . 15
⊢ ((ℝ
∈ V ∧ 𝑋 ∈ V)
→ ((𝑙 ∈ 𝑋 ↦ (1st
‘((𝑖‘𝑛)‘𝑙))) ∈ (ℝ ↑m 𝑋) ↔ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙))):𝑋⟶ℝ)) | 
| 33 | 24, 31, 32 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙))) ∈ (ℝ ↑m 𝑋) ↔ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙))):𝑋⟶ℝ)) | 
| 34 | 22, 33 | mpbird 257 | . . . . . . . . . . . . 13
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙))) ∈ (ℝ ↑m 𝑋)) | 
| 35 | 34 | fmpttd 7135 | . . . . . . . . . . . 12
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) → (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))):ℕ⟶(ℝ
↑m 𝑋)) | 
| 36 |  | id 22 | . . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) → 𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m
ℕ)) | 
| 37 |  | nnex 12272 | . . . . . . . . . . . . . . . 16
⊢ ℕ
∈ V | 
| 38 | 37 | mptex 7243 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))) ∈ V | 
| 39 | 38 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) → (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))) ∈ V) | 
| 40 |  | ovnhoilem2.f | . . . . . . . . . . . . . . 15
⊢ 𝐹 = (𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ↦ (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙))))) | 
| 41 | 40 | fvmpt2 7027 | . . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))) ∈ V) → (𝐹‘𝑖) = (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙))))) | 
| 42 | 36, 39, 41 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) → (𝐹‘𝑖) = (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙))))) | 
| 43 | 42 | feq1d 6720 | . . . . . . . . . . . 12
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) → ((𝐹‘𝑖):ℕ⟶(ℝ ↑m
𝑋) ↔ (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))):ℕ⟶(ℝ
↑m 𝑋))) | 
| 44 | 35, 43 | mpbird 257 | . . . . . . . . . . 11
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) → (𝐹‘𝑖):ℕ⟶(ℝ ↑m
𝑋)) | 
| 45 | 44 | 3ad2ant2 1135 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ (𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → (𝐹‘𝑖):ℕ⟶(ℝ ↑m
𝑋)) | 
| 46 |  | xp2nd 8047 | . . . . . . . . . . . . . . . 16
⊢ (((𝑖‘𝑛)‘𝑙) ∈ (ℝ × ℝ) →
(2nd ‘((𝑖‘𝑛)‘𝑙)) ∈ ℝ) | 
| 47 | 19, 46 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) ∧ 𝑙 ∈ 𝑋) → (2nd ‘((𝑖‘𝑛)‘𝑙)) ∈ ℝ) | 
| 48 | 47 | fmpttd 7135 | . . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙))):𝑋⟶ℝ) | 
| 49 |  | elmapg 8879 | . . . . . . . . . . . . . . 15
⊢ ((ℝ
∈ V ∧ 𝑋 ∈ V)
→ ((𝑙 ∈ 𝑋 ↦ (2nd
‘((𝑖‘𝑛)‘𝑙))) ∈ (ℝ ↑m 𝑋) ↔ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙))):𝑋⟶ℝ)) | 
| 50 | 24, 31, 49 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙))) ∈ (ℝ ↑m 𝑋) ↔ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙))):𝑋⟶ℝ)) | 
| 51 | 48, 50 | mpbird 257 | . . . . . . . . . . . . 13
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙))) ∈ (ℝ ↑m 𝑋)) | 
| 52 | 51 | fmpttd 7135 | . . . . . . . . . . . 12
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) → (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))):ℕ⟶(ℝ
↑m 𝑋)) | 
| 53 | 37 | mptex 7243 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))) ∈ V | 
| 54 | 53 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) → (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))) ∈ V) | 
| 55 |  | ovnhoilem2.s | . . . . . . . . . . . . . . 15
⊢ 𝑆 = (𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ↦ (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙))))) | 
| 56 | 55 | fvmpt2 7027 | . . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))) ∈ V) → (𝑆‘𝑖) = (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙))))) | 
| 57 | 36, 54, 56 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) → (𝑆‘𝑖) = (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙))))) | 
| 58 | 57 | feq1d 6720 | . . . . . . . . . . . 12
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) → ((𝑆‘𝑖):ℕ⟶(ℝ ↑m
𝑋) ↔ (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))):ℕ⟶(ℝ
↑m 𝑋))) | 
| 59 | 52, 58 | mpbird 257 | . . . . . . . . . . 11
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) → (𝑆‘𝑖):ℕ⟶(ℝ ↑m
𝑋)) | 
| 60 | 59 | 3ad2ant2 1135 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ (𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → (𝑆‘𝑖):ℕ⟶(ℝ ↑m
𝑋)) | 
| 61 |  | simp3 1139 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ 𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) → 𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) | 
| 62 |  | ovnhoilem2.i | . . . . . . . . . . . . . 14
⊢ 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) | 
| 63 | 62 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ 𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) → 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))) | 
| 64 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = 𝑛 → (𝑖‘𝑗) = (𝑖‘𝑛)) | 
| 65 | 64 | fveq1d 6908 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 = 𝑛 → ((𝑖‘𝑗)‘𝑘) = ((𝑖‘𝑛)‘𝑘)) | 
| 66 | 65 | fveq2d 6910 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑛 → (1st ‘((𝑖‘𝑗)‘𝑘)) = (1st ‘((𝑖‘𝑛)‘𝑘))) | 
| 67 | 65 | fveq2d 6910 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 = 𝑛 → (2nd ‘((𝑖‘𝑗)‘𝑘)) = (2nd ‘((𝑖‘𝑛)‘𝑘))) | 
| 68 | 66, 67 | oveq12d 7449 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = 𝑛 → ((1st ‘((𝑖‘𝑗)‘𝑘))[,)(2nd ‘((𝑖‘𝑗)‘𝑘))) = ((1st ‘((𝑖‘𝑛)‘𝑘))[,)(2nd ‘((𝑖‘𝑛)‘𝑘)))) | 
| 69 | 68 | ixpeq2dv 8953 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑛 → X𝑘 ∈ 𝑋 ((1st ‘((𝑖‘𝑗)‘𝑘))[,)(2nd ‘((𝑖‘𝑗)‘𝑘))) = X𝑘 ∈ 𝑋 ((1st ‘((𝑖‘𝑛)‘𝑘))[,)(2nd ‘((𝑖‘𝑛)‘𝑘)))) | 
| 70 | 69 | cbviunv 5040 | . . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((1st ‘((𝑖‘𝑗)‘𝑘))[,)(2nd ‘((𝑖‘𝑗)‘𝑘))) = ∪
𝑛 ∈ ℕ X𝑘 ∈
𝑋 ((1st
‘((𝑖‘𝑛)‘𝑘))[,)(2nd ‘((𝑖‘𝑛)‘𝑘))) | 
| 71 | 70 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) →
∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 ((1st ‘((𝑖‘𝑗)‘𝑘))[,)(2nd ‘((𝑖‘𝑗)‘𝑘))) = ∪
𝑛 ∈ ℕ X𝑘 ∈
𝑋 ((1st
‘((𝑖‘𝑛)‘𝑘))[,)(2nd ‘((𝑖‘𝑛)‘𝑘)))) | 
| 72 | 15 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑗 ∈ ℕ) → (𝑖‘𝑗) ∈ ((ℝ × ℝ)
↑m 𝑋)) | 
| 73 |  | elmapi 8889 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖‘𝑗) ∈ ((ℝ × ℝ)
↑m 𝑋)
→ (𝑖‘𝑗):𝑋⟶(ℝ ×
ℝ)) | 
| 74 | 72, 73 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑗 ∈ ℕ) → (𝑖‘𝑗):𝑋⟶(ℝ ×
ℝ)) | 
| 75 | 74 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (𝑖‘𝑗):𝑋⟶(ℝ ×
ℝ)) | 
| 76 |  | simpr 484 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) | 
| 77 | 75, 76 | fvovco 45198 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (([,) ∘ (𝑖‘𝑗))‘𝑘) = ((1st ‘((𝑖‘𝑗)‘𝑘))[,)(2nd ‘((𝑖‘𝑗)‘𝑘)))) | 
| 78 | 77 | ixpeq2dva 8952 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑗 ∈ ℕ) → X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) = X𝑘 ∈ 𝑋 ((1st ‘((𝑖‘𝑗)‘𝑘))[,)(2nd ‘((𝑖‘𝑗)‘𝑘)))) | 
| 79 | 78 | iuneq2dv 5016 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) →
∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) = ∪ 𝑗 ∈ ℕ X𝑘 ∈
𝑋 ((1st
‘((𝑖‘𝑗)‘𝑘))[,)(2nd ‘((𝑖‘𝑗)‘𝑘)))) | 
| 80 |  | simpl 482 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → 𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m
ℕ)) | 
| 81 | 38 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))) ∈ V) | 
| 82 | 80, 81, 41 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑖) = (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙))))) | 
| 83 | 82 | fveq1d 6908 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑖)‘𝑛) = ((𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙))))‘𝑛)) | 
| 84 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈
ℕ) | 
| 85 |  | mptexg 7241 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑋 ∈ V → (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙))) ∈ V) | 
| 86 | 30, 85 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) → (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙))) ∈ V) | 
| 87 | 86 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙))) ∈ V) | 
| 88 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))) = (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))) | 
| 89 | 88 | fvmpt2 7027 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑛 ∈ ℕ ∧ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙))) ∈ V) → ((𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙))))‘𝑛) = (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))) | 
| 90 | 84, 87, 89 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙))))‘𝑛) = (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))) | 
| 91 | 83, 90 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑖)‘𝑛) = (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))) | 
| 92 | 91 | fveq1d 6908 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (((𝐹‘𝑖)‘𝑛)‘𝑘) = ((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)) | 
| 93 | 92 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝐹‘𝑖)‘𝑛)‘𝑘) = ((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)) | 
| 94 |  | eqidd 2738 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑘 ∈ 𝑋) → (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙))) = (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))) | 
| 95 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑙 = 𝑘) → 𝑙 = 𝑘) | 
| 96 | 95 | fveq2d 6910 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑙 = 𝑘) → ((𝑖‘𝑛)‘𝑙) = ((𝑖‘𝑛)‘𝑘)) | 
| 97 | 96 | fveq2d 6910 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑙 = 𝑘) → (1st ‘((𝑖‘𝑛)‘𝑙)) = (1st ‘((𝑖‘𝑛)‘𝑘))) | 
| 98 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋) | 
| 99 |  | fvexd 6921 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑘 ∈ 𝑋) → (1st ‘((𝑖‘𝑛)‘𝑘)) ∈ V) | 
| 100 | 94, 97, 98, 99 | fvmptd 7023 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))‘𝑘) = (1st ‘((𝑖‘𝑛)‘𝑘))) | 
| 101 | 100 | adantlr 715 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))‘𝑘) = (1st ‘((𝑖‘𝑛)‘𝑘))) | 
| 102 | 93, 101 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝐹‘𝑖)‘𝑛)‘𝑘) = (1st ‘((𝑖‘𝑛)‘𝑘))) | 
| 103 | 57 | fveq1d 6908 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) → ((𝑆‘𝑖)‘𝑛) = ((𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙))))‘𝑛)) | 
| 104 | 103 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ((𝑆‘𝑖)‘𝑛) = ((𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙))))‘𝑛)) | 
| 105 |  | mptexg 7241 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑋 ∈ V → (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙))) ∈ V) | 
| 106 | 30, 105 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) → (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙))) ∈ V) | 
| 107 | 106 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙))) ∈ V) | 
| 108 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))) = (𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))) | 
| 109 | 108 | fvmpt2 7027 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑛 ∈ ℕ ∧ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙))) ∈ V) → ((𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙))))‘𝑛) = (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))) | 
| 110 | 84, 107, 109 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ((𝑛 ∈ ℕ ↦ (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙))))‘𝑛) = (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))) | 
| 111 | 104, 110 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → ((𝑆‘𝑖)‘𝑛) = (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))) | 
| 112 | 111 | fveq1d 6908 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → (((𝑆‘𝑖)‘𝑛)‘𝑘) = ((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)) | 
| 113 | 112 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑖)‘𝑛)‘𝑘) = ((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)) | 
| 114 |  | eqidd 2738 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑘 ∈ 𝑋) → (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙))) = (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))) | 
| 115 |  | 2fveq3 6911 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑙 = 𝑘 → (2nd ‘((𝑖‘𝑛)‘𝑙)) = (2nd ‘((𝑖‘𝑛)‘𝑘))) | 
| 116 | 115 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑘 ∈ 𝑋) ∧ 𝑙 = 𝑘) → (2nd ‘((𝑖‘𝑛)‘𝑙)) = (2nd ‘((𝑖‘𝑛)‘𝑘))) | 
| 117 |  | fvexd 6921 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑘 ∈ 𝑋) → (2nd ‘((𝑖‘𝑛)‘𝑘)) ∈ V) | 
| 118 | 114, 116,
98, 117 | fvmptd 7023 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))‘𝑘) = (2nd ‘((𝑖‘𝑛)‘𝑘))) | 
| 119 | 118 | adantlr 715 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))‘𝑘) = (2nd ‘((𝑖‘𝑛)‘𝑘))) | 
| 120 | 113, 119 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (((𝑆‘𝑖)‘𝑛)‘𝑘) = (2nd ‘((𝑖‘𝑛)‘𝑘))) | 
| 121 | 102, 120 | oveq12d 7449 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((((𝐹‘𝑖)‘𝑛)‘𝑘)[,)(((𝑆‘𝑖)‘𝑛)‘𝑘)) = ((1st ‘((𝑖‘𝑛)‘𝑘))[,)(2nd ‘((𝑖‘𝑛)‘𝑘)))) | 
| 122 | 121 | ixpeq2dva 8952 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑛 ∈ ℕ) → X𝑘 ∈
𝑋 ((((𝐹‘𝑖)‘𝑛)‘𝑘)[,)(((𝑆‘𝑖)‘𝑛)‘𝑘)) = X𝑘 ∈ 𝑋 ((1st ‘((𝑖‘𝑛)‘𝑘))[,)(2nd ‘((𝑖‘𝑛)‘𝑘)))) | 
| 123 | 122 | iuneq2dv 5016 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) →
∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝐹‘𝑖)‘𝑛)‘𝑘)[,)(((𝑆‘𝑖)‘𝑛)‘𝑘)) = ∪
𝑛 ∈ ℕ X𝑘 ∈
𝑋 ((1st
‘((𝑖‘𝑛)‘𝑘))[,)(2nd ‘((𝑖‘𝑛)‘𝑘)))) | 
| 124 | 71, 79, 123 | 3eqtr4d 2787 | . . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) →
∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) = ∪ 𝑛 ∈ ℕ X𝑘 ∈
𝑋 ((((𝐹‘𝑖)‘𝑛)‘𝑘)[,)(((𝑆‘𝑖)‘𝑛)‘𝑘))) | 
| 125 | 124 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)) → ∪ 𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) = ∪ 𝑛 ∈ ℕ X𝑘 ∈
𝑋 ((((𝐹‘𝑖)‘𝑛)‘𝑘)[,)(((𝑆‘𝑖)‘𝑛)‘𝑘))) | 
| 126 | 125 | 3adant3 1133 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ 𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) → ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) = ∪ 𝑛 ∈ ℕ X𝑘 ∈
𝑋 ((((𝐹‘𝑖)‘𝑛)‘𝑘)[,)(((𝑆‘𝑖)‘𝑛)‘𝑘))) | 
| 127 | 63, 126 | sseq12d 4017 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ 𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) → (𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ↔ X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝐹‘𝑖)‘𝑛)‘𝑘)[,)(((𝑆‘𝑖)‘𝑛)‘𝑘)))) | 
| 128 | 61, 127 | mpbid 232 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ 𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘)) → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝐹‘𝑖)‘𝑛)‘𝑘)[,)(((𝑆‘𝑖)‘𝑛)‘𝑘))) | 
| 129 | 128 | 3adant3r 1182 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ (𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ∪ 𝑛 ∈ ℕ X𝑘 ∈ 𝑋 ((((𝐹‘𝑖)‘𝑛)‘𝑘)[,)(((𝑆‘𝑖)‘𝑛)‘𝑘))) | 
| 130 | 8, 10, 12, 14, 45, 60, 129 | hoidmvle 46615 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ (𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → (𝐴(𝐿‘𝑋)𝐵) ≤
(Σ^‘(𝑛 ∈ ℕ ↦ (((𝐹‘𝑖)‘𝑛)(𝐿‘𝑋)((𝑆‘𝑖)‘𝑛))))) | 
| 131 |  | simpl 482 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑛 = 𝑗 ∧ 𝑙 ∈ 𝑋) → 𝑛 = 𝑗) | 
| 132 | 131 | fveq2d 6910 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑛 = 𝑗 ∧ 𝑙 ∈ 𝑋) → (𝑖‘𝑛) = (𝑖‘𝑗)) | 
| 133 | 132 | fveq1d 6908 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑛 = 𝑗 ∧ 𝑙 ∈ 𝑋) → ((𝑖‘𝑛)‘𝑙) = ((𝑖‘𝑗)‘𝑙)) | 
| 134 | 133 | fveq2d 6910 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 = 𝑗 ∧ 𝑙 ∈ 𝑋) → (1st ‘((𝑖‘𝑛)‘𝑙)) = (1st ‘((𝑖‘𝑗)‘𝑙))) | 
| 135 | 134 | mpteq2dva 5242 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑗 → (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙))) = (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑗)‘𝑙)))) | 
| 136 | 135 | fveq1d 6908 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑗 → ((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))‘𝑘) = ((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑗)‘𝑙)))‘𝑘)) | 
| 137 | 136 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋) → ((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))‘𝑘) = ((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑗)‘𝑙)))‘𝑘)) | 
| 138 |  | eqidd 2738 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ 𝑋 → (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑗)‘𝑙))) = (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑗)‘𝑙)))) | 
| 139 |  | 2fveq3 6911 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑙 = 𝑘 → (1st ‘((𝑖‘𝑗)‘𝑙)) = (1st ‘((𝑖‘𝑗)‘𝑘))) | 
| 140 | 139 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ 𝑋 ∧ 𝑙 = 𝑘) → (1st ‘((𝑖‘𝑗)‘𝑙)) = (1st ‘((𝑖‘𝑗)‘𝑘))) | 
| 141 |  | id 22 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ 𝑋 → 𝑘 ∈ 𝑋) | 
| 142 |  | fvexd 6921 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ 𝑋 → (1st ‘((𝑖‘𝑗)‘𝑘)) ∈ V) | 
| 143 | 138, 140,
141, 142 | fvmptd 7023 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ 𝑋 → ((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑗)‘𝑙)))‘𝑘) = (1st ‘((𝑖‘𝑗)‘𝑘))) | 
| 144 | 143 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋) → ((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑗)‘𝑙)))‘𝑘) = (1st ‘((𝑖‘𝑗)‘𝑘))) | 
| 145 | 137, 144 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋) → ((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))‘𝑘) = (1st ‘((𝑖‘𝑗)‘𝑘))) | 
| 146 | 133 | fveq2d 6910 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑛 = 𝑗 ∧ 𝑙 ∈ 𝑋) → (2nd ‘((𝑖‘𝑛)‘𝑙)) = (2nd ‘((𝑖‘𝑗)‘𝑙))) | 
| 147 | 146 | mpteq2dva 5242 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑗 → (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙))) = (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑗)‘𝑙)))) | 
| 148 | 147 | fveq1d 6908 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑗 → ((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))‘𝑘) = ((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑗)‘𝑙)))‘𝑘)) | 
| 149 | 148 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋) → ((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))‘𝑘) = ((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑗)‘𝑙)))‘𝑘)) | 
| 150 |  | eqidd 2738 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ 𝑋 → (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑗)‘𝑙))) = (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑗)‘𝑙)))) | 
| 151 |  | 2fveq3 6911 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑙 = 𝑘 → (2nd ‘((𝑖‘𝑗)‘𝑙)) = (2nd ‘((𝑖‘𝑗)‘𝑘))) | 
| 152 | 151 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ 𝑋 ∧ 𝑙 = 𝑘) → (2nd ‘((𝑖‘𝑗)‘𝑙)) = (2nd ‘((𝑖‘𝑗)‘𝑘))) | 
| 153 |  | fvexd 6921 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ 𝑋 → (2nd ‘((𝑖‘𝑗)‘𝑘)) ∈ V) | 
| 154 | 150, 152,
141, 153 | fvmptd 7023 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ 𝑋 → ((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑗)‘𝑙)))‘𝑘) = (2nd ‘((𝑖‘𝑗)‘𝑘))) | 
| 155 | 154 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋) → ((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑗)‘𝑙)))‘𝑘) = (2nd ‘((𝑖‘𝑗)‘𝑘))) | 
| 156 | 149, 155 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋) → ((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))‘𝑘) = (2nd ‘((𝑖‘𝑗)‘𝑘))) | 
| 157 | 145, 156 | oveq12d 7449 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋) → (((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)[,)((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)) = ((1st ‘((𝑖‘𝑗)‘𝑘))[,)(2nd ‘((𝑖‘𝑗)‘𝑘)))) | 
| 158 | 157 | fveq2d 6910 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑛 = 𝑗 ∧ 𝑘 ∈ 𝑋) → (vol‘(((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)[,)((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))‘𝑘))) = (vol‘((1st
‘((𝑖‘𝑗)‘𝑘))[,)(2nd ‘((𝑖‘𝑗)‘𝑘))))) | 
| 159 | 158 | prodeq2dv 15958 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑗 → ∏𝑘 ∈ 𝑋 (vol‘(((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)[,)((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))‘𝑘))) = ∏𝑘 ∈ 𝑋 (vol‘((1st ‘((𝑖‘𝑗)‘𝑘))[,)(2nd ‘((𝑖‘𝑗)‘𝑘))))) | 
| 160 | 159 | cbvmptv 5255 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ ↦
∏𝑘 ∈ 𝑋 (vol‘(((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)[,)((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘((1st ‘((𝑖‘𝑗)‘𝑘))[,)(2nd ‘((𝑖‘𝑗)‘𝑘))))) | 
| 161 | 160 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) → (𝑛 ∈ ℕ ↦
∏𝑘 ∈ 𝑋 (vol‘(((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)[,)((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘((1st ‘((𝑖‘𝑗)‘𝑘))[,)(2nd ‘((𝑖‘𝑗)‘𝑘)))))) | 
| 162 | 77 | eqcomd 2743 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → ((1st ‘((𝑖‘𝑗)‘𝑘))[,)(2nd ‘((𝑖‘𝑗)‘𝑘))) = (([,) ∘ (𝑖‘𝑗))‘𝑘)) | 
| 163 | 162 | fveq2d 6910 | . . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑗 ∈ ℕ) ∧ 𝑘 ∈ 𝑋) → (vol‘((1st
‘((𝑖‘𝑗)‘𝑘))[,)(2nd ‘((𝑖‘𝑗)‘𝑘)))) = (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) | 
| 164 | 163 | prodeq2dv 15958 | . . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) ∧ 𝑗 ∈ ℕ) →
∏𝑘 ∈ 𝑋 (vol‘((1st
‘((𝑖‘𝑗)‘𝑘))[,)(2nd ‘((𝑖‘𝑗)‘𝑘)))) = ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))) | 
| 165 | 164 | mpteq2dva 5242 | . . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) → (𝑗 ∈ ℕ ↦
∏𝑘 ∈ 𝑋 (vol‘((1st
‘((𝑖‘𝑗)‘𝑘))[,)(2nd ‘((𝑖‘𝑗)‘𝑘))))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) | 
| 166 | 161, 165 | eqtrd 2777 | . . . . . . . . . . . . 13
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) → (𝑛 ∈ ℕ ↦
∏𝑘 ∈ 𝑋 (vol‘(((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)[,)((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)))) = (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))) | 
| 167 | 166 | fveq2d 6910 | . . . . . . . . . . . 12
⊢ (𝑖 ∈ (((ℝ ×
ℝ) ↑m 𝑋) ↑m ℕ) →
(Σ^‘(𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)[,)((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))‘𝑘))))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) | 
| 168 | 167 | 3ad2ant2 1135 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) →
(Σ^‘(𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)[,)((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))‘𝑘))))) =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) | 
| 169 | 91 | adantll 714 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)) ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑖)‘𝑛) = (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))) | 
| 170 | 111 | adantll 714 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)) ∧ 𝑛 ∈ ℕ) → ((𝑆‘𝑖)‘𝑛) = (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))) | 
| 171 | 169, 170 | oveq12d 7449 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)) ∧ 𝑛 ∈ ℕ) → (((𝐹‘𝑖)‘𝑛)(𝐿‘𝑋)((𝑆‘𝑖)‘𝑛)) = ((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))(𝐿‘𝑋)(𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙))))) | 
| 172 | 9 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)) ∧ 𝑛 ∈ ℕ) → 𝑋 ∈ Fin) | 
| 173 |  | ovnhoilem2.n | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑋 ≠ ∅) | 
| 174 | 173 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)) ∧ 𝑛 ∈ ℕ) → 𝑋 ≠ ∅) | 
| 175 | 19 | adantlll 718 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)) ∧ 𝑛 ∈ ℕ) ∧ 𝑙 ∈ 𝑋) → ((𝑖‘𝑛)‘𝑙) ∈ (ℝ ×
ℝ)) | 
| 176 | 175, 20 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)) ∧ 𝑛 ∈ ℕ) ∧ 𝑙 ∈ 𝑋) → (1st ‘((𝑖‘𝑛)‘𝑙)) ∈ ℝ) | 
| 177 | 176 | fmpttd 7135 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)) ∧ 𝑛 ∈ ℕ) → (𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙))):𝑋⟶ℝ) | 
| 178 | 175, 46 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)) ∧ 𝑛 ∈ ℕ) ∧ 𝑙 ∈ 𝑋) → (2nd ‘((𝑖‘𝑛)‘𝑙)) ∈ ℝ) | 
| 179 | 178 | fmpttd 7135 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)) ∧ 𝑛 ∈ ℕ) → (𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙))):𝑋⟶ℝ) | 
| 180 | 8, 172, 174, 177, 179 | hoidmvn0val 46599 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)) ∧ 𝑛 ∈ ℕ) → ((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))(𝐿‘𝑋)(𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))) = ∏𝑘 ∈ 𝑋 (vol‘(((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)[,)((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)))) | 
| 181 | 171, 180 | eqtrd 2777 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)) ∧ 𝑛 ∈ ℕ) → (((𝐹‘𝑖)‘𝑛)(𝐿‘𝑋)((𝑆‘𝑖)‘𝑛)) = ∏𝑘 ∈ 𝑋 (vol‘(((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)[,)((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)))) | 
| 182 | 181 | mpteq2dva 5242 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)) → (𝑛 ∈ ℕ ↦ (((𝐹‘𝑖)‘𝑛)(𝐿‘𝑋)((𝑆‘𝑖)‘𝑛))) = (𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)[,)((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))‘𝑘))))) | 
| 183 | 182 | fveq2d 6910 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)) →
(Σ^‘(𝑛 ∈ ℕ ↦ (((𝐹‘𝑖)‘𝑛)(𝐿‘𝑋)((𝑆‘𝑖)‘𝑛)))) =
(Σ^‘(𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)[,)((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)))))) | 
| 184 | 183 | 3adant3 1133 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) →
(Σ^‘(𝑛 ∈ ℕ ↦ (((𝐹‘𝑖)‘𝑛)(𝐿‘𝑋)((𝑆‘𝑖)‘𝑛)))) =
(Σ^‘(𝑛 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(((𝑙 ∈ 𝑋 ↦ (1st ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)[,)((𝑙 ∈ 𝑋 ↦ (2nd ‘((𝑖‘𝑛)‘𝑙)))‘𝑘)))))) | 
| 185 |  | simp3 1139 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) → 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) | 
| 186 | 168, 184,
185 | 3eqtr4d 2787 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) →
(Σ^‘(𝑛 ∈ ℕ ↦ (((𝐹‘𝑖)‘𝑛)(𝐿‘𝑋)((𝑆‘𝑖)‘𝑛)))) = 𝑧) | 
| 187 | 186 | 3adant3l 1181 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ (𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) →
(Σ^‘(𝑛 ∈ ℕ ↦ (((𝐹‘𝑖)‘𝑛)(𝐿‘𝑋)((𝑆‘𝑖)‘𝑛)))) = 𝑧) | 
| 188 | 130, 187 | breqtrd 5169 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) ∧ (𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))) → (𝐴(𝐿‘𝑋)𝐵) ≤ 𝑧) | 
| 189 | 188 | 3exp 1120 | . . . . . . 7
⊢ (𝜑 → (𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) → ((𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) → (𝐴(𝐿‘𝑋)𝐵) ≤ 𝑧))) | 
| 190 | 189 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑀) → (𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ) → ((𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) → (𝐴(𝐿‘𝑋)𝐵) ≤ 𝑧))) | 
| 191 | 190 | rexlimdv 3153 | . . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑀) → (∃𝑖 ∈ (((ℝ × ℝ)
↑m 𝑋)
↑m ℕ)(𝐼 ⊆ ∪
𝑗 ∈ ℕ X𝑘 ∈
𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))) → (𝐴(𝐿‘𝑋)𝐵) ≤ 𝑧)) | 
| 192 | 7, 191 | mpd 15 | . . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ 𝑀) → (𝐴(𝐿‘𝑋)𝐵) ≤ 𝑧) | 
| 193 | 192 | ralrimiva 3146 | . . 3
⊢ (𝜑 → ∀𝑧 ∈ 𝑀 (𝐴(𝐿‘𝑋)𝐵) ≤ 𝑧) | 
| 194 |  | ssrab2 4080 | . . . . . 6
⊢ {𝑧 ∈ ℝ*
∣ ∃𝑖 ∈
(((ℝ × ℝ) ↑m 𝑋) ↑m ℕ)(𝐼 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑋 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 =
(Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑋 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))} ⊆
ℝ* | 
| 195 | 1, 194 | eqsstri 4030 | . . . . 5
⊢ 𝑀 ⊆
ℝ* | 
| 196 | 195 | a1i 11 | . . . 4
⊢ (𝜑 → 𝑀 ⊆
ℝ*) | 
| 197 |  | icossxr 13472 | . . . . 5
⊢
(0[,)+∞) ⊆ ℝ* | 
| 198 | 8, 9, 11, 13 | hoidmvcl 46597 | . . . . 5
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ∈ (0[,)+∞)) | 
| 199 | 197, 198 | sselid 3981 | . . . 4
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ∈
ℝ*) | 
| 200 |  | infxrgelb 13377 | . . . 4
⊢ ((𝑀 ⊆ ℝ*
∧ (𝐴(𝐿‘𝑋)𝐵) ∈ ℝ*) → ((𝐴(𝐿‘𝑋)𝐵) ≤ inf(𝑀, ℝ*, < ) ↔
∀𝑧 ∈ 𝑀 (𝐴(𝐿‘𝑋)𝐵) ≤ 𝑧)) | 
| 201 | 196, 199,
200 | syl2anc 584 | . . 3
⊢ (𝜑 → ((𝐴(𝐿‘𝑋)𝐵) ≤ inf(𝑀, ℝ*, < ) ↔
∀𝑧 ∈ 𝑀 (𝐴(𝐿‘𝑋)𝐵) ≤ 𝑧)) | 
| 202 | 193, 201 | mpbird 257 | . 2
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ≤ inf(𝑀, ℝ*, <
)) | 
| 203 | 62 | a1i 11 | . . . . 5
⊢ (𝜑 → 𝐼 = X𝑘 ∈ 𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘))) | 
| 204 |  | nfv 1914 | . . . . . 6
⊢
Ⅎ𝑘𝜑 | 
| 205 | 11 | ffvelcdmda 7104 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ) | 
| 206 | 13 | ffvelcdmda 7104 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ) | 
| 207 | 206 | rexrd 11311 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈
ℝ*) | 
| 208 | 204, 205,
207 | hoissrrn2 46593 | . . . . 5
⊢ (𝜑 → X𝑘 ∈
𝑋 ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ (ℝ ↑m 𝑋)) | 
| 209 | 203, 208 | eqsstrd 4018 | . . . 4
⊢ (𝜑 → 𝐼 ⊆ (ℝ ↑m 𝑋)) | 
| 210 | 9, 173, 209, 1 | ovnn0val 46566 | . . 3
⊢ (𝜑 → ((voln*‘𝑋)‘𝐼) = inf(𝑀, ℝ*, <
)) | 
| 211 | 210 | eqcomd 2743 | . 2
⊢ (𝜑 → inf(𝑀, ℝ*, < ) =
((voln*‘𝑋)‘𝐼)) | 
| 212 | 202, 211 | breqtrd 5169 | 1
⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) ≤ ((voln*‘𝑋)‘𝐼)) |