Definition df-oms 30354

Description: Define a function constructing an outer measure. See omsval 30355 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 30353	. 2 class toOMeas
2		vr	. . 3 setvar 𝑟
3		cvv 3200	. . 3 class V
4		va	. . . 4 setvar 𝑎
5	2	cv 1482	. . . . . . 7 class 𝑟
6	5	cdm 5114	. . . . . 6 class dom 𝑟
7	6	cuni 4436	. . . . 5 class ∪ dom 𝑟
8	7	cpw 4158	. . . 4 class 𝒫 ∪ dom 𝑟
9		vx	. . . . . . 7 setvar 𝑥
10	4	cv 1482	. . . . . . . . . 10 class 𝑎
11		vz	. . . . . . . . . . . 12 setvar 𝑧
12	11	cv 1482	. . . . . . . . . . 11 class 𝑧
13	12	cuni 4436	. . . . . . . . . 10 class ∪ 𝑧
14	10, 13	wss 3574	. . . . . . . . 9 wff 𝑎 ⊆ ∪ 𝑧
15		com 7065	. . . . . . . . . 10 class ω
16		cdom 7953	. . . . . . . . . 10 class ≼
17	12, 15, 16	wbr 4653	. . . . . . . . 9 wff 𝑧 ≼ ω
18	14, 17	wa 384	. . . . . . . 8 wff (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)
19	6	cpw 4158	. . . . . . . 8 class 𝒫 dom 𝑟
20	18, 11, 19	crab 2916	. . . . . . 7 class {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}
21	9	cv 1482	. . . . . . . 8 class 𝑥
22		vy	. . . . . . . . . 10 setvar 𝑦
23	22	cv 1482	. . . . . . . . 9 class 𝑦
24	23, 5	cfv 5888	. . . . . . . 8 class (𝑟‘𝑦)
25	21, 24, 22	cesum 30089	. . . . . . 7 class Σ*𝑦 ∈ 𝑥(𝑟‘𝑦)
26	9, 20, 25	cmpt 4729	. . . . . 6 class (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑟‘𝑦))
27	26	crn 5115	. . . . 5 class ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑟‘𝑦))
28		cc0 9936	. . . . . 6 class 0
29		cpnf 10071	. . . . . 6 class +∞
30		cicc 12178	. . . . . 6 class [,]
31	28, 29, 30	co 6650	. . . . 5 class (0[,]+∞)
32		clt 10074	. . . . 5 class <
33	27, 31, 32	cinf 8347	. . . 4 class inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑟‘𝑦)), (0[,]+∞), < )
34	4, 8, 33	cmpt 4729	. . 3 class (𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑟‘𝑦)), (0[,]+∞), < ))
35	2, 3, 34	cmpt 4729	. 2 class (𝑟 ∈ V ↦ (𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑟‘𝑦)), (0[,]+∞), < )))
36	1, 35	wceq 1483	1 wff toOMeas = (𝑟 ∈ V ↦ (𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑟‘𝑦)), (0[,]+∞), < )))

This definition is referenced by:  omsval  30355