Definition df-itg2 23794

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 +∞ for functions that take the value +∞ 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	⊢ ∫2 = (𝑓 ∈ ((0[,]+∞) ↑𝑚 ℝ) ↦ sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ 𝑓 ∧ 𝑥 = (∫1‘𝑔))}, ℝ*, < ))

Distinct variable group:   𝑓,𝑔,𝑥

Detailed syntax breakdown of Definition df-itg2

Step	Hyp	Ref	Expression
1		citg2 23789	. 2 class ∫2
2		vf	. . 3 setvar 𝑓
3		cc0 10259	. . . . 5 class 0
4		cpnf 10395	. . . . 5 class +∞
5		cicc 12473	. . . . 5 class [,]
6	3, 4, 5	co 6910	. . . 4 class (0[,]+∞)
7		cr 10258	. . . 4 class ℝ
8		cmap 8127	. . . 4 class ↑𝑚
9	6, 7, 8	co 6910	. . 3 class ((0[,]+∞) ↑𝑚 ℝ)
10		vg	. . . . . . . . 9 setvar 𝑔
11	10	cv 1655	. . . . . . . 8 class 𝑔
12	2	cv 1655	. . . . . . . 8 class 𝑓
13		cle 10399	. . . . . . . . 9 class ≤
14	13	cofr 7161	. . . . . . . 8 class ∘𝑟 ≤
15	11, 12, 14	wbr 4875	. . . . . . 7 wff 𝑔 ∘𝑟 ≤ 𝑓
16		vx	. . . . . . . . 9 setvar 𝑥
17	16	cv 1655	. . . . . . . 8 class 𝑥
18		citg1 23788	. . . . . . . . 9 class ∫1
19	11, 18	cfv 6127	. . . . . . . 8 class (∫1‘𝑔)
20	17, 19	wceq 1656	. . . . . . 7 wff 𝑥 = (∫1‘𝑔)
21	15, 20	wa 386	. . . . . 6 wff (𝑔 ∘𝑟 ≤ 𝑓 ∧ 𝑥 = (∫1‘𝑔))
22	18	cdm 5346	. . . . . 6 class dom ∫1
23	21, 10, 22	wrex 3118	. . . . 5 wff ∃𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ 𝑓 ∧ 𝑥 = (∫1‘𝑔))
24	23, 16	cab 2811	. . . 4 class {𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ 𝑓 ∧ 𝑥 = (∫1‘𝑔))}
25		cxr 10397	. . . 4 class ℝ*
26		clt 10398	. . . 4 class <
27	24, 25, 26	csup 8621	. . 3 class sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ 𝑓 ∧ 𝑥 = (∫1‘𝑔))}, ℝ*, < )
28	2, 9, 27	cmpt 4954	. 2 class (𝑓 ∈ ((0[,]+∞) ↑𝑚 ℝ) ↦ sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ 𝑓 ∧ 𝑥 = (∫1‘𝑔))}, ℝ*, < ))
29	1, 28	wceq 1656	1 wff ∫2 = (𝑓 ∈ ((0[,]+∞) ↑𝑚 ℝ) ↦ sup({𝑥 ∣ ∃𝑔 ∈ dom ∫1(𝑔 ∘𝑟 ≤ 𝑓 ∧ 𝑥 = (∫1‘𝑔))}, ℝ*, < ))

This definition is referenced by:  itg2val  23901