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⁡xy≼ω∧Disjw∈yw→x⁡⋃y=sum^⁡x↾y

Detailed syntax breakdown

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