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	|- S.2 = ( f e. ( ( 0 [,] +oo ) ^m RR ) |-> sup ( { x | E. g e. dom S.1 ( g oR <_ f /\ x = ( S.1 ` g ) ) } , RR* , < ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		citg2	|- S.2
1		vf	|- f
2		cc0	|- 0
3		cicc	|- [,]
4		cpnf	|- +oo
5	2 4 3	co	|- ( 0 [,] +oo )
6		cmap	|- ^m
7		cr	|- RR
8	5 7 6	co	|- ( ( 0 [,] +oo ) ^m RR )
9		vx	|- x
10		vg	|- g
11		citg1	|- S.1
12	11	cdm	|- dom S.1
13	10	cv	|- g
14		cle	|- <_
15	14	cofr	|- oR <_
16	1	cv	|- f
17	13 16 15	wbr	|- g oR <_ f
18	9	cv	|- x
19	13 11	cfv	|- ( S.1 ` g )
20	18 19	wceq	|- x = ( S.1 ` g )
21	17 20	wa	|- ( g oR <_ f /\ x = ( S.1 ` g ) )
22	21 10 12	wrex	|- E. g e. dom S.1 ( g oR <_ f /\ x = ( S.1 ` g ) )
23	22 9	cab	|- { x | E. g e. dom S.1 ( g oR <_ f /\ x = ( S.1 ` g ) ) }
24		cxr	|- RR*
25		clt	|- <
26	23 24 25	csup	|- sup ( { x | E. g e. dom S.1 ( g oR <_ f /\ x = ( S.1 ` g ) ) } , RR* , < )
27	1 8 26	cmpt	|- ( f e. ( ( 0 [,] +oo ) ^m RR ) |-> sup ( { x | E. g e. dom S.1 ( g oR <_ f /\ x = ( S.1 ` g ) ) } , RR* , < ) )
28	0 27	wceq	|- S.2 = ( f e. ( ( 0 [,] +oo ) ^m RR ) |-> sup ( { x | E. g e. dom S.1 ( g oR <_ f /\ x = ( S.1 ` g ) ) } , RR* , < ) )