Metamath Proof Explorer

Theorem itg2ub

Description: The integral of a nonnegative real function F is an upper bound on the integrals of all simple functions G dominated by F . (Contributed by Mario Carneiro, 28-Jun-2014)

		Ref	Expression
	Assertion	itg2ub	$⊢ (F : ℝ ⟶ [0, +∞] \land G \in dom \int^{1} \land G \leq_{f} F) \to \int^{1} (G) \leq \int^{2} (F)$

Proof

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	itg2lcl	$⊢ \{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} \subseteq ℝ^{*}$
3	1	itg2lr	$⊢ (G \in dom \int^{1} \land G \leq_{f} F) \to \int^{1} (G) \in \{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\}$
4	3	3adant1	$⊢ (F : ℝ ⟶ [0, +∞] \land G \in dom \int^{1} \land G \leq_{f} F) \to \int^{1} (G) \in \{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\}$
5		supxrub	$⊢ (\{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} \subseteq ℝ^{} \land \int^{1} (G) \in \{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\}) \to \int^{1} (G) \leq sup (\{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} ℝ^{} <)$
6	2 4 5	sylancr	$⊢ (F : ℝ ⟶ [0, +∞] \land G \in dom \int^{1} \land G \leq_{f} F) \to \int^{1} (G) \leq sup (\{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} ℝ^{*} <)$
7	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))\} ℝ^{*} <)$
8	7	3ad2ant1	$⊢ (F : ℝ ⟶ [0, +∞] \land G \in dom \int^{1} \land G \leq_{f} F) \to \int^{2} (F) = sup (\{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} ℝ^{*} <)$
9	6 8	breqtrrd	$⊢ (F : ℝ ⟶ [0, +∞] \land G \in dom \int^{1} \land G \leq_{f} F) \to \int^{1} (G) \leq \int^{2} (F)$