Metamath Proof Explorer


Theorem ioombl1

Description: An open right-unbounded interval is measurable. (Contributed by Mario Carneiro, 16-Jun-2014) (Proof shortened by Mario Carneiro, 25-Mar-2015)

Ref Expression
Assertion ioombl1
|- ( A e. RR* -> ( A (,) +oo ) e. dom vol )

Proof

Step Hyp Ref Expression
1 elxr
 |-  ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
2 ioossre
 |-  ( A (,) +oo ) C_ RR
3 2 a1i
 |-  ( A e. RR -> ( A (,) +oo ) C_ RR )
4 elpwi
 |-  ( x e. ~P RR -> x C_ RR )
5 simplrl
 |-  ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) -> x C_ RR )
6 simplrr
 |-  ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) -> ( vol* ` x ) e. RR )
7 simpr
 |-  ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) -> y e. RR+ )
8 eqid
 |-  seq 1 ( + , ( ( abs o. - ) o. f ) ) = seq 1 ( + , ( ( abs o. - ) o. f ) )
9 8 ovolgelb
 |-  ( ( x C_ RR /\ ( vol* ` x ) e. RR /\ y e. RR+ ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( x C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) ) )
10 5 6 7 9 syl3anc
 |-  ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( x C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) ) )
11 eqid
 |-  ( A (,) +oo ) = ( A (,) +oo )
12 simplll
 |-  ( ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( x C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) ) ) ) -> A e. RR )
13 5 adantr
 |-  ( ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( x C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) ) ) ) -> x C_ RR )
14 6 adantr
 |-  ( ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( x C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) ) ) ) -> ( vol* ` x ) e. RR )
15 simplr
 |-  ( ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( x C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) ) ) ) -> y e. RR+ )
16 eqid
 |-  seq 1 ( + , ( ( abs o. - ) o. ( m e. NN |-> <. if ( if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) <_ ( 2nd ` ( f ` m ) ) , if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) >. ) ) ) = seq 1 ( + , ( ( abs o. - ) o. ( m e. NN |-> <. if ( if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) <_ ( 2nd ` ( f ` m ) ) , if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) >. ) ) )
17 eqid
 |-  seq 1 ( + , ( ( abs o. - ) o. ( m e. NN |-> <. ( 1st ` ( f ` m ) ) , if ( if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) <_ ( 2nd ` ( f ` m ) ) , if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) ) >. ) ) ) = seq 1 ( + , ( ( abs o. - ) o. ( m e. NN |-> <. ( 1st ` ( f ` m ) ) , if ( if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) <_ ( 2nd ` ( f ` m ) ) , if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) ) >. ) ) )
18 simprl
 |-  ( ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( x C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) ) ) ) -> f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
19 elovolmlem
 |-  ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) <-> f : NN --> ( <_ i^i ( RR X. RR ) ) )
20 18 19 sylib
 |-  ( ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( x C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) ) ) ) -> f : NN --> ( <_ i^i ( RR X. RR ) ) )
21 simprrl
 |-  ( ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( x C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) ) ) ) -> x C_ U. ran ( (,) o. f ) )
22 simprrr
 |-  ( ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( x C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) ) ) ) -> sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) )
23 eqid
 |-  ( 1st ` ( f ` n ) ) = ( 1st ` ( f ` n ) )
24 eqid
 |-  ( 2nd ` ( f ` n ) ) = ( 2nd ` ( f ` n ) )
25 2fveq3
 |-  ( m = n -> ( 1st ` ( f ` m ) ) = ( 1st ` ( f ` n ) ) )
26 25 breq1d
 |-  ( m = n -> ( ( 1st ` ( f ` m ) ) <_ A <-> ( 1st ` ( f ` n ) ) <_ A ) )
27 26 25 ifbieq2d
 |-  ( m = n -> if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) = if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) )
28 2fveq3
 |-  ( m = n -> ( 2nd ` ( f ` m ) ) = ( 2nd ` ( f ` n ) ) )
29 27 28 breq12d
 |-  ( m = n -> ( if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) <_ ( 2nd ` ( f ` m ) ) <-> if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) <_ ( 2nd ` ( f ` n ) ) ) )
30 29 27 28 ifbieq12d
 |-  ( m = n -> if ( if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) <_ ( 2nd ` ( f ` m ) ) , if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) ) = if ( if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) <_ ( 2nd ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) , ( 2nd ` ( f ` n ) ) ) )
31 30 28 opeq12d
 |-  ( m = n -> <. if ( if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) <_ ( 2nd ` ( f ` m ) ) , if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) >. = <. if ( if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) <_ ( 2nd ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) , ( 2nd ` ( f ` n ) ) ) , ( 2nd ` ( f ` n ) ) >. )
32 31 cbvmptv
 |-  ( m e. NN |-> <. if ( if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) <_ ( 2nd ` ( f ` m ) ) , if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) >. ) = ( n e. NN |-> <. if ( if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) <_ ( 2nd ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) , ( 2nd ` ( f ` n ) ) ) , ( 2nd ` ( f ` n ) ) >. )
33 25 30 opeq12d
 |-  ( m = n -> <. ( 1st ` ( f ` m ) ) , if ( if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) <_ ( 2nd ` ( f ` m ) ) , if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) ) >. = <. ( 1st ` ( f ` n ) ) , if ( if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) <_ ( 2nd ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) , ( 2nd ` ( f ` n ) ) ) >. )
34 33 cbvmptv
 |-  ( m e. NN |-> <. ( 1st ` ( f ` m ) ) , if ( if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) <_ ( 2nd ` ( f ` m ) ) , if ( ( 1st ` ( f ` m ) ) <_ A , A , ( 1st ` ( f ` m ) ) ) , ( 2nd ` ( f ` m ) ) ) >. ) = ( n e. NN |-> <. ( 1st ` ( f ` n ) ) , if ( if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) <_ ( 2nd ` ( f ` n ) ) , if ( ( 1st ` ( f ` n ) ) <_ A , A , ( 1st ` ( f ` n ) ) ) , ( 2nd ` ( f ` n ) ) ) >. )
35 11 12 13 14 15 8 16 17 20 21 22 23 24 32 34 ioombl1lem4
 |-  ( ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) /\ ( f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) /\ ( x C_ U. ran ( (,) o. f ) /\ sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) <_ ( ( vol* ` x ) + y ) ) ) ) -> ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( ( vol* ` x ) + y ) )
36 10 35 rexlimddv
 |-  ( ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) /\ y e. RR+ ) -> ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( ( vol* ` x ) + y ) )
37 36 ralrimiva
 |-  ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> A. y e. RR+ ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( ( vol* ` x ) + y ) )
38 inss1
 |-  ( x i^i ( A (,) +oo ) ) C_ x
39 ovolsscl
 |-  ( ( ( x i^i ( A (,) +oo ) ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i ( A (,) +oo ) ) ) e. RR )
40 38 39 mp3an1
 |-  ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i ( A (,) +oo ) ) ) e. RR )
41 40 adantl
 |-  ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x i^i ( A (,) +oo ) ) ) e. RR )
42 difss
 |-  ( x \ ( A (,) +oo ) ) C_ x
43 ovolsscl
 |-  ( ( ( x \ ( A (,) +oo ) ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ ( A (,) +oo ) ) ) e. RR )
44 42 43 mp3an1
 |-  ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ ( A (,) +oo ) ) ) e. RR )
45 44 adantl
 |-  ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x \ ( A (,) +oo ) ) ) e. RR )
46 41 45 readdcld
 |-  ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) e. RR )
47 simprr
 |-  ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` x ) e. RR )
48 alrple
 |-  ( ( ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) e. RR /\ ( vol* ` x ) e. RR ) -> ( ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( vol* ` x ) <-> A. y e. RR+ ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( ( vol* ` x ) + y ) ) )
49 46 47 48 syl2anc
 |-  ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( vol* ` x ) <-> A. y e. RR+ ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( ( vol* ` x ) + y ) ) )
50 37 49 mpbird
 |-  ( ( A e. RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( vol* ` x ) )
51 50 expr
 |-  ( ( A e. RR /\ x C_ RR ) -> ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( vol* ` x ) ) )
52 4 51 sylan2
 |-  ( ( A e. RR /\ x e. ~P RR ) -> ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( vol* ` x ) ) )
53 52 ralrimiva
 |-  ( A e. RR -> A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( vol* ` x ) ) )
54 ismbl2
 |-  ( ( A (,) +oo ) e. dom vol <-> ( ( A (,) +oo ) C_ RR /\ A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i ( A (,) +oo ) ) ) + ( vol* ` ( x \ ( A (,) +oo ) ) ) ) <_ ( vol* ` x ) ) ) )
55 3 53 54 sylanbrc
 |-  ( A e. RR -> ( A (,) +oo ) e. dom vol )
56 oveq1
 |-  ( A = +oo -> ( A (,) +oo ) = ( +oo (,) +oo ) )
57 iooid
 |-  ( +oo (,) +oo ) = (/)
58 56 57 eqtrdi
 |-  ( A = +oo -> ( A (,) +oo ) = (/) )
59 0mbl
 |-  (/) e. dom vol
60 58 59 eqeltrdi
 |-  ( A = +oo -> ( A (,) +oo ) e. dom vol )
61 oveq1
 |-  ( A = -oo -> ( A (,) +oo ) = ( -oo (,) +oo ) )
62 ioomax
 |-  ( -oo (,) +oo ) = RR
63 61 62 eqtrdi
 |-  ( A = -oo -> ( A (,) +oo ) = RR )
64 rembl
 |-  RR e. dom vol
65 63 64 eqeltrdi
 |-  ( A = -oo -> ( A (,) +oo ) e. dom vol )
66 55 60 65 3jaoi
 |-  ( ( A e. RR \/ A = +oo \/ A = -oo ) -> ( A (,) +oo ) e. dom vol )
67 1 66 sylbi
 |-  ( A e. RR* -> ( A (,) +oo ) e. dom vol )