Metamath Proof Explorer

Theorem xrub

Description: By quantifying only over reals, we can specify any extended real upper bound for any set of extended reals. (Contributed by NM, 9-Apr-2006)

Ref Expression
Assertion xrub 
|- ( ( A C_ RR* /\ B e. RR* ) -> ( A. x e. RR ( x < B -> E. y e. A x < y ) <-> A. x e. RR* ( x < B -> E. y e. A x < y ) ) )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( x = z -> ( x < B <-> z < B ) )
2 breq1 
 |-  ( x = z -> ( x < y <-> z < y ) )
3 2 rexbidv 
 |-  ( x = z -> ( E. y e. A x < y <-> E. y e. A z < y ) )
4 1 3 imbi12d 
 |-  ( x = z -> ( ( x < B -> E. y e. A x < y ) <-> ( z < B -> E. y e. A z < y ) ) )
5 4 cbvralvw 
 |-  ( A. x e. RR ( x < B -> E. y e. A x < y ) <-> A. z e. RR ( z < B -> E. y e. A z < y ) )
6 elxr 
 |-  ( x e. RR* <-> ( x e. RR \/ x = +oo \/ x = -oo ) )
7 pm2.27 
 |-  ( x e. RR -> ( ( x e. RR -> ( x < B -> E. y e. A x < y ) ) -> ( x < B -> E. y e. A x < y ) ) )
8 7 a1i 
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ A. z e. RR ( z < B -> E. y e. A z < y ) ) -> ( x e. RR -> ( ( x e. RR -> ( x < B -> E. y e. A x < y ) ) -> ( x < B -> E. y e. A x < y ) ) ) )
9 pnfnlt 
 |-  ( B e. RR* -> -. +oo < B )
10 breq1 
 |-  ( x = +oo -> ( x < B <-> +oo < B ) )
11 10 notbid 
 |-  ( x = +oo -> ( -. x < B <-> -. +oo < B ) )
12 9 11 syl5ibr 
 |-  ( x = +oo -> ( B e. RR* -> -. x < B ) )
13 pm2.21 
 |-  ( -. x < B -> ( x < B -> E. y e. A x < y ) )
14 12 13 syl6com 
 |-  ( B e. RR* -> ( x = +oo -> ( x < B -> E. y e. A x < y ) ) )
15 14 ad2antlr 
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ A. z e. RR ( z < B -> E. y e. A z < y ) ) -> ( x = +oo -> ( x < B -> E. y e. A x < y ) ) )
16 15 a1dd 
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ A. z e. RR ( z < B -> E. y e. A z < y ) ) -> ( x = +oo -> ( ( x e. RR -> ( x < B -> E. y e. A x < y ) ) -> ( x < B -> E. y e. A x < y ) ) ) )
17 elxr 
 |-  ( B e. RR* <-> ( B e. RR \/ B = +oo \/ B = -oo ) )
18 peano2rem 
 |-  ( B e. RR -> ( B - 1 ) e. RR )
19 breq1 
 |-  ( z = ( B - 1 ) -> ( z < B <-> ( B - 1 ) < B ) )
20 breq1 
 |-  ( z = ( B - 1 ) -> ( z < y <-> ( B - 1 ) < y ) )
21 20 rexbidv 
 |-  ( z = ( B - 1 ) -> ( E. y e. A z < y <-> E. y e. A ( B - 1 ) < y ) )
22 19 21 imbi12d 
 |-  ( z = ( B - 1 ) -> ( ( z < B -> E. y e. A z < y ) <-> ( ( B - 1 ) < B -> E. y e. A ( B - 1 ) < y ) ) )
23 22 rspcv 
 |-  ( ( B - 1 ) e. RR -> ( A. z e. RR ( z < B -> E. y e. A z < y ) -> ( ( B - 1 ) < B -> E. y e. A ( B - 1 ) < y ) ) )
24 18 23 syl 
 |-  ( B e. RR -> ( A. z e. RR ( z < B -> E. y e. A z < y ) -> ( ( B - 1 ) < B -> E. y e. A ( B - 1 ) < y ) ) )
25 24 adantl 
 |-  ( ( A C_ RR* /\ B e. RR ) -> ( A. z e. RR ( z < B -> E. y e. A z < y ) -> ( ( B - 1 ) < B -> E. y e. A ( B - 1 ) < y ) ) )
26 ltm1 
 |-  ( B e. RR -> ( B - 1 ) < B )
27 id 
 |-  ( ( ( B - 1 ) < B -> E. y e. A ( B - 1 ) < y ) -> ( ( B - 1 ) < B -> E. y e. A ( B - 1 ) < y ) )
28 26 27 syl5com 
 |-  ( B e. RR -> ( ( ( B - 1 ) < B -> E. y e. A ( B - 1 ) < y ) -> E. y e. A ( B - 1 ) < y ) )
29 28 adantl 
 |-  ( ( A C_ RR* /\ B e. RR ) -> ( ( ( B - 1 ) < B -> E. y e. A ( B - 1 ) < y ) -> E. y e. A ( B - 1 ) < y ) )
30 18 ad2antlr 
 |-  ( ( ( A C_ RR* /\ B e. RR ) /\ y e. A ) -> ( B - 1 ) e. RR )
31 mnflt 
 |-  ( ( B - 1 ) e. RR -> -oo < ( B - 1 ) )
32 30 31 syl 
 |-  ( ( ( A C_ RR* /\ B e. RR ) /\ y e. A ) -> -oo < ( B - 1 ) )
33 mnfxr 
 |-  -oo e. RR*
34 30 rexrd 
 |-  ( ( ( A C_ RR* /\ B e. RR ) /\ y e. A ) -> ( B - 1 ) e. RR* )
35 ssel2 
 |-  ( ( A C_ RR* /\ y e. A ) -> y e. RR* )
36 35 adantlr 
 |-  ( ( ( A C_ RR* /\ B e. RR ) /\ y e. A ) -> y e. RR* )
37 xrlttr 
 |-  ( ( -oo e. RR* /\ ( B - 1 ) e. RR* /\ y e. RR* ) -> ( ( -oo < ( B - 1 ) /\ ( B - 1 ) < y ) -> -oo < y ) )
38 33 34 36 37 mp3an2i 
 |-  ( ( ( A C_ RR* /\ B e. RR ) /\ y e. A ) -> ( ( -oo < ( B - 1 ) /\ ( B - 1 ) < y ) -> -oo < y ) )
39 32 38 mpand 
 |-  ( ( ( A C_ RR* /\ B e. RR ) /\ y e. A ) -> ( ( B - 1 ) < y -> -oo < y ) )
40 39 reximdva 
 |-  ( ( A C_ RR* /\ B e. RR ) -> ( E. y e. A ( B - 1 ) < y -> E. y e. A -oo < y ) )
41 25 29 40 3syld 
 |-  ( ( A C_ RR* /\ B e. RR ) -> ( A. z e. RR ( z < B -> E. y e. A z < y ) -> E. y e. A -oo < y ) )
42 41 a1dd 
 |-  ( ( A C_ RR* /\ B e. RR ) -> ( A. z e. RR ( z < B -> E. y e. A z < y ) -> ( -oo < B -> E. y e. A -oo < y ) ) )
43 1re 
 |-  1 e. RR
44 breq1 
 |-  ( z = 1 -> ( z < B <-> 1 < B ) )
45 breq1 
 |-  ( z = 1 -> ( z < y <-> 1 < y ) )
46 45 rexbidv 
 |-  ( z = 1 -> ( E. y e. A z < y <-> E. y e. A 1 < y ) )
47 44 46 imbi12d 
 |-  ( z = 1 -> ( ( z < B -> E. y e. A z < y ) <-> ( 1 < B -> E. y e. A 1 < y ) ) )
48 47 rspcv 
 |-  ( 1 e. RR -> ( A. z e. RR ( z < B -> E. y e. A z < y ) -> ( 1 < B -> E. y e. A 1 < y ) ) )
49 43 48 ax-mp 
 |-  ( A. z e. RR ( z < B -> E. y e. A z < y ) -> ( 1 < B -> E. y e. A 1 < y ) )
50 ltpnf 
 |-  ( 1 e. RR -> 1 < +oo )
51 43 50 ax-mp 
 |-  1 < +oo
52 breq2 
 |-  ( B = +oo -> ( 1 < B <-> 1 < +oo ) )
53 51 52 mpbiri 
 |-  ( B = +oo -> 1 < B )
54 id 
 |-  ( ( 1 < B -> E. y e. A 1 < y ) -> ( 1 < B -> E. y e. A 1 < y ) )
55 53 54 syl5com 
 |-  ( B = +oo -> ( ( 1 < B -> E. y e. A 1 < y ) -> E. y e. A 1 < y ) )
56 mnflt 
 |-  ( 1 e. RR -> -oo < 1 )
57 43 56 ax-mp 
 |-  -oo < 1
58 rexr 
 |-  ( 1 e. RR -> 1 e. RR* )
59 43 58 ax-mp 
 |-  1 e. RR*
60 xrlttr 
 |-  ( ( -oo e. RR* /\ 1 e. RR* /\ y e. RR* ) -> ( ( -oo < 1 /\ 1 < y ) -> -oo < y ) )
61 33 59 60 mp3an12 
 |-  ( y e. RR* -> ( ( -oo < 1 /\ 1 < y ) -> -oo < y ) )
62 57 61 mpani 
 |-  ( y e. RR* -> ( 1 < y -> -oo < y ) )
63 35 62 syl 
 |-  ( ( A C_ RR* /\ y e. A ) -> ( 1 < y -> -oo < y ) )
64 63 reximdva 
 |-  ( A C_ RR* -> ( E. y e. A 1 < y -> E. y e. A -oo < y ) )
65 55 64 sylan9r 
 |-  ( ( A C_ RR* /\ B = +oo ) -> ( ( 1 < B -> E. y e. A 1 < y ) -> E. y e. A -oo < y ) )
66 49 65 syl5 
 |-  ( ( A C_ RR* /\ B = +oo ) -> ( A. z e. RR ( z < B -> E. y e. A z < y ) -> E. y e. A -oo < y ) )
67 66 a1dd 
 |-  ( ( A C_ RR* /\ B = +oo ) -> ( A. z e. RR ( z < B -> E. y e. A z < y ) -> ( -oo < B -> E. y e. A -oo < y ) ) )
68 xrltnr 
 |-  ( -oo e. RR* -> -. -oo < -oo )
69 33 68 ax-mp 
 |-  -. -oo < -oo
70 breq2 
 |-  ( B = -oo -> ( -oo < B <-> -oo < -oo ) )
71 69 70 mtbiri 
 |-  ( B = -oo -> -. -oo < B )
72 71 adantl 
 |-  ( ( A C_ RR* /\ B = -oo ) -> -. -oo < B )
73 72 pm2.21d 
 |-  ( ( A C_ RR* /\ B = -oo ) -> ( -oo < B -> E. y e. A -oo < y ) )
74 73 a1d 
 |-  ( ( A C_ RR* /\ B = -oo ) -> ( A. z e. RR ( z < B -> E. y e. A z < y ) -> ( -oo < B -> E. y e. A -oo < y ) ) )
75 42 67 74 3jaodan 
 |-  ( ( A C_ RR* /\ ( B e. RR \/ B = +oo \/ B = -oo ) ) -> ( A. z e. RR ( z < B -> E. y e. A z < y ) -> ( -oo < B -> E. y e. A -oo < y ) ) )
76 17 75 sylan2b 
 |-  ( ( A C_ RR* /\ B e. RR* ) -> ( A. z e. RR ( z < B -> E. y e. A z < y ) -> ( -oo < B -> E. y e. A -oo < y ) ) )
77 76 imp 
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ A. z e. RR ( z < B -> E. y e. A z < y ) ) -> ( -oo < B -> E. y e. A -oo < y ) )
78 breq1 
 |-  ( x = -oo -> ( x < B <-> -oo < B ) )
79 breq1 
 |-  ( x = -oo -> ( x < y <-> -oo < y ) )
80 79 rexbidv 
 |-  ( x = -oo -> ( E. y e. A x < y <-> E. y e. A -oo < y ) )
81 78 80 imbi12d 
 |-  ( x = -oo -> ( ( x < B -> E. y e. A x < y ) <-> ( -oo < B -> E. y e. A -oo < y ) ) )
82 77 81 syl5ibrcom 
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ A. z e. RR ( z < B -> E. y e. A z < y ) ) -> ( x = -oo -> ( x < B -> E. y e. A x < y ) ) )
83 82 a1dd 
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ A. z e. RR ( z < B -> E. y e. A z < y ) ) -> ( x = -oo -> ( ( x e. RR -> ( x < B -> E. y e. A x < y ) ) -> ( x < B -> E. y e. A x < y ) ) ) )
84 8 16 83 3jaod 
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ A. z e. RR ( z < B -> E. y e. A z < y ) ) -> ( ( x e. RR \/ x = +oo \/ x = -oo ) -> ( ( x e. RR -> ( x < B -> E. y e. A x < y ) ) -> ( x < B -> E. y e. A x < y ) ) ) )
85 6 84 syl5bi 
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ A. z e. RR ( z < B -> E. y e. A z < y ) ) -> ( x e. RR* -> ( ( x e. RR -> ( x < B -> E. y e. A x < y ) ) -> ( x < B -> E. y e. A x < y ) ) ) )
86 85 com23 
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ A. z e. RR ( z < B -> E. y e. A z < y ) ) -> ( ( x e. RR -> ( x < B -> E. y e. A x < y ) ) -> ( x e. RR* -> ( x < B -> E. y e. A x < y ) ) ) )
87 86 ralimdv2 
 |-  ( ( ( A C_ RR* /\ B e. RR* ) /\ A. z e. RR ( z < B -> E. y e. A z < y ) ) -> ( A. x e. RR ( x < B -> E. y e. A x < y ) -> A. x e. RR* ( x < B -> E. y e. A x < y ) ) )
88 87 ex 
 |-  ( ( A C_ RR* /\ B e. RR* ) -> ( A. z e. RR ( z < B -> E. y e. A z < y ) -> ( A. x e. RR ( x < B -> E. y e. A x < y ) -> A. x e. RR* ( x < B -> E. y e. A x < y ) ) ) )
89 5 88 syl5bi 
 |-  ( ( A C_ RR* /\ B e. RR* ) -> ( A. x e. RR ( x < B -> E. y e. A x < y ) -> ( A. x e. RR ( x < B -> E. y e. A x < y ) -> A. x e. RR* ( x < B -> E. y e. A x < y ) ) ) )
90 89 pm2.43d 
 |-  ( ( A C_ RR* /\ B e. RR* ) -> ( A. x e. RR ( x < B -> E. y e. A x < y ) -> A. x e. RR* ( x < B -> E. y e. A x < y ) ) )
91 rexr 
 |-  ( x e. RR -> x e. RR* )
92 91 imim1i 
 |-  ( ( x e. RR* -> ( x < B -> E. y e. A x < y ) ) -> ( x e. RR -> ( x < B -> E. y e. A x < y ) ) )
93 92 ralimi2 
 |-  ( A. x e. RR* ( x < B -> E. y e. A x < y ) -> A. x e. RR ( x < B -> E. y e. A x < y ) )
94 90 93 impbid1 
 |-  ( ( A C_ RR* /\ B e. RR* ) -> ( A. x e. RR ( x < B -> E. y e. A x < y ) <-> A. x e. RR* ( x < B -> E. y e. A x < y ) ) )