Metamath Proof Explorer

Definition df-mea

Description: Define the class of measures. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion df-mea ⊢ Meas = x | x : dom ⁡ x ⟶ 0 +∞ ∧ dom ⁡ x ∈ SAlg ∧ x ⁡ ∅ = 0 ∧ ∀ y ∈ 𝒫 dom ⁡ x y ≼ ω ∧ Disj w ∈ y w → x ⁡ ⋃ y = sum^ ⁡ x ↾ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmea class Meas
1 vx setvar x
2 1 cv setvar x
3 2 cdm class dom ⁡ x
4 cc0 class 0
5 cicc class .
6 cpnf class +∞
7 4 6 5 co class 0 +∞
8 3 7 2 wf wff x : dom ⁡ x ⟶ 0 +∞
9 csalg class SAlg
10 3 9 wcel wff dom ⁡ x ∈ SAlg
11 8 10 wa wff x : dom ⁡ x ⟶ 0 +∞ ∧ dom ⁡ x ∈ SAlg
12 c0 class ∅
13 12 2 cfv class x ⁡ ∅
14 13 4 wceq wff x ⁡ ∅ = 0
15 11 14 wa wff x : dom ⁡ x ⟶ 0 +∞ ∧ dom ⁡ x ∈ SAlg ∧ x ⁡ ∅ = 0
16 vy setvar y
17 3 cpw class 𝒫 dom ⁡ x
18 16 cv setvar y
19 cdom class ≼
20 com class ω
21 18 20 19 wbr wff y ≼ ω
22 vw setvar w
23 22 cv setvar w
24 22 18 23 wdisj wff Disj w ∈ y w
25 21 24 wa wff y ≼ ω ∧ Disj w ∈ y w
26 18 cuni class ⋃ y
27 26 2 cfv class x ⁡ ⋃ y
28 csumge0 class sum^
29 2 18 cres class x ↾ y
30 29 28 cfv class sum^ ⁡ x ↾ y
31 27 30 wceq wff x ⁡ ⋃ y = sum^ ⁡ x ↾ y
32 25 31 wi wff y ≼ ω ∧ Disj w ∈ y w → x ⁡ ⋃ y = sum^ ⁡ x ↾ y
33 32 16 17 wral wff ∀ y ∈ 𝒫 dom ⁡ x y ≼ ω ∧ Disj w ∈ y w → x ⁡ ⋃ y = sum^ ⁡ x ↾ y
34 15 33 wa wff x : dom ⁡ x ⟶ 0 +∞ ∧ dom ⁡ x ∈ SAlg ∧ x ⁡ ∅ = 0 ∧ ∀ y ∈ 𝒫 dom ⁡ x y ≼ ω ∧ Disj w ∈ y w → x ⁡ ⋃ y = sum^ ⁡ x ↾ y
35 34 1 cab class x | x : dom ⁡ x ⟶ 0 +∞ ∧ dom ⁡ x ∈ SAlg ∧ x ⁡ ∅ = 0 ∧ ∀ y ∈ 𝒫 dom ⁡ x y ≼ ω ∧ Disj w ∈ y w → x ⁡ ⋃ y = sum^ ⁡ x ↾ y
36 0 35 wceq wff Meas = x | x : dom ⁡ x ⟶ 0 +∞ ∧ dom ⁡ x ∈ SAlg ∧ x ⁡ ∅ = 0 ∧ ∀ y ∈ 𝒫 dom ⁡ x y ≼ ω ∧ Disj w ∈ y w → x ⁡ ⋃ y = sum^ ⁡ x ↾ y