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 
|- ( ( F : RR --> ( 0 [,] +oo ) /\ A e. RR* ) -> ( ( S.2 ` F ) <_ A <-> A. g e. dom S.1 ( g oR <_ F -> ( S.1 ` g ) <_ A ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } = { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) }
2 1 itg2val 
 |-  ( F : RR --> ( 0 [,] +oo ) -> ( S.2 ` F ) = sup ( { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } , RR* , < ) )
3 2 adantr 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ A e. RR* ) -> ( S.2 ` F ) = sup ( { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } , RR* , < ) )
4 3 breq1d 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ A e. RR* ) -> ( ( S.2 ` F ) <_ A <-> sup ( { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } , RR* , < ) <_ A ) )
5 1 itg2lcl 
 |-  { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } C_ RR*
6 supxrleub 
 |-  ( ( { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } C_ RR* /\ A e. RR* ) -> ( sup ( { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } , RR* , < ) <_ A <-> A. z e. { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } z <_ A ) )
7 5 6 mpan 
 |-  ( A e. RR* -> ( sup ( { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } , RR* , < ) <_ A <-> A. z e. { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } z <_ A ) )
8 7 adantl 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ A e. RR* ) -> ( sup ( { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } , RR* , < ) <_ A <-> A. z e. { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } z <_ A ) )
9 eqeq1 
 |-  ( x = z -> ( x = ( S.1 ` g ) <-> z = ( S.1 ` g ) ) )
10 9 anbi2d 
 |-  ( x = z -> ( ( g oR <_ F /\ x = ( S.1 ` g ) ) <-> ( g oR <_ F /\ z = ( S.1 ` g ) ) ) )
11 10 rexbidv 
 |-  ( x = z -> ( E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) <-> E. g e. dom S.1 ( g oR <_ F /\ z = ( S.1 ` g ) ) ) )
12 11 ralab 
 |-  ( A. z e. { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } z <_ A <-> A. z ( E. g e. dom S.1 ( g oR <_ F /\ z = ( S.1 ` g ) ) -> z <_ A ) )
13 r19.23v 
 |-  ( A. g e. dom S.1 ( ( g oR <_ F /\ z = ( S.1 ` g ) ) -> z <_ A ) <-> ( E. g e. dom S.1 ( g oR <_ F /\ z = ( S.1 ` g ) ) -> z <_ A ) )
14 ancomst 
 |-  ( ( ( g oR <_ F /\ z = ( S.1 ` g ) ) -> z <_ A ) <-> ( ( z = ( S.1 ` g ) /\ g oR <_ F ) -> z <_ A ) )
15 impexp 
 |-  ( ( ( z = ( S.1 ` g ) /\ g oR <_ F ) -> z <_ A ) <-> ( z = ( S.1 ` g ) -> ( g oR <_ F -> z <_ A ) ) )
16 14 15 bitri 
 |-  ( ( ( g oR <_ F /\ z = ( S.1 ` g ) ) -> z <_ A ) <-> ( z = ( S.1 ` g ) -> ( g oR <_ F -> z <_ A ) ) )
17 16 ralbii 
 |-  ( A. g e. dom S.1 ( ( g oR <_ F /\ z = ( S.1 ` g ) ) -> z <_ A ) <-> A. g e. dom S.1 ( z = ( S.1 ` g ) -> ( g oR <_ F -> z <_ A ) ) )
18 13 17 bitr3i 
 |-  ( ( E. g e. dom S.1 ( g oR <_ F /\ z = ( S.1 ` g ) ) -> z <_ A ) <-> A. g e. dom S.1 ( z = ( S.1 ` g ) -> ( g oR <_ F -> z <_ A ) ) )
19 18 albii 
 |-  ( A. z ( E. g e. dom S.1 ( g oR <_ F /\ z = ( S.1 ` g ) ) -> z <_ A ) <-> A. z A. g e. dom S.1 ( z = ( S.1 ` g ) -> ( g oR <_ F -> z <_ A ) ) )
20 ralcom4 
 |-  ( A. g e. dom S.1 A. z ( z = ( S.1 ` g ) -> ( g oR <_ F -> z <_ A ) ) <-> A. z A. g e. dom S.1 ( z = ( S.1 ` g ) -> ( g oR <_ F -> z <_ A ) ) )
21 fvex 
 |-  ( S.1 ` g ) e. _V
22 breq1 
 |-  ( z = ( S.1 ` g ) -> ( z <_ A <-> ( S.1 ` g ) <_ A ) )
23 22 imbi2d 
 |-  ( z = ( S.1 ` g ) -> ( ( g oR <_ F -> z <_ A ) <-> ( g oR <_ F -> ( S.1 ` g ) <_ A ) ) )
24 21 23 ceqsalv 
 |-  ( A. z ( z = ( S.1 ` g ) -> ( g oR <_ F -> z <_ A ) ) <-> ( g oR <_ F -> ( S.1 ` g ) <_ A ) )
25 24 ralbii 
 |-  ( A. g e. dom S.1 A. z ( z = ( S.1 ` g ) -> ( g oR <_ F -> z <_ A ) ) <-> A. g e. dom S.1 ( g oR <_ F -> ( S.1 ` g ) <_ A ) )
26 20 25 bitr3i 
 |-  ( A. z A. g e. dom S.1 ( z = ( S.1 ` g ) -> ( g oR <_ F -> z <_ A ) ) <-> A. g e. dom S.1 ( g oR <_ F -> ( S.1 ` g ) <_ A ) )
27 19 26 bitri 
 |-  ( A. z ( E. g e. dom S.1 ( g oR <_ F /\ z = ( S.1 ` g ) ) -> z <_ A ) <-> A. g e. dom S.1 ( g oR <_ F -> ( S.1 ` g ) <_ A ) )
28 12 27 bitri 
 |-  ( A. z e. { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } z <_ A <-> A. g e. dom S.1 ( g oR <_ F -> ( S.1 ` g ) <_ A ) )
29 8 28 bitrdi 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ A e. RR* ) -> ( sup ( { x | E. g e. dom S.1 ( g oR <_ F /\ x = ( S.1 ` g ) ) } , RR* , < ) <_ A <-> A. g e. dom S.1 ( g oR <_ F -> ( S.1 ` g ) <_ A ) ) )
30 4 29 bitrd 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ A e. RR* ) -> ( ( S.2 ` F ) <_ A <-> A. g e. dom S.1 ( g oR <_ F -> ( S.1 ` g ) <_ A ) ) )