Metamath Proof Explorer


Theorem ublbneg

Description: The image under negation of a bounded-above set of reals is bounded below. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion ublbneg
|- ( E. x e. RR A. y e. A y <_ x -> E. x e. RR A. y e. { z e. RR | -u z e. A } x <_ y )

Proof

Step Hyp Ref Expression
1 breq1
 |-  ( b = y -> ( b <_ a <-> y <_ a ) )
2 1 cbvralvw
 |-  ( A. b e. A b <_ a <-> A. y e. A y <_ a )
3 2 rexbii
 |-  ( E. a e. RR A. b e. A b <_ a <-> E. a e. RR A. y e. A y <_ a )
4 breq2
 |-  ( a = x -> ( y <_ a <-> y <_ x ) )
5 4 ralbidv
 |-  ( a = x -> ( A. y e. A y <_ a <-> A. y e. A y <_ x ) )
6 5 cbvrexvw
 |-  ( E. a e. RR A. y e. A y <_ a <-> E. x e. RR A. y e. A y <_ x )
7 3 6 bitri
 |-  ( E. a e. RR A. b e. A b <_ a <-> E. x e. RR A. y e. A y <_ x )
8 renegcl
 |-  ( a e. RR -> -u a e. RR )
9 elrabi
 |-  ( y e. { z e. RR | -u z e. A } -> y e. RR )
10 negeq
 |-  ( z = y -> -u z = -u y )
11 10 eleq1d
 |-  ( z = y -> ( -u z e. A <-> -u y e. A ) )
12 11 elrab3
 |-  ( y e. RR -> ( y e. { z e. RR | -u z e. A } <-> -u y e. A ) )
13 12 biimpd
 |-  ( y e. RR -> ( y e. { z e. RR | -u z e. A } -> -u y e. A ) )
14 9 13 mpcom
 |-  ( y e. { z e. RR | -u z e. A } -> -u y e. A )
15 breq1
 |-  ( b = -u y -> ( b <_ a <-> -u y <_ a ) )
16 15 rspcv
 |-  ( -u y e. A -> ( A. b e. A b <_ a -> -u y <_ a ) )
17 14 16 syl
 |-  ( y e. { z e. RR | -u z e. A } -> ( A. b e. A b <_ a -> -u y <_ a ) )
18 17 adantl
 |-  ( ( a e. RR /\ y e. { z e. RR | -u z e. A } ) -> ( A. b e. A b <_ a -> -u y <_ a ) )
19 lenegcon1
 |-  ( ( a e. RR /\ y e. RR ) -> ( -u a <_ y <-> -u y <_ a ) )
20 9 19 sylan2
 |-  ( ( a e. RR /\ y e. { z e. RR | -u z e. A } ) -> ( -u a <_ y <-> -u y <_ a ) )
21 18 20 sylibrd
 |-  ( ( a e. RR /\ y e. { z e. RR | -u z e. A } ) -> ( A. b e. A b <_ a -> -u a <_ y ) )
22 21 ralrimdva
 |-  ( a e. RR -> ( A. b e. A b <_ a -> A. y e. { z e. RR | -u z e. A } -u a <_ y ) )
23 breq1
 |-  ( x = -u a -> ( x <_ y <-> -u a <_ y ) )
24 23 ralbidv
 |-  ( x = -u a -> ( A. y e. { z e. RR | -u z e. A } x <_ y <-> A. y e. { z e. RR | -u z e. A } -u a <_ y ) )
25 24 rspcev
 |-  ( ( -u a e. RR /\ A. y e. { z e. RR | -u z e. A } -u a <_ y ) -> E. x e. RR A. y e. { z e. RR | -u z e. A } x <_ y )
26 8 22 25 syl6an
 |-  ( a e. RR -> ( A. b e. A b <_ a -> E. x e. RR A. y e. { z e. RR | -u z e. A } x <_ y ) )
27 26 rexlimiv
 |-  ( E. a e. RR A. b e. A b <_ a -> E. x e. RR A. y e. { z e. RR | -u z e. A } x <_ y )
28 7 27 sylbir
 |-  ( E. x e. RR A. y e. A y <_ x -> E. x e. RR A. y e. { z e. RR | -u z e. A } x <_ y )