Definition df-mea

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmea	⊢ Meas
1		vx	⊢ 𝑥
2	1	cv	⊢ 𝑥
3	2	cdm	⊢ dom 𝑥
4		cc0	⊢ 0
5		cicc	⊢ [,]
6		cpnf	⊢ +∞
7	4 6 5	co	⊢ ( 0 [,] +∞ )
8	3 7 2	wf	⊢ 𝑥 : dom 𝑥 ⟶ ( 0 [,] +∞ )
9		csalg	⊢ SAlg
10	3 9	wcel	⊢ dom 𝑥 ∈ SAlg
11	8 10	wa	⊢ ( 𝑥 : dom 𝑥 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑥 ∈ SAlg )
12		c0	⊢ ∅
13	12 2	cfv	⊢ ( 𝑥 ‘ ∅ )
14	13 4	wceq	⊢ ( 𝑥 ‘ ∅ ) = 0
15	11 14	wa	⊢ ( ( 𝑥 : dom 𝑥 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑥 ∈ SAlg ) ∧ ( 𝑥 ‘ ∅ ) = 0 )
16		vy	⊢ 𝑦
17	3	cpw	⊢ 𝒫 dom 𝑥
18	16	cv	⊢ 𝑦
19		cdom	⊢ ≼
20		com	⊢ ω
21	18 20 19	wbr	⊢ 𝑦 ≼ ω
22		vw	⊢ 𝑤
23	22	cv	⊢ 𝑤
24	22 18 23	wdisj	⊢ Disj 𝑤 ∈ 𝑦 𝑤
25	21 24	wa	⊢ ( 𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤 )
26	18	cuni	⊢ ∪ 𝑦
27	26 2	cfv	⊢ ( 𝑥 ‘ ∪ 𝑦 )
28		csumge0	⊢ Σ^
29	2 18	cres	⊢ ( 𝑥 ↾ 𝑦 )
30	29 28	cfv	⊢ ( Σ^ ‘ ( 𝑥 ↾ 𝑦 ) )
31	27 30	wceq	⊢ ( 𝑥 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑥 ↾ 𝑦 ) )
32	25 31	wi	⊢ ( ( 𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) → ( 𝑥 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑥 ↾ 𝑦 ) ) )
33	32 16 17	wral	⊢ ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( ( 𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) → ( 𝑥 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑥 ↾ 𝑦 ) ) )
34	15 33	wa	⊢ ( ( ( 𝑥 : dom 𝑥 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑥 ∈ SAlg ) ∧ ( 𝑥 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( ( 𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) → ( 𝑥 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑥 ↾ 𝑦 ) ) ) )
35	34 1	cab	⊢ { 𝑥 ∣ ( ( ( 𝑥 : dom 𝑥 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑥 ∈ SAlg ) ∧ ( 𝑥 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( ( 𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) → ( 𝑥 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑥 ↾ 𝑦 ) ) ) ) }
36	0 35	wceq	⊢ Meas = { 𝑥 ∣ ( ( ( 𝑥 : dom 𝑥 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑥 ∈ SAlg ) ∧ ( 𝑥 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑥 ( ( 𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) → ( 𝑥 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑥 ↾ 𝑦 ) ) ) ) }