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

Metamath Proof Explorer

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 } =/= (/) )