Theorem negn0

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

	Ref	Expression
Assertion	negn0	|- ( ( A C_ RR /\ A =/= (/) ) -> { z e. RR | -u z e. A } =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		n0	|- ( A =/= (/) <-> E. x x e. A )
2		ssel	|- ( A C_ RR -> ( x e. A -> x e. RR ) )
3		renegcl	|- ( x e. RR -> -u x e. RR )
4		negeq	|- ( z = -u x -> -u z = -u -u x )
5	4	eleq1d	|- ( z = -u x -> ( -u z e. A <-> -u -u x e. A ) )
6	5	elrab3	|- ( -u x e. RR -> ( -u x e. { z e. RR | -u z e. A } <-> -u -u x e. A ) )
7	3 6	syl	|- ( x e. RR -> ( -u x e. { z e. RR | -u z e. A } <-> -u -u x e. A ) )
8		recn	|- ( x e. RR -> x e. CC )
9	8	negnegd	|- ( x e. RR -> -u -u x = x )
10	9	eleq1d	|- ( x e. RR -> ( -u -u x e. A <-> x e. A ) )
11	7 10	bitrd	|- ( x e. RR -> ( -u x e. { z e. RR | -u z e. A } <-> x e. A ) )
12	11	biimprd	|- ( x e. RR -> ( x e. A -> -u x e. { z e. RR | -u z e. A } ) )
13	2 12	syli	|- ( A C_ RR -> ( x e. A -> -u x e. { z e. RR | -u z e. A } ) )
14		elex2	|- ( -u x e. { z e. RR | -u z e. A } -> E. y y e. { z e. RR | -u z e. A } )
15	13 14	syl6	|- ( A C_ RR -> ( x e. A -> E. y y e. { z e. RR | -u z e. A } ) )
16		n0	|- ( { z e. RR | -u z e. A } =/= (/) <-> E. y y e. { z e. RR | -u z e. A } )
17	15 16	imbitrrdi	|- ( A C_ RR -> ( x e. A -> { z e. RR | -u z e. A } =/= (/) ) )
18	17	exlimdv	|- ( A C_ RR -> ( E. x x e. A -> { z e. RR | -u z e. A } =/= (/) ) )
19	1 18	biimtrid	|- ( A C_ RR -> ( A =/= (/) -> { z e. RR | -u z e. A } =/= (/) ) )
20	19	imp	|- ( ( A C_ RR /\ A =/= (/) ) -> { z e. RR | -u z e. A } =/= (/) )