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 ⊆ ℝ ∧ A ≠ ∅ → z ∈ ℝ | − z ∈ A ≠ ∅

Proof

Step Hyp Ref Expression
1 n0 ⊢ A ≠ ∅ ↔ ∃ x x ∈ A
2 ssel ⊢ A ⊆ ℝ → x ∈ A → x ∈ ℝ
3 renegcl ⊢ x ∈ ℝ → − x ∈ ℝ
4 negeq ⊢ z = − x → − z = − − x
5 4 eleq1d ⊢ z = − x → − z ∈ A ↔ − − x ∈ A
6 5 elrab3 ⊢ − x ∈ ℝ → − x ∈ z ∈ ℝ | − z ∈ A ↔ − − x ∈ A
7 3 6 syl ⊢ x ∈ ℝ → − x ∈ z ∈ ℝ | − z ∈ A ↔ − − x ∈ A
8 recn ⊢ x ∈ ℝ → x ∈ ℂ
9 8 negnegd ⊢ x ∈ ℝ → − − x = x
10 9 eleq1d ⊢ x ∈ ℝ → − − x ∈ A ↔ x ∈ A
11 7 10 bitrd ⊢ x ∈ ℝ → − x ∈ z ∈ ℝ | − z ∈ A ↔ x ∈ A
12 11 biimprd ⊢ x ∈ ℝ → x ∈ A → − x ∈ z ∈ ℝ | − z ∈ A
13 2 12 syli ⊢ A ⊆ ℝ → x ∈ A → − x ∈ z ∈ ℝ | − z ∈ A
14 elex2 ⊢ − x ∈ z ∈ ℝ | − z ∈ A → ∃ y y ∈ z ∈ ℝ | − z ∈ A
15 13 14 syl6 ⊢ A ⊆ ℝ → x ∈ A → ∃ y y ∈ z ∈ ℝ | − z ∈ A
16 n0 ⊢ z ∈ ℝ | − z ∈ A ≠ ∅ ↔ ∃ y y ∈ z ∈ ℝ | − z ∈ A
17 15 16 imbitrrdi ⊢ A ⊆ ℝ → x ∈ A → z ∈ ℝ | − z ∈ A ≠ ∅
18 17 exlimdv ⊢ A ⊆ ℝ → ∃ x x ∈ A → z ∈ ℝ | − z ∈ A ≠ ∅
19 1 18 biimtrid ⊢ A ⊆ ℝ → A ≠ ∅ → z ∈ ℝ | − z ∈ A ≠ ∅
20 19 imp ⊢ A ⊆ ℝ ∧ A ≠ ∅ → z ∈ ℝ | − z ∈ A ≠ ∅