Definition df-oms 32259

Description: Define a function constructing an outer measure. See omsval 32260 for its value. Definition 1.5 of [Bogachev] p. 16. (Contributed by Thierry Arnoux, 15-Sep-2019.) (Revised by AV, 4-Oct-2020.)

Assertion

Ref	Expression
df-oms	⊢ toOMeas = (𝑟 ∈ V ↦ (𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑟‘𝑦)), (0[,]+∞), < )))

Distinct variable group:   𝑟,𝑎,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-oms

Step	Hyp	Ref	Expression
1		coms 32258	. 2 class toOMeas
2		vr	. . 3 setvar 𝑟
3		cvv 3432	. . 3 class V
4		va	. . . 4 setvar 𝑎
5	2	cv 1538	. . . . . . 7 class 𝑟
6	5	cdm 5589	. . . . . 6 class dom 𝑟
7	6	cuni 4839	. . . . 5 class ∪ dom 𝑟
8	7	cpw 4533	. . . 4 class 𝒫 ∪ dom 𝑟
9		vx	. . . . . . 7 setvar 𝑥
10	4	cv 1538	. . . . . . . . . 10 class 𝑎
11		vz	. . . . . . . . . . . 12 setvar 𝑧
12	11	cv 1538	. . . . . . . . . . 11 class 𝑧
13	12	cuni 4839	. . . . . . . . . 10 class ∪ 𝑧
14	10, 13	wss 3887	. . . . . . . . 9 wff 𝑎 ⊆ ∪ 𝑧
15		com 7712	. . . . . . . . . 10 class ω
16		cdom 8731	. . . . . . . . . 10 class ≼
17	12, 15, 16	wbr 5074	. . . . . . . . 9 wff 𝑧 ≼ ω
18	14, 17	wa 396	. . . . . . . 8 wff (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)
19	6	cpw 4533	. . . . . . . 8 class 𝒫 dom 𝑟
20	18, 11, 19	crab 3068	. . . . . . 7 class {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}
21	9	cv 1538	. . . . . . . 8 class 𝑥
22		vy	. . . . . . . . . 10 setvar 𝑦
23	22	cv 1538	. . . . . . . . 9 class 𝑦
24	23, 5	cfv 6433	. . . . . . . 8 class (𝑟‘𝑦)
25	21, 24, 22	cesum 31995	. . . . . . 7 class Σ*𝑦 ∈ 𝑥(𝑟‘𝑦)
26	9, 20, 25	cmpt 5157	. . . . . 6 class (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑟‘𝑦))
27	26	crn 5590	. . . . 5 class ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑟‘𝑦))
28		cc0 10871	. . . . . 6 class 0
29		cpnf 11006	. . . . . 6 class +∞
30		cicc 13082	. . . . . 6 class [,]
31	28, 29, 30	co 7275	. . . . 5 class (0[,]+∞)
32		clt 11009	. . . . 5 class <
33	27, 31, 32	cinf 9200	. . . 4 class inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑟‘𝑦)), (0[,]+∞), < )
34	4, 8, 33	cmpt 5157	. . 3 class (𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑟‘𝑦)), (0[,]+∞), < ))
35	2, 3, 34	cmpt 5157	. 2 class (𝑟 ∈ V ↦ (𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑟‘𝑦)), (0[,]+∞), < )))
36	1, 35	wceq 1539	1 wff toOMeas = (𝑟 ∈ V ↦ (𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑟‘𝑦)), (0[,]+∞), < )))

This definition is referenced by:  omsval  32260