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	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
2		ssel	⊢ ( 𝐴 ⊆ ℝ → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℝ ) )
3		renegcl	⊢ ( 𝑥 ∈ ℝ → - 𝑥 ∈ ℝ )
4		negeq	⊢ ( 𝑧 = - 𝑥 → - 𝑧 = - - 𝑥 )
5	4	eleq1d	⊢ ( 𝑧 = - 𝑥 → ( - 𝑧 ∈ 𝐴 ↔ - - 𝑥 ∈ 𝐴 ) )
6	5	elrab3	⊢ ( - 𝑥 ∈ ℝ → ( - 𝑥 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } ↔ - - 𝑥 ∈ 𝐴 ) )
7	3 6	syl	⊢ ( 𝑥 ∈ ℝ → ( - 𝑥 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } ↔ - - 𝑥 ∈ 𝐴 ) )
8		recn	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
9	8	negnegd	⊢ ( 𝑥 ∈ ℝ → - - 𝑥 = 𝑥 )
10	9	eleq1d	⊢ ( 𝑥 ∈ ℝ → ( - - 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 ) )
11	7 10	bitrd	⊢ ( 𝑥 ∈ ℝ → ( - 𝑥 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } ↔ 𝑥 ∈ 𝐴 ) )
12	11	biimprd	⊢ ( 𝑥 ∈ ℝ → ( 𝑥 ∈ 𝐴 → - 𝑥 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } ) )
13	2 12	syli	⊢ ( 𝐴 ⊆ ℝ → ( 𝑥 ∈ 𝐴 → - 𝑥 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } ) )
14		elex2	⊢ ( - 𝑥 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } → ∃ 𝑦 𝑦 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } )
15	13 14	syl6	⊢ ( 𝐴 ⊆ ℝ → ( 𝑥 ∈ 𝐴 → ∃ 𝑦 𝑦 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } ) )
16		n0	⊢ ( { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } )
17	15 16	imbitrrdi	⊢ ( 𝐴 ⊆ ℝ → ( 𝑥 ∈ 𝐴 → { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } ≠ ∅ ) )
18	17	exlimdv	⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑥 𝑥 ∈ 𝐴 → { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } ≠ ∅ ) )
19	1 18	biimtrid	⊢ ( 𝐴 ⊆ ℝ → ( 𝐴 ≠ ∅ → { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } ≠ ∅ ) )
20	19	imp	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } ≠ ∅ )