itg2leub

Description: Any upper bound on the integrals of all simple functions G dominated by F is greater than ( S.2F ) , the least upper bound. (Contributed by Mario Carneiro, 28-Jun-2014)

		Ref	Expression
	Assertion	itg2leub	$⊢ (F : ℝ ⟶ [0, +∞] \land A \in ℝ^{*}) \to (\int^{2} (F) \leq A \leftrightarrow \forall g \in dom \int^{1} (g \leq_{f} F \to \int^{1} (g) \leq A))$

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	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	2	adantr	$⊢ (F : ℝ ⟶ [0, +∞] \land A \in ℝ^{}) \to \int^{2} (F) = sup (\{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} ℝ^{} <)$
4	3	breq1d	$⊢ (F : ℝ ⟶ [0, +∞] \land A \in ℝ^{}) \to (\int^{2} (F) \leq A \leftrightarrow sup (\{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} ℝ^{} <) \leq A)$
5	1	itg2lcl	$⊢ \{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} \subseteq ℝ^{*}$
6		supxrleub	$⊢ (\{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} \subseteq ℝ^{} \land A \in ℝ^{}) \to (sup (\{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} ℝ^{*} <) \leq A \leftrightarrow \forall z \in \{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} z \leq A)$
7	5 6	mpan	$⊢ A \in ℝ^{} \to (sup (\{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} ℝ^{} <) \leq A \leftrightarrow \forall z \in \{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} z \leq A)$
8	7	adantl	$⊢ (F : ℝ ⟶ [0, +∞] \land A \in ℝ^{}) \to (sup (\{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} ℝ^{} <) \leq A \leftrightarrow \forall z \in \{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} z \leq A)$
9		eqeq1	$⊢ x = z \to (x = \int^{1} (g) \leftrightarrow z = \int^{1} (g))$
10	9	anbi2d	$⊢ x = z \to ((g \leq_{f} F \land x = \int^{1} (g)) \leftrightarrow (g \leq_{f} F \land z = \int^{1} (g)))$
11	10	rexbidv	$⊢ x = z \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 z = \int^{1} (g)))$
12	11	ralab	$⊢ \forall z \in \{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} z \leq A \leftrightarrow \forall z (\exists g \in dom \int^{1} (g \leq_{f} F \land z = \int^{1} (g)) \to z \leq A)$
13		r19.23v	$⊢ \forall g \in dom \int^{1} ((g \leq_{f} F \land z = \int^{1} (g)) \to z \leq A) \leftrightarrow (\exists g \in dom \int^{1} (g \leq_{f} F \land z = \int^{1} (g)) \to z \leq A)$
14		ancomst	$⊢ ((g \leq_{f} F \land z = \int^{1} (g)) \to z \leq A) \leftrightarrow ((z = \int^{1} (g) \land g \leq_{f} F) \to z \leq A)$
15		impexp	$⊢ ((z = \int^{1} (g) \land g \leq_{f} F) \to z \leq A) \leftrightarrow (z = \int^{1} (g) \to (g \leq_{f} F \to z \leq A))$
16	14 15	bitri	$⊢ ((g \leq_{f} F \land z = \int^{1} (g)) \to z \leq A) \leftrightarrow (z = \int^{1} (g) \to (g \leq_{f} F \to z \leq A))$
17	16	ralbii	$⊢ \forall g \in dom \int^{1} ((g \leq_{f} F \land z = \int^{1} (g)) \to z \leq A) \leftrightarrow \forall g \in dom \int^{1} (z = \int^{1} (g) \to (g \leq_{f} F \to z \leq A))$
18	13 17	bitr3i	$⊢ (\exists g \in dom \int^{1} (g \leq_{f} F \land z = \int^{1} (g)) \to z \leq A) \leftrightarrow \forall g \in dom \int^{1} (z = \int^{1} (g) \to (g \leq_{f} F \to z \leq A))$
19	18	albii	$⊢ \forall z (\exists g \in dom \int^{1} (g \leq_{f} F \land z = \int^{1} (g)) \to z \leq A) \leftrightarrow \forall z \forall g \in dom \int^{1} (z = \int^{1} (g) \to (g \leq_{f} F \to z \leq A))$
20		ralcom4	$⊢ \forall g \in dom \int^{1} \forall z (z = \int^{1} (g) \to (g \leq_{f} F \to z \leq A)) \leftrightarrow \forall z \forall g \in dom \int^{1} (z = \int^{1} (g) \to (g \leq_{f} F \to z \leq A))$
21		fvex	$⊢ \int^{1} (g) \in V$
22		breq1	$⊢ z = \int^{1} (g) \to (z \leq A \leftrightarrow \int^{1} (g) \leq A)$
23	22	imbi2d	$⊢ z = \int^{1} (g) \to ((g \leq_{f} F \to z \leq A) \leftrightarrow (g \leq_{f} F \to \int^{1} (g) \leq A))$
24	21 23	ceqsalv	$⊢ \forall z (z = \int^{1} (g) \to (g \leq_{f} F \to z \leq A)) \leftrightarrow (g \leq_{f} F \to \int^{1} (g) \leq A)$
25	24	ralbii	$⊢ \forall g \in dom \int^{1} \forall z (z = \int^{1} (g) \to (g \leq_{f} F \to z \leq A)) \leftrightarrow \forall g \in dom \int^{1} (g \leq_{f} F \to \int^{1} (g) \leq A)$
26	20 25	bitr3i	$⊢ \forall z \forall g \in dom \int^{1} (z = \int^{1} (g) \to (g \leq_{f} F \to z \leq A)) \leftrightarrow \forall g \in dom \int^{1} (g \leq_{f} F \to \int^{1} (g) \leq A)$
27	19 26	bitri	$⊢ \forall z (\exists g \in dom \int^{1} (g \leq_{f} F \land z = \int^{1} (g)) \to z \leq A) \leftrightarrow \forall g \in dom \int^{1} (g \leq_{f} F \to \int^{1} (g) \leq A)$
28	12 27	bitri	$⊢ \forall z \in \{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} z \leq A \leftrightarrow \forall g \in dom \int^{1} (g \leq_{f} F \to \int^{1} (g) \leq A)$
29	8 28	syl6bb	$⊢ (F : ℝ ⟶ [0, +∞] \land A \in ℝ^{}) \to (sup (\{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} ℝ^{} <) \leq A \leftrightarrow \forall g \in dom \int^{1} (g \leq_{f} F \to \int^{1} (g) \leq A))$
30	4 29	bitrd	$⊢ (F : ℝ ⟶ [0, +∞] \land A \in ℝ^{*}) \to (\int^{2} (F) \leq A \leftrightarrow \forall g \in dom \int^{1} (g \leq_{f} F \to \int^{1} (g) \leq A))$

Metamath Proof Explorer

Theorem itg2leub

Proof