Definition df-meas

Description: Define a measure as a nonnegative countably additive function over a sigma-algebra onto ( 0 , +oo ) . (Contributed by Thierry Arnoux, 10-Sep-2016)

	Ref	Expression
Assertion	df-meas	⊢ measures = ( 𝑠 ∈ ∪ ran sigAlgebra ↦ { 𝑚 ∣ ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmeas	⊢ measures
1		vs	⊢ 𝑠
2		csiga	⊢ sigAlgebra
3	2	crn	⊢ ran sigAlgebra
4	3	cuni	⊢ ∪ ran sigAlgebra
5		vm	⊢ 𝑚
6	5	cv	⊢ 𝑚
7	1	cv	⊢ 𝑠
8		cc0	⊢ 0
9		cicc	⊢ [,]
10		cpnf	⊢ +∞
11	8 10 9	co	⊢ ( 0 [,] +∞ )
12	7 11 6	wf	⊢ 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ )
13		c0	⊢ ∅
14	13 6	cfv	⊢ ( 𝑚 ‘ ∅ )
15	14 8	wceq	⊢ ( 𝑚 ‘ ∅ ) = 0
16		vx	⊢ 𝑥
17	7	cpw	⊢ 𝒫 𝑠
18	16	cv	⊢ 𝑥
19		cdom	⊢ ≼
20		com	⊢ ω
21	18 20 19	wbr	⊢ 𝑥 ≼ ω
22		vy	⊢ 𝑦
23	22	cv	⊢ 𝑦
24	22 18 23	wdisj	⊢ Disj 𝑦 ∈ 𝑥 𝑦
25	21 24	wa	⊢ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 )
26	18	cuni	⊢ ∪ 𝑥
27	26 6	cfv	⊢ ( 𝑚 ‘ ∪ 𝑥 )
28	23 6	cfv	⊢ ( 𝑚 ‘ 𝑦 )
29	18 28 22	cesum	⊢ Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 )
30	27 29	wceq	⊢ ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 )
31	25 30	wi	⊢ ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) )
32	31 16 17	wral	⊢ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) )
33	12 15 32	w3a	⊢ ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) )
34	33 5	cab	⊢ { 𝑚 ∣ ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) }
35	1 4 34	cmpt	⊢ ( 𝑠 ∈ ∪ ran sigAlgebra ↦ { 𝑚 ∣ ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) } )
36	0 35	wceq	⊢ measures = ( 𝑠 ∈ ∪ ran sigAlgebra ↦ { 𝑚 ∣ ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) } )