Definition df-oms

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		coms	⊢ toOMeas
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		va	⊢ 𝑎
4	1	cv	⊢ 𝑟
5	4	cdm	⊢ dom 𝑟
6	5	cuni	⊢ ∪ dom 𝑟
7	6	cpw	⊢ 𝒫 ∪ dom 𝑟
8		vx	⊢ 𝑥
9		vz	⊢ 𝑧
10	5	cpw	⊢ 𝒫 dom 𝑟
11	3	cv	⊢ 𝑎
12	9	cv	⊢ 𝑧
13	12	cuni	⊢ ∪ 𝑧
14	11 13	wss	⊢ 𝑎 ⊆ ∪ 𝑧
15		cdom	⊢ ≼
16		com	⊢ ω
17	12 16 15	wbr	⊢ 𝑧 ≼ ω
18	14 17	wa	⊢ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω )
19	18 9 10	crab	⊢ { 𝑧 ∈ 𝒫 dom 𝑟 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) }
20		vy	⊢ 𝑦
21	8	cv	⊢ 𝑥
22	20	cv	⊢ 𝑦
23	22 4	cfv	⊢ ( 𝑟 ‘ 𝑦 )
24	21 23 20	cesum	⊢ Σ* 𝑦 ∈ 𝑥 ( 𝑟 ‘ 𝑦 )
25	8 19 24	cmpt	⊢ ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑟 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑟 ‘ 𝑦 ) )
26	25	crn	⊢ ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑟 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑟 ‘ 𝑦 ) )
27		cc0	⊢ 0
28		cicc	⊢ [,]
29		cpnf	⊢ +∞
30	27 29 28	co	⊢ ( 0 [,] +∞ )
31		clt	⊢ <
32	26 30 31	cinf	⊢ inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑟 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑟 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < )
33	3 7 32	cmpt	⊢ ( 𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑟 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑟 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < ) )
34	1 2 33	cmpt	⊢ ( 𝑟 ∈ V ↦ ( 𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑟 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑟 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < ) ) )
35	0 34	wceq	⊢ toOMeas = ( 𝑟 ∈ V ↦ ( 𝑎 ∈ 𝒫 ∪ dom 𝑟 ↦ inf ( ran ( 𝑥 ∈ { 𝑧 ∈ 𝒫 dom 𝑟 ∣ ( 𝑎 ⊆ ∪ 𝑧 ∧ 𝑧 ≼ ω ) } ↦ Σ* 𝑦 ∈ 𝑥 ( 𝑟 ‘ 𝑦 ) ) , ( 0 [,] +∞ ) , < ) ) )