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

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 syl6ibr ( 𝐴 ⊆ ℝ → ( 𝑥𝐴 → { 𝑧 ∈ ℝ ∣ - 𝑧𝐴 } ≠ ∅ ) )
18 17 exlimdv ( 𝐴 ⊆ ℝ → ( ∃ 𝑥 𝑥𝐴 → { 𝑧 ∈ ℝ ∣ - 𝑧𝐴 } ≠ ∅ ) )
19 1 18 syl5bi ( 𝐴 ⊆ ℝ → ( 𝐴 ≠ ∅ → { 𝑧 ∈ ℝ ∣ - 𝑧𝐴 } ≠ ∅ ) )
20 19 imp ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → { 𝑧 ∈ ℝ ∣ - 𝑧𝐴 } ≠ ∅ )