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 )