Metamath Proof Explorer

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 = r ∈ V ⟼ a ∈ 𝒫 ⋃ dom ⁡ r ⟼ inf ran ⁡ x ∈ z ∈ 𝒫 dom ⁡ r | a ⊆ ⋃ z ∧ z ≼ ω ⟼ ∑ * y ∈ x r ⁡ y 0 +∞ <

Detailed syntax breakdown

Step Hyp Ref Expression
0 coms class toOMeas
1 vr setvar r
2 cvv class V
3 va setvar a
4 1 cv setvar r
5 4 cdm class dom ⁡ r
6 5 cuni class ⋃ dom ⁡ r
7 6 cpw class 𝒫 ⋃ dom ⁡ r
8 vx setvar x
9 vz setvar z
10 5 cpw class 𝒫 dom ⁡ r
11 3 cv setvar a
12 9 cv setvar z
13 12 cuni class ⋃ z
14 11 13 wss wff a ⊆ ⋃ z
15 cdom class ≼
16 com class ω
17 12 16 15 wbr wff z ≼ ω
18 14 17 wa wff a ⊆ ⋃ z ∧ z ≼ ω
19 18 9 10 crab class z ∈ 𝒫 dom ⁡ r | a ⊆ ⋃ z ∧ z ≼ ω
20 vy setvar y
21 8 cv setvar x
22 20 cv setvar y
23 22 4 cfv class r ⁡ y
24 21 23 20 cesum class ∑ * y ∈ x r ⁡ y
25 8 19 24 cmpt class x ∈ z ∈ 𝒫 dom ⁡ r | a ⊆ ⋃ z ∧ z ≼ ω ⟼ ∑ * y ∈ x r ⁡ y
26 25 crn class ran ⁡ x ∈ z ∈ 𝒫 dom ⁡ r | a ⊆ ⋃ z ∧ z ≼ ω ⟼ ∑ * y ∈ x r ⁡ y
27 cc0 class 0
28 cicc class .
29 cpnf class +∞
30 27 29 28 co class 0 +∞
31 clt class <
32 26 30 31 cinf class inf ran ⁡ x ∈ z ∈ 𝒫 dom ⁡ r | a ⊆ ⋃ z ∧ z ≼ ω ⟼ ∑ * y ∈ x r ⁡ y 0 +∞ <
33 3 7 32 cmpt class a ∈ 𝒫 ⋃ dom ⁡ r ⟼ inf ran ⁡ x ∈ z ∈ 𝒫 dom ⁡ r | a ⊆ ⋃ z ∧ z ≼ ω ⟼ ∑ * y ∈ x r ⁡ y 0 +∞ <
34 1 2 33 cmpt class r ∈ V ⟼ a ∈ 𝒫 ⋃ dom ⁡ r ⟼ inf ran ⁡ x ∈ z ∈ 𝒫 dom ⁡ r | a ⊆ ⋃ z ∧ z ≼ ω ⟼ ∑ * y ∈ x r ⁡ y 0 +∞ <
35 0 34 wceq wff toOMeas = r ∈ V ⟼ a ∈ 𝒫 ⋃ dom ⁡ r ⟼ inf ran ⁡ x ∈ z ∈ 𝒫 dom ⁡ r | a ⊆ ⋃ z ∧ z ≼ ω ⟼ ∑ * y ∈ x r ⁡ y 0 +∞ <