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