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 )