Definition df-itg2

Description: Define the Lebesgue integral for nonnegative functions. A nonnegative function's integral is the supremum of the integrals of all simple functions that are less than the input function. Note that this may be +oo for functions that take the value +oo on a set of positive measure or functions that are bounded below by a positive number on a set of infinite measure. (Contributed by Mario Carneiro, 28-Jun-2014)

	Ref	Expression
Assertion	df-itg2	⊢ ∫2 = ( 𝑓 ∈ ( ( 0 [,] +∞ ) ↑m ℝ ) ↦ sup ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝑓 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } , ℝ* , < ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		citg2	⊢ ∫2
1		vf	⊢ 𝑓
2		cc0	⊢ 0
3		cicc	⊢ [,]
4		cpnf	⊢ +∞
5	2 4 3	co	⊢ ( 0 [,] +∞ )
6		cmap	⊢ ↑m
7		cr	⊢ ℝ
8	5 7 6	co	⊢ ( ( 0 [,] +∞ ) ↑m ℝ )
9		vx	⊢ 𝑥
10		vg	⊢ 𝑔
11		citg1	⊢ ∫1
12	11	cdm	⊢ dom ∫1
13	10	cv	⊢ 𝑔
14		cle	⊢ ≤
15	14	cofr	⊢ ∘r ≤
16	1	cv	⊢ 𝑓
17	13 16 15	wbr	⊢ 𝑔 ∘r ≤ 𝑓
18	9	cv	⊢ 𝑥
19	13 11	cfv	⊢ ( ∫1 ‘ 𝑔 )
20	18 19	wceq	⊢ 𝑥 = ( ∫1 ‘ 𝑔 )
21	17 20	wa	⊢ ( 𝑔 ∘r ≤ 𝑓 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) )
22	21 10 12	wrex	⊢ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝑓 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) )
23	22 9	cab	⊢ { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝑓 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) }
24		cxr	⊢ ℝ*
25		clt	⊢ <
26	23 24 25	csup	⊢ sup ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝑓 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } , ℝ* , < )
27	1 8 26	cmpt	⊢ ( 𝑓 ∈ ( ( 0 [,] +∞ ) ↑m ℝ ) ↦ sup ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝑓 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } , ℝ* , < ) )
28	0 27	wceq	⊢ ∫2 = ( 𝑓 ∈ ( ( 0 [,] +∞ ) ↑m ℝ ) ↦ sup ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝑓 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } , ℝ* , < ) )