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	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \right)\to \left\{z\in ℝ|-z\in A\right\}\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		n0	$$⊢A\ne \varnothing \leftrightarrow \exists xx\in A$$
2		ssel	$$⊢A\subseteq ℝ\to \left(x\in A\to x\in ℝ\right)$$
3		renegcl	$$⊢x\in ℝ\to -x\in ℝ$$
4		negeq	$$⊢z=-x\to -z=-\left(-x\right)$$
5	4	eleq1d	$$⊢z=-x\to \left(-z\in A\leftrightarrow -\left(-x\right)\in A\right)$$
6	5	elrab3	$$⊢-x\in ℝ\to \left(-x\in \left\{z\in ℝ|-z\in A\right\}\leftrightarrow -\left(-x\right)\in A\right)$$
7	3 6	syl	$$⊢x\in ℝ\to \left(-x\in \left\{z\in ℝ|-z\in A\right\}\leftrightarrow -\left(-x\right)\in A\right)$$
8		recn	$$⊢x\in ℝ\to x\in ℂ$$
9	8	negnegd	$$⊢x\in ℝ\to -\left(-x\right)=x$$
10	9	eleq1d	$$⊢x\in ℝ\to \left(-\left(-x\right)\in A\leftrightarrow x\in A\right)$$
11	7 10	bitrd	$$⊢x\in ℝ\to \left(-x\in \left\{z\in ℝ|-z\in A\right\}\leftrightarrow x\in A\right)$$
12	11	biimprd	$$⊢x\in ℝ\to \left(x\in A\to -x\in \left\{z\in ℝ|-z\in A\right\}\right)$$
13	2 12	syli	$$⊢A\subseteq ℝ\to \left(x\in A\to -x\in \left\{z\in ℝ|-z\in A\right\}\right)$$
14		elex2	$$⊢-x\in \left\{z\in ℝ|-z\in A\right\}\to \exists yy\in \left\{z\in ℝ|-z\in A\right\}$$
15	13 14	syl6	$$⊢A\subseteq ℝ\to \left(x\in A\to \exists yy\in \left\{z\in ℝ|-z\in A\right\}\right)$$
16		n0	$$⊢\left\{z\in ℝ|-z\in A\right\}\ne \varnothing \leftrightarrow \exists yy\in \left\{z\in ℝ|-z\in A\right\}$$
17	15 16	imbitrrdi	$$⊢A\subseteq ℝ\to \left(x\in A\to \left\{z\in ℝ|-z\in A\right\}\ne \varnothing \right)$$
18	17	exlimdv	$$⊢A\subseteq ℝ\to \left(\exists xx\in A\to \left\{z\in ℝ|-z\in A\right\}\ne \varnothing \right)$$
19	1 18	biimtrid	$$⊢A\subseteq ℝ\to \left(A\ne \varnothing \to \left\{z\in ℝ|-z\in A\right\}\ne \varnothing \right)$$
20	19	imp	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \right)\to \left\{z\in ℝ|-z\in A\right\}\ne \varnothing$$