# 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 ${⊢}\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left\{{z}\in ℝ|-{z}\in {A}\right\}\phantom{\rule{.4em}{0ex}}{x}\le {y}$

### Proof

Step Hyp Ref Expression
1 breq1 ${⊢}{b}={y}\to \left({b}\le {a}↔{y}\le {a}\right)$
2 1 cbvralvw ${⊢}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}{b}\le {a}↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {a}$
3 2 rexbii ${⊢}\exists {a}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}{b}\le {a}↔\exists {a}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {a}$
4 breq2 ${⊢}{a}={x}\to \left({y}\le {a}↔{y}\le {x}\right)$
5 4 ralbidv ${⊢}{a}={x}\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {a}↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)$
6 5 cbvrexvw ${⊢}\exists {a}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {a}↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}$
7 3 6 bitri ${⊢}\exists {a}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}{b}\le {a}↔\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}$
8 renegcl ${⊢}{a}\in ℝ\to -{a}\in ℝ$
9 elrabi ${⊢}{y}\in \left\{{z}\in ℝ|-{z}\in {A}\right\}\to {y}\in ℝ$
10 negeq ${⊢}{z}={y}\to -{z}=-{y}$
11 10 eleq1d ${⊢}{z}={y}\to \left(-{z}\in {A}↔-{y}\in {A}\right)$
12 11 elrab3 ${⊢}{y}\in ℝ\to \left({y}\in \left\{{z}\in ℝ|-{z}\in {A}\right\}↔-{y}\in {A}\right)$
13 12 biimpd ${⊢}{y}\in ℝ\to \left({y}\in \left\{{z}\in ℝ|-{z}\in {A}\right\}\to -{y}\in {A}\right)$
14 9 13 mpcom ${⊢}{y}\in \left\{{z}\in ℝ|-{z}\in {A}\right\}\to -{y}\in {A}$
15 breq1 ${⊢}{b}=-{y}\to \left({b}\le {a}↔-{y}\le {a}\right)$
16 15 rspcv ${⊢}-{y}\in {A}\to \left(\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}{b}\le {a}\to -{y}\le {a}\right)$
17 14 16 syl ${⊢}{y}\in \left\{{z}\in ℝ|-{z}\in {A}\right\}\to \left(\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}{b}\le {a}\to -{y}\le {a}\right)$
18 17 adantl ${⊢}\left({a}\in ℝ\wedge {y}\in \left\{{z}\in ℝ|-{z}\in {A}\right\}\right)\to \left(\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}{b}\le {a}\to -{y}\le {a}\right)$
19 lenegcon1 ${⊢}\left({a}\in ℝ\wedge {y}\in ℝ\right)\to \left(-{a}\le {y}↔-{y}\le {a}\right)$
20 9 19 sylan2 ${⊢}\left({a}\in ℝ\wedge {y}\in \left\{{z}\in ℝ|-{z}\in {A}\right\}\right)\to \left(-{a}\le {y}↔-{y}\le {a}\right)$
21 18 20 sylibrd ${⊢}\left({a}\in ℝ\wedge {y}\in \left\{{z}\in ℝ|-{z}\in {A}\right\}\right)\to \left(\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}{b}\le {a}\to -{a}\le {y}\right)$
22 21 ralrimdva ${⊢}{a}\in ℝ\to \left(\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}{b}\le {a}\to \forall {y}\in \left\{{z}\in ℝ|-{z}\in {A}\right\}\phantom{\rule{.4em}{0ex}}-{a}\le {y}\right)$
23 breq1 ${⊢}{x}=-{a}\to \left({x}\le {y}↔-{a}\le {y}\right)$
24 23 ralbidv ${⊢}{x}=-{a}\to \left(\forall {y}\in \left\{{z}\in ℝ|-{z}\in {A}\right\}\phantom{\rule{.4em}{0ex}}{x}\le {y}↔\forall {y}\in \left\{{z}\in ℝ|-{z}\in {A}\right\}\phantom{\rule{.4em}{0ex}}-{a}\le {y}\right)$
25 24 rspcev ${⊢}\left(-{a}\in ℝ\wedge \forall {y}\in \left\{{z}\in ℝ|-{z}\in {A}\right\}\phantom{\rule{.4em}{0ex}}-{a}\le {y}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left\{{z}\in ℝ|-{z}\in {A}\right\}\phantom{\rule{.4em}{0ex}}{x}\le {y}$
26 8 22 25 syl6an ${⊢}{a}\in ℝ\to \left(\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}{b}\le {a}\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left\{{z}\in ℝ|-{z}\in {A}\right\}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)$
27 26 rexlimiv ${⊢}\exists {a}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {b}\in {A}\phantom{\rule{.4em}{0ex}}{b}\le {a}\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left\{{z}\in ℝ|-{z}\in {A}\right\}\phantom{\rule{.4em}{0ex}}{x}\le {y}$
28 7 27 sylbir ${⊢}\exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \left\{{z}\in ℝ|-{z}\in {A}\right\}\phantom{\rule{.4em}{0ex}}{x}\le {y}$