Definition df-oms 31821

Description: Define a function constructing an outer measure. See omsval 31822 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 31820	. 2 class toOMeas
2		vr	. . 3 setvar 𝑟
3		cvv 3397	. . 3 class V
4		va	. . . 4 setvar 𝑎
5	2	cv 1541	. . . . . . 7 class 𝑟
6	5	cdm 5519	. . . . . 6 class dom 𝑟
7	6	cuni 4793	. . . . 5 class ∪ dom 𝑟
8	7	cpw 4485	. . . 4 class 𝒫 ∪ dom 𝑟
9		vx	. . . . . . 7 setvar 𝑥
10	4	cv 1541	. . . . . . . . . 10 class 𝑎
11		vz	. . . . . . . . . . . 12 setvar 𝑧
12	11	cv 1541	. . . . . . . . . . 11 class 𝑧
13	12	cuni 4793	. . . . . . . . . 10 class ∪ 𝑧
14	10, 13	wss 3841	. . . . . . . . 9 wff 𝑎 ⊆ ∪ 𝑧
15		com 7593	. . . . . . . . . 10 class ω
16		cdom 8546	. . . . . . . . . 10 class ≼
17	12, 15, 16	wbr 5027	. . . . . . . . 9 wff 𝑧 ≼ ω
18	14, 17	wa 399	. . . . . . . 8 wff (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)
19	6	cpw 4485	. . . . . . . 8 class 𝒫 dom 𝑟
20	18, 11, 19	crab 3057	. . . . . . 7 class {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)}
21	9	cv 1541	. . . . . . . 8 class 𝑥
22		vy	. . . . . . . . . 10 setvar 𝑦
23	22	cv 1541	. . . . . . . . 9 class 𝑦
24	23, 5	cfv 6333	. . . . . . . 8 class (𝑟‘𝑦)
25	21, 24, 22	cesum 31557	. . . . . . 7 class Σ*𝑦 ∈ 𝑥(𝑟‘𝑦)
26	9, 20, 25	cmpt 5107	. . . . . 6 class (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑟‘𝑦))
27	26	crn 5520	. . . . 5 class ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑟‘𝑦))
28		cc0 10608	. . . . . 6 class 0
29		cpnf 10743	. . . . . 6 class +∞
30		cicc 12817	. . . . . 6 class [,]
31	28, 29, 30	co 7164	. . . . 5 class (0[,]+∞)
32		clt 10746	. . . . 5 class <
33	27, 31, 32	cinf 8971	. . . 4 class inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑟‘𝑦)), (0[,]+∞), < )
34	4, 8, 33	cmpt 5107	. . 3 class (𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑟‘𝑦)), (0[,]+∞), < ))
35	2, 3, 34	cmpt 5107	. 2 class (𝑟 ∈ V ↦ (𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑟‘𝑦)), (0[,]+∞), < )))
36	1, 35	wceq 1542	1 wff toOMeas = (𝑟 ∈ V ↦ (𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf(ran (𝑥 ∈ {𝑧 ∈ 𝒫 dom 𝑟 ∣ (𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω)} ↦ Σ*𝑦 ∈ 𝑥(𝑟‘𝑦)), (0[,]+∞), < )))

This definition is referenced by:  omsval  31822