Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mea Structured version   Visualization version   GIF version

Definition df-mea 45719
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
StepHypRef Expression
1 cmea 45718 . 2 class Meas
2 vx . . . . . . . . 9 setvar 𝑥
32cv 1532 . . . . . . . 8 class 𝑥
43cdm 5669 . . . . . . 7 class dom 𝑥
5 cc0 11109 . . . . . . . 8 class 0
6 cpnf 11246 . . . . . . . 8 class +∞
7 cicc 13330 . . . . . . . 8 class [,]
85, 6, 7co 7404 . . . . . . 7 class (0[,]+∞)
94, 8, 3wf 6532 . . . . . 6 wff 𝑥:dom 𝑥⟶(0[,]+∞)
10 csalg 45577 . . . . . . 7 class SAlg
114, 10wcel 2098 . . . . . 6 wff dom 𝑥 ∈ SAlg
129, 11wa 395 . . . . 5 wff (𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 ∈ SAlg)
13 c0 4317 . . . . . . 7 class
1413, 3cfv 6536 . . . . . 6 class (𝑥‘∅)
1514, 5wceq 1533 . . . . 5 wff (𝑥‘∅) = 0
1612, 15wa 395 . . . 4 wff ((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 ∈ SAlg) ∧ (𝑥‘∅) = 0)
17 vy . . . . . . . . 9 setvar 𝑦
1817cv 1532 . . . . . . . 8 class 𝑦
19 com 7851 . . . . . . . 8 class ω
20 cdom 8936 . . . . . . . 8 class
2118, 19, 20wbr 5141 . . . . . . 7 wff 𝑦 ≼ ω
22 vw . . . . . . . 8 setvar 𝑤
2322cv 1532 . . . . . . . 8 class 𝑤
2422, 18, 23wdisj 5106 . . . . . . 7 wff Disj 𝑤𝑦 𝑤
2521, 24wa 395 . . . . . 6 wff (𝑦 ≼ ω ∧ Disj 𝑤𝑦 𝑤)
2618cuni 4902 . . . . . . . 8 class 𝑦
2726, 3cfv 6536 . . . . . . 7 class (𝑥 𝑦)
283, 18cres 5671 . . . . . . . 8 class (𝑥𝑦)
29 csumge0 45631 . . . . . . . 8 class Σ^
3028, 29cfv 6536 . . . . . . 7 class ^‘(𝑥𝑦))
3127, 30wceq 1533 . . . . . 6 wff (𝑥 𝑦) = (Σ^‘(𝑥𝑦))
3225, 31wi 4 . . . . 5 wff ((𝑦 ≼ ω ∧ Disj 𝑤𝑦 𝑤) → (𝑥 𝑦) = (Σ^‘(𝑥𝑦)))
334cpw 4597 . . . . 5 class 𝒫 dom 𝑥
3432, 17, 33wral 3055 . . . 4 wff 𝑦 ∈ 𝒫 dom 𝑥((𝑦 ≼ ω ∧ Disj 𝑤𝑦 𝑤) → (𝑥 𝑦) = (Σ^‘(𝑥𝑦)))
3516, 34wa 395 . . 3 wff (((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 ∈ SAlg) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥((𝑦 ≼ ω ∧ Disj 𝑤𝑦 𝑤) → (𝑥 𝑦) = (Σ^‘(𝑥𝑦))))
3635, 2cab 2703 . 2 class {𝑥 ∣ (((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 ∈ SAlg) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥((𝑦 ≼ ω ∧ Disj 𝑤𝑦 𝑤) → (𝑥 𝑦) = (Σ^‘(𝑥𝑦))))}
371, 36wceq 1533 1 wff Meas = {𝑥 ∣ (((𝑥:dom 𝑥⟶(0[,]+∞) ∧ dom 𝑥 ∈ SAlg) ∧ (𝑥‘∅) = 0) ∧ ∀𝑦 ∈ 𝒫 dom 𝑥((𝑦 ≼ ω ∧ Disj 𝑤𝑦 𝑤) → (𝑥 𝑦) = (Σ^‘(𝑥𝑦))))}
Colors of variables: wff setvar class
This definition is referenced by:  ismea  45720
  Copyright terms: Public domain W3C validator