Definition df-mea 43878

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

Assertion

Ref	Expression
df-mea	⊢ Meas = {𝑥 ∣ (((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 ∈ SAlg) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥((𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤) → (𝑥‘∪ 𝑦) = (Σ^‘(𝑥 ↾ 𝑦))))}

Distinct variable group:   𝑥,𝑤,𝑦

Detailed syntax breakdown of Definition df-mea

Step	Hyp	Ref	Expression
1		cmea 43877	. 2 class Meas
2		vx	. . . . . . . . 9 setvar 𝑥
3	2	cv 1538	. . . . . . . 8 class 𝑥
4	3	cdm 5580	. . . . . . 7 class dom 𝑥
5		cc0 10802	. . . . . . . 8 class 0
6		cpnf 10937	. . . . . . . 8 class +∞
7		cicc 13011	. . . . . . . 8 class [,]
8	5, 6, 7	co 7255	. . . . . . 7 class (0[,]+∞)
9	4, 8, 3	wf 6414	. . . . . 6 wff 𝑥:dom 𝑥⟶(0[,]+∞)
10		csalg 43739	. . . . . . 7 class SAlg
11	4, 10	wcel 2108	. . . . . 6 wff dom 𝑥 ∈ SAlg
12	9, 11	wa 395	. . . . 5 wff (𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 ∈ SAlg)
13		c0 4253	. . . . . . 7 class ∅
14	13, 3	cfv 6418	. . . . . 6 class (𝑥‘∅)
15	14, 5	wceq 1539	. . . . 5 wff (𝑥‘∅) = 0
16	12, 15	wa 395	. . . 4 wff ((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 ∈ SAlg) ∧ (𝑥‘∅) = 0)
17		vy	. . . . . . . . 9 setvar 𝑦
18	17	cv 1538	. . . . . . . 8 class 𝑦
19		com 7687	. . . . . . . 8 class ω
20		cdom 8689	. . . . . . . 8 class ≼
21	18, 19, 20	wbr 5070	. . . . . . 7 wff 𝑦 ≼ ω
22		vw	. . . . . . . 8 setvar 𝑤
23	22	cv 1538	. . . . . . . 8 class 𝑤
24	22, 18, 23	wdisj 5035	. . . . . . 7 wff Disj 𝑤 ∈ 𝑦 𝑤
25	21, 24	wa 395	. . . . . 6 wff (𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤)
26	18	cuni 4836	. . . . . . . 8 class ∪ 𝑦
27	26, 3	cfv 6418	. . . . . . 7 class (𝑥‘∪ 𝑦)
28	3, 18	cres 5582	. . . . . . . 8 class (𝑥 ↾ 𝑦)
29		csumge0 43790	. . . . . . . 8 class Σ^
30	28, 29	cfv 6418	. . . . . . 7 class (Σ^‘(𝑥 ↾ 𝑦))
31	27, 30	wceq 1539	. . . . . 6 wff (𝑥‘∪ 𝑦) = (Σ^‘(𝑥 ↾ 𝑦))
32	25, 31	wi 4	. . . . 5 wff ((𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤) → (𝑥‘∪ 𝑦) = (Σ^‘(𝑥 ↾ 𝑦)))
33	4	cpw 4530	. . . . 5 class 𝒫 dom 𝑥
34	32, 17, 33	wral 3063	. . . 4 wff ∀𝑦 ∈ 𝒫 dom 𝑥((𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤) → (𝑥‘∪ 𝑦) = (Σ^‘(𝑥 ↾ 𝑦)))
35	16, 34	wa 395	. . 3 wff (((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 ∈ SAlg) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥((𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤) → (𝑥‘∪ 𝑦) = (Σ^‘(𝑥 ↾ 𝑦))))
36	35, 2	cab 2715	. 2 class {𝑥 ∣ (((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 ∈ SAlg) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥((𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤) → (𝑥‘∪ 𝑦) = (Σ^‘(𝑥 ↾ 𝑦))))}
37	1, 36	wceq 1539	1 wff Meas = {𝑥 ∣ (((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 ∈ SAlg) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥((𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤) → (𝑥‘∪ 𝑦) = (Σ^‘(𝑥 ↾ 𝑦))))}

This definition is referenced by:  ismea  43879