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	$⊢ \int^{2} = (f \in ({[0, +∞]}^{ℝ}) ⟼ sup (\{x \| \exists g \in dom \int^{1} (g \leq_{f} f \land x = \int^{1} (g))\} ℝ^{*} <))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		citg2	$class \int^{2}$
1		vf	$setvar f$
2		cc0	$class 0$
3		cicc	$class [.]$
4		cpnf	$class +∞$
5	2 4 3	co	$class [0, +∞]$
6		cmap	$class ↑_{𝑚}$
7		cr	$class ℝ$
8	5 7 6	co	$class ({[0, +∞]}^{ℝ})$
9		vx	$setvar x$
10		vg	$setvar g$
11		citg1	$class \int^{1}$
12	11	cdm	$class dom \int^{1}$
13	10	cv	$setvar g$
14		cle	$class \leq$
15	14	cofr	$class \circ_{r} \leq$
16	1	cv	$setvar f$
17	13 16 15	wbr	$wff g \leq_{f} f$
18	9	cv	$setvar x$
19	13 11	cfv	$class \int^{1} (g)$
20	18 19	wceq	$wff x = \int^{1} (g)$
21	17 20	wa	$wff (g \leq_{f} f \land x = \int^{1} (g))$
22	21 10 12	wrex	$wff \exists g \in dom \int^{1} (g \leq_{f} f \land x = \int^{1} (g))$
23	22 9	cab	$class \{x \| \exists g \in dom \int^{1} (g \leq_{f} f \land x = \int^{1} (g))\}$
24		cxr	$class ℝ^{*}$
25		clt	$class <$
26	23 24 25	csup	$class sup (\{x \| \exists g \in dom \int^{1} (g \leq_{f} f \land x = \int^{1} (g))\} ℝ^{*} <)$
27	1 8 26	cmpt	$class (f \in ({[0, +∞]}^{ℝ}) ⟼ sup (\{x \| \exists g \in dom \int^{1} (g \leq_{f} f \land x = \int^{1} (g))\} ℝ^{*} <))$
28	0 27	wceq	$wff \int^{2} = (f \in ({[0, +∞]}^{ℝ}) ⟼ sup (\{x \| \exists g \in dom \int^{1} (g \leq_{f} f \land x = \int^{1} (g))\} ℝ^{*} <))$

Metamath Proof Explorer

Definition df-itg2

Detailed syntax breakdown