Metamath Proof Explorer

Theorem ublbneg

Description: The image under negation of a bounded-above set of reals is bounded below. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion ublbneg ⊢ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x → ∃ x ∈ ℝ ∀ y ∈ z ∈ ℝ | − z ∈ A x ≤ y

Proof

Step Hyp Ref Expression
1 breq1 ⊢ b = y → b ≤ a ↔ y ≤ a
2 1 cbvralvw ⊢ ∀ b ∈ A b ≤ a ↔ ∀ y ∈ A y ≤ a
3 2 rexbii ⊢ ∃ a ∈ ℝ ∀ b ∈ A b ≤ a ↔ ∃ a ∈ ℝ ∀ y ∈ A y ≤ a
4 breq2 ⊢ a = x → y ≤ a ↔ y ≤ x
5 4 ralbidv ⊢ a = x → ∀ y ∈ A y ≤ a ↔ ∀ y ∈ A y ≤ x
6 5 cbvrexvw ⊢ ∃ a ∈ ℝ ∀ y ∈ A y ≤ a ↔ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x
7 3 6 bitri ⊢ ∃ a ∈ ℝ ∀ b ∈ A b ≤ a ↔ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x
8 renegcl ⊢ a ∈ ℝ → − a ∈ ℝ
9 elrabi ⊢ y ∈ z ∈ ℝ | − z ∈ A → y ∈ ℝ
10 negeq ⊢ z = y → − z = − y
11 10 eleq1d ⊢ z = y → − z ∈ A ↔ − y ∈ A
12 11 elrab3 ⊢ y ∈ ℝ → y ∈ z ∈ ℝ | − z ∈ A ↔ − y ∈ A
13 12 biimpd ⊢ y ∈ ℝ → y ∈ z ∈ ℝ | − z ∈ A → − y ∈ A
14 9 13 mpcom ⊢ y ∈ z ∈ ℝ | − z ∈ A → − y ∈ A
15 breq1 ⊢ b = − y → b ≤ a ↔ − y ≤ a
16 15 rspcv ⊢ − y ∈ A → ∀ b ∈ A b ≤ a → − y ≤ a
17 14 16 syl ⊢ y ∈ z ∈ ℝ | − z ∈ A → ∀ b ∈ A b ≤ a → − y ≤ a
18 17 adantl ⊢ a ∈ ℝ ∧ y ∈ z ∈ ℝ | − z ∈ A → ∀ b ∈ A b ≤ a → − y ≤ a
19 lenegcon1 ⊢ a ∈ ℝ ∧ y ∈ ℝ → − a ≤ y ↔ − y ≤ a
20 9 19 sylan2 ⊢ a ∈ ℝ ∧ y ∈ z ∈ ℝ | − z ∈ A → − a ≤ y ↔ − y ≤ a
21 18 20 sylibrd ⊢ a ∈ ℝ ∧ y ∈ z ∈ ℝ | − z ∈ A → ∀ b ∈ A b ≤ a → − a ≤ y
22 21 ralrimdva ⊢ a ∈ ℝ → ∀ b ∈ A b ≤ a → ∀ y ∈ z ∈ ℝ | − z ∈ A − a ≤ y
23 breq1 ⊢ x = − a → x ≤ y ↔ − a ≤ y
24 23 ralbidv ⊢ x = − a → ∀ y ∈ z ∈ ℝ | − z ∈ A x ≤ y ↔ ∀ y ∈ z ∈ ℝ | − z ∈ A − a ≤ y
25 24 rspcev ⊢ − a ∈ ℝ ∧ ∀ y ∈ z ∈ ℝ | − z ∈ A − a ≤ y → ∃ x ∈ ℝ ∀ y ∈ z ∈ ℝ | − z ∈ A x ≤ y
26 8 22 25 syl6an ⊢ a ∈ ℝ → ∀ b ∈ A b ≤ a → ∃ x ∈ ℝ ∀ y ∈ z ∈ ℝ | − z ∈ A x ≤ y
27 26 rexlimiv ⊢ ∃ a ∈ ℝ ∀ b ∈ A b ≤ a → ∃ x ∈ ℝ ∀ y ∈ z ∈ ℝ | − z ∈ A x ≤ y
28 7 27 sylbir ⊢ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x → ∃ x ∈ ℝ ∀ y ∈ z ∈ ℝ | − z ∈ A x ≤ y