itg2cl

Description: The integral of a nonnegative real function is an extended real number. (Contributed by Mario Carneiro, 28-Jun-2014)

		Ref	Expression
	Assertion	itg2cl	$⊢ F : ℝ ⟶ [0, +∞] \to \int^{2} (F) \in ℝ^{*}$

Step	Hyp	Ref	Expression
1		eqid	$⊢ \{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))\}$
2	1	itg2val	$⊢ F : ℝ ⟶ [0, +∞] \to \int^{2} (F) = sup (\{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} ℝ^{*} <)$
3	1	itg2lcl	$⊢ \{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} \subseteq ℝ^{*}$
4		supxrcl	$⊢ \{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} \subseteq ℝ^{} \to sup (\{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} ℝ^{} <) \in ℝ^{*}$
5	3 4	ax-mp	$⊢ sup (\{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} ℝ^{} <) \in ℝ^{}$
6	2 5	eqeltrdi	$⊢ F : ℝ ⟶ [0, +∞] \to \int^{2} (F) \in ℝ^{*}$

Metamath Proof Explorer