# Metamath Proof Explorer

## Theorem 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 ${⊢}\left({F}:ℝ⟶\left[0,\mathrm{+\infty }\right]\wedge {A}\in {ℝ}^{*}\right)\to \left({\int }^{2}\left({F}\right)\le {A}↔\forall {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\to {\int }^{1}\left({g}\right)\le {A}\right)\right)$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\}=\left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\}$
2 1 itg2val ${⊢}{F}:ℝ⟶\left[0,\mathrm{+\infty }\right]\to {\int }^{2}\left({F}\right)=sup\left(\left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\},{ℝ}^{*},<\right)$
3 2 adantr ${⊢}\left({F}:ℝ⟶\left[0,\mathrm{+\infty }\right]\wedge {A}\in {ℝ}^{*}\right)\to {\int }^{2}\left({F}\right)=sup\left(\left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\},{ℝ}^{*},<\right)$
4 3 breq1d ${⊢}\left({F}:ℝ⟶\left[0,\mathrm{+\infty }\right]\wedge {A}\in {ℝ}^{*}\right)\to \left({\int }^{2}\left({F}\right)\le {A}↔sup\left(\left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\},{ℝ}^{*},<\right)\le {A}\right)$
5 1 itg2lcl ${⊢}\left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\}\subseteq {ℝ}^{*}$
6 supxrleub ${⊢}\left(\left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\}\subseteq {ℝ}^{*}\wedge {A}\in {ℝ}^{*}\right)\to \left(sup\left(\left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\},{ℝ}^{*},<\right)\le {A}↔\forall {z}\in \left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{z}\le {A}\right)$
7 5 6 mpan ${⊢}{A}\in {ℝ}^{*}\to \left(sup\left(\left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\},{ℝ}^{*},<\right)\le {A}↔\forall {z}\in \left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{z}\le {A}\right)$
8 7 adantl ${⊢}\left({F}:ℝ⟶\left[0,\mathrm{+\infty }\right]\wedge {A}\in {ℝ}^{*}\right)\to \left(sup\left(\left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\},{ℝ}^{*},<\right)\le {A}↔\forall {z}\in \left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{z}\le {A}\right)$
9 eqeq1 ${⊢}{x}={z}\to \left({x}={\int }^{1}\left({g}\right)↔{z}={\int }^{1}\left({g}\right)\right)$
10 9 anbi2d ${⊢}{x}={z}\to \left(\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)↔\left({g}{\le }_{f}{F}\wedge {z}={\int }^{1}\left({g}\right)\right)\right)$
11 10 rexbidv ${⊢}{x}={z}\to \left(\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)↔\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {z}={\int }^{1}\left({g}\right)\right)\right)$
12 11 ralab ${⊢}\forall {z}\in \left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{z}\le {A}↔\forall {z}\phantom{\rule{.4em}{0ex}}\left(\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {z}={\int }^{1}\left({g}\right)\right)\to {z}\le {A}\right)$
13 r19.23v ${⊢}\forall {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left(\left({g}{\le }_{f}{F}\wedge {z}={\int }^{1}\left({g}\right)\right)\to {z}\le {A}\right)↔\left(\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {z}={\int }^{1}\left({g}\right)\right)\to {z}\le {A}\right)$
14 ancomst ${⊢}\left(\left({g}{\le }_{f}{F}\wedge {z}={\int }^{1}\left({g}\right)\right)\to {z}\le {A}\right)↔\left(\left({z}={\int }^{1}\left({g}\right)\wedge {g}{\le }_{f}{F}\right)\to {z}\le {A}\right)$
15 impexp ${⊢}\left(\left({z}={\int }^{1}\left({g}\right)\wedge {g}{\le }_{f}{F}\right)\to {z}\le {A}\right)↔\left({z}={\int }^{1}\left({g}\right)\to \left({g}{\le }_{f}{F}\to {z}\le {A}\right)\right)$
16 14 15 bitri ${⊢}\left(\left({g}{\le }_{f}{F}\wedge {z}={\int }^{1}\left({g}\right)\right)\to {z}\le {A}\right)↔\left({z}={\int }^{1}\left({g}\right)\to \left({g}{\le }_{f}{F}\to {z}\le {A}\right)\right)$
17 16 ralbii ${⊢}\forall {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left(\left({g}{\le }_{f}{F}\wedge {z}={\int }^{1}\left({g}\right)\right)\to {z}\le {A}\right)↔\forall {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({z}={\int }^{1}\left({g}\right)\to \left({g}{\le }_{f}{F}\to {z}\le {A}\right)\right)$
18 13 17 bitr3i ${⊢}\left(\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {z}={\int }^{1}\left({g}\right)\right)\to {z}\le {A}\right)↔\forall {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({z}={\int }^{1}\left({g}\right)\to \left({g}{\le }_{f}{F}\to {z}\le {A}\right)\right)$
19 18 albii ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {z}={\int }^{1}\left({g}\right)\right)\to {z}\le {A}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\forall {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({z}={\int }^{1}\left({g}\right)\to \left({g}{\le }_{f}{F}\to {z}\le {A}\right)\right)$
20 ralcom4 ${⊢}\forall {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={\int }^{1}\left({g}\right)\to \left({g}{\le }_{f}{F}\to {z}\le {A}\right)\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\forall {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({z}={\int }^{1}\left({g}\right)\to \left({g}{\le }_{f}{F}\to {z}\le {A}\right)\right)$
21 fvex ${⊢}{\int }^{1}\left({g}\right)\in \mathrm{V}$
22 breq1 ${⊢}{z}={\int }^{1}\left({g}\right)\to \left({z}\le {A}↔{\int }^{1}\left({g}\right)\le {A}\right)$
23 22 imbi2d ${⊢}{z}={\int }^{1}\left({g}\right)\to \left(\left({g}{\le }_{f}{F}\to {z}\le {A}\right)↔\left({g}{\le }_{f}{F}\to {\int }^{1}\left({g}\right)\le {A}\right)\right)$
24 21 23 ceqsalv ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={\int }^{1}\left({g}\right)\to \left({g}{\le }_{f}{F}\to {z}\le {A}\right)\right)↔\left({g}{\le }_{f}{F}\to {\int }^{1}\left({g}\right)\le {A}\right)$
25 24 ralbii ${⊢}\forall {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={\int }^{1}\left({g}\right)\to \left({g}{\le }_{f}{F}\to {z}\le {A}\right)\right)↔\forall {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\to {\int }^{1}\left({g}\right)\le {A}\right)$
26 20 25 bitr3i ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\forall {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({z}={\int }^{1}\left({g}\right)\to \left({g}{\le }_{f}{F}\to {z}\le {A}\right)\right)↔\forall {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\to {\int }^{1}\left({g}\right)\le {A}\right)$
27 19 26 bitri ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {z}={\int }^{1}\left({g}\right)\right)\to {z}\le {A}\right)↔\forall {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\to {\int }^{1}\left({g}\right)\le {A}\right)$
28 12 27 bitri ${⊢}\forall {z}\in \left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\}\phantom{\rule{.4em}{0ex}}{z}\le {A}↔\forall {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\to {\int }^{1}\left({g}\right)\le {A}\right)$
29 8 28 syl6bb ${⊢}\left({F}:ℝ⟶\left[0,\mathrm{+\infty }\right]\wedge {A}\in {ℝ}^{*}\right)\to \left(sup\left(\left\{{x}|\exists {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\wedge {x}={\int }^{1}\left({g}\right)\right)\right\},{ℝ}^{*},<\right)\le {A}↔\forall {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\to {\int }^{1}\left({g}\right)\le {A}\right)\right)$
30 4 29 bitrd ${⊢}\left({F}:ℝ⟶\left[0,\mathrm{+\infty }\right]\wedge {A}\in {ℝ}^{*}\right)\to \left({\int }^{2}\left({F}\right)\le {A}↔\forall {g}\in \mathrm{dom}{\int }^{1}\phantom{\rule{.4em}{0ex}}\left({g}{\le }_{f}{F}\to {\int }^{1}\left({g}\right)\le {A}\right)\right)$