This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )