Definition df-ovoln 44075

Description: Define the outer measure for the space of multidimensional real numbers. The cardinality of 𝑥 is the dimension of the space modeled. Definition 115C of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020.)

Assertion

Ref	Expression
df-ovoln	⊢ voln* = (𝑥 ∈ Fin ↦ (𝑦 ∈ 𝒫 (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, inf({𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑥) ↑m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < ))))

Distinct variable group:   𝑥,𝑦,𝑧,𝑖,𝑗,𝑘

Detailed syntax breakdown of Definition df-ovoln

Step	Hyp	Ref	Expression
1		covoln 44074	. 2 class voln*
2		vx	. . 3 setvar 𝑥
3		cfn 8733	. . 3 class Fin
4		vy	. . . 4 setvar 𝑦
5		cr 10870	. . . . . 6 class ℝ
6	2	cv 1538	. . . . . 6 class 𝑥
7		cmap 8615	. . . . . 6 class ↑m
8	5, 6, 7	co 7275	. . . . 5 class (ℝ ↑m 𝑥)
9	8	cpw 4533	. . . 4 class 𝒫 (ℝ ↑m 𝑥)
10		c0 4256	. . . . . 6 class ∅
11	6, 10	wceq 1539	. . . . 5 wff 𝑥 = ∅
12		cc0 10871	. . . . 5 class 0
13	4	cv 1538	. . . . . . . . . 10 class 𝑦
14		vj	. . . . . . . . . . 11 setvar 𝑗
15		cn 11973	. . . . . . . . . . 11 class ℕ
16		vk	. . . . . . . . . . . 12 setvar 𝑘
17	16	cv 1538	. . . . . . . . . . . . 13 class 𝑘
18		cico 13081	. . . . . . . . . . . . . 14 class [,)
19	14	cv 1538	. . . . . . . . . . . . . . 15 class 𝑗
20		vi	. . . . . . . . . . . . . . . 16 setvar 𝑖
21	20	cv 1538	. . . . . . . . . . . . . . 15 class 𝑖
22	19, 21	cfv 6433	. . . . . . . . . . . . . 14 class (𝑖‘𝑗)
23	18, 22	ccom 5593	. . . . . . . . . . . . 13 class ([,) ∘ (𝑖‘𝑗))
24	17, 23	cfv 6433	. . . . . . . . . . . 12 class (([,) ∘ (𝑖‘𝑗))‘𝑘)
25	16, 6, 24	cixp 8685	. . . . . . . . . . 11 class X𝑘 ∈ 𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘)
26	14, 15, 25	ciun 4924	. . . . . . . . . 10 class ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘)
27	13, 26	wss 3887	. . . . . . . . 9 wff 𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘)
28		vz	. . . . . . . . . . 11 setvar 𝑧
29	28	cv 1538	. . . . . . . . . 10 class 𝑧
30		cvol 24627	. . . . . . . . . . . . . 14 class vol
31	24, 30	cfv 6433	. . . . . . . . . . . . 13 class (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))
32	6, 31, 16	cprod 15615	. . . . . . . . . . . 12 class ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))
33	14, 15, 32	cmpt 5157	. . . . . . . . . . 11 class (𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))
34		csumge0 43900	. . . . . . . . . . 11 class Σ^
35	33, 34	cfv 6433	. . . . . . . . . 10 class (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))
36	29, 35	wceq 1539	. . . . . . . . 9 wff 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘))))
37	27, 36	wa 396	. . . . . . . 8 wff (𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))
38	5, 5	cxp 5587	. . . . . . . . . 10 class (ℝ × ℝ)
39	38, 6, 7	co 7275	. . . . . . . . 9 class ((ℝ × ℝ) ↑m 𝑥)
40	39, 15, 7	co 7275	. . . . . . . 8 class (((ℝ × ℝ) ↑m 𝑥) ↑m ℕ)
41	37, 20, 40	wrex 3065	. . . . . . 7 wff ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑥) ↑m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))
42		cxr 11008	. . . . . . 7 class ℝ*
43	41, 28, 42	crab 3068	. . . . . 6 class {𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑥) ↑m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}
44		clt 11009	. . . . . 6 class <
45	43, 42, 44	cinf 9200	. . . . 5 class inf({𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑥) ↑m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < )
46	11, 12, 45	cif 4459	. . . 4 class if(𝑥 = ∅, 0, inf({𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑥) ↑m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < ))
47	4, 9, 46	cmpt 5157	. . 3 class (𝑦 ∈ 𝒫 (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, inf({𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑥) ↑m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < )))
48	2, 3, 47	cmpt 5157	. 2 class (𝑥 ∈ Fin ↦ (𝑦 ∈ 𝒫 (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, inf({𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑥) ↑m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < ))))
49	1, 48	wceq 1539	1 wff voln* = (𝑥 ∈ Fin ↦ (𝑦 ∈ 𝒫 (ℝ ↑m 𝑥) ↦ if(𝑥 = ∅, 0, inf({𝑧 ∈ ℝ* ∣ ∃𝑖 ∈ (((ℝ × ℝ) ↑m 𝑥) ↑m ℕ)(𝑦 ⊆ ∪ 𝑗 ∈ ℕ X𝑘 ∈ 𝑥 (([,) ∘ (𝑖‘𝑗))‘𝑘) ∧ 𝑧 = (Σ^‘(𝑗 ∈ ℕ ↦ ∏𝑘 ∈ 𝑥 (vol‘(([,) ∘ (𝑖‘𝑗))‘𝑘)))))}, ℝ*, < ))))

This definition is referenced by:  ovnval  44079