itg2val

Description: Value of the integral on nonnegative real functions. (Contributed by Mario Carneiro, 28-Jun-2014)

		Ref	Expression
	Hypothesis	itg2val.1	$⊢ L = \{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\}$
	Assertion	itg2val	$⊢ F : ℝ ⟶ [0, +∞] \to \int^{2} (F) = sup (L ℝ^{*} <)$

Step	Hyp	Ref	Expression
1		itg2val.1	$⊢ L = \{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\}$
2		xrltso	$⊢ < Or ℝ^{*}$
3	2	supex	$⊢ sup (L ℝ^{*} <) \in V$
4		reex	$⊢ ℝ \in V$
5		ovex	$⊢ [0, +∞] \in V$
6		breq2	$⊢ f = F \to (g \leq_{f} f \leftrightarrow g \leq_{f} F)$
7	6	anbi1d	$⊢ f = F \to ((g \leq_{f} f \land x = \int^{1} (g)) \leftrightarrow (g \leq_{f} F \land x = \int^{1} (g)))$
8	7	rexbidv	$⊢ f = F \to (\exists g \in dom \int^{1} (g \leq_{f} f \land x = \int^{1} (g)) \leftrightarrow \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g)))$
9	8	abbidv	$⊢ f = F \to \{x \| \exists g \in dom \int^{1} (g \leq_{f} f \land x = \int^{1} (g))\} = \{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\}$
10	9 1	eqtr4di	$⊢ f = F \to \{x \| \exists g \in dom \int^{1} (g \leq_{f} f \land x = \int^{1} (g))\} = L$
11	10	supeq1d	$⊢ f = F \to sup (\{x \| \exists g \in dom \int^{1} (g \leq_{f} f \land x = \int^{1} (g))\} ℝ^{} <) = sup (L ℝ^{} <)$
12		df-itg2	$⊢ \int^{2} = (f \in ({[0, +∞]}^{ℝ}) ⟼ sup (\{x \| \exists g \in dom \int^{1} (g \leq_{f} f \land x = \int^{1} (g))\} ℝ^{*} <))$
13	3 4 5 11 12	fvmptmap	$⊢ F : ℝ ⟶ [0, +∞] \to \int^{2} (F) = sup (L ℝ^{*} <)$

Metamath Proof Explorer