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

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