Definition df-itg2 23390

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.)

Assertion

Ref	Expression
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* , < ) )

Distinct variable group:   f, g, x

Detailed syntax breakdown of Definition df-itg2

Step	Hyp	Ref	Expression
1		citg2 23385	. 2 class S.2
2		vf	. . 3 setvar f
3		cc0 9936	. . . . 5 class 0
4		cpnf 10071	. . . . 5 class +oo
5		cicc 12178	. . . . 5 class [,]
6	3, 4, 5	co 6650	. . . 4 class ( 0 [,] +oo )
7		cr 9935	. . . 4 class RR
8		cmap 7857	. . . 4 class ^m
9	6, 7, 8	co 6650	. . 3 class ( ( 0 [,] +oo ) ^m RR )
10		vg	. . . . . . . . 9 setvar g
11	10	cv 1482	. . . . . . . 8 class g
12	2	cv 1482	. . . . . . . 8 class f
13		cle 10075	. . . . . . . . 9 class <_
14	13	cofr 6896	. . . . . . . 8 class oR <_
15	11, 12, 14	wbr 4653	. . . . . . 7 wff g oR <_ f
16		vx	. . . . . . . . 9 setvar x
17	16	cv 1482	. . . . . . . 8 class x
18		citg1 23384	. . . . . . . . 9 class S.1
19	11, 18	cfv 5888	. . . . . . . 8 class ( S.1 ` g )
20	17, 19	wceq 1483	. . . . . . 7 wff x = ( S.1 ` g )
21	15, 20	wa 384	. . . . . 6 wff ( g oR <_ f /\ x = ( S.1 ` g ) )
22	18	cdm 5114	. . . . . 6 class dom S.1
23	21, 10, 22	wrex 2913	. . . . 5 wff E. g e. dom S.1 ( g oR <_ f /\ x = ( S.1 ` g ) )
24	23, 16	cab 2608	. . . 4 class { x | E. g e. dom S.1 ( g oR <_ f /\ x = ( S.1 ` g ) ) }
25		cxr 10073	. . . 4 class RR*
26		clt 10074	. . . 4 class <
27	24, 25, 26	csup 8346	. . 3 class sup ( { x | E. g e. dom S.1 ( g oR <_ f /\ x = ( S.1 ` g ) ) } , RR* , < )
28	2, 9, 27	cmpt 4729	. 2 class ( f e. ( ( 0 [,] +oo ) ^m RR ) |-> sup ( { x | E. g e. dom S.1 ( g oR <_ f /\ x = ( S.1 ` g ) ) } , RR* , < ) )
29	1, 28	wceq 1483	1 wff S.2 = ( f e. ( ( 0 [,] +oo ) ^m RR ) |-> sup ( { x | E. g e. dom S.1 ( g oR <_ f /\ x = ( S.1 ` g ) ) } , RR* , < ) )

This definition is referenced by:  itg2val  23495