# Metamath Proof Explorer

## Theorem xrsupss

Description: Any subset of extended reals has a supremum. (Contributed by NM, 25-Oct-2005)

Ref Expression
Assertion xrsupss ${⊢}{A}\subseteq {ℝ}^{*}\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$

### Proof

Step Hyp Ref Expression
1 xrsupsslem ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge \left({A}\subseteq ℝ\vee \mathrm{+\infty }\in {A}\right)\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
2 ssdifss ${⊢}{A}\subseteq {ℝ}^{*}\to {A}\setminus \left\{\mathrm{-\infty }\right\}\subseteq {ℝ}^{*}$
3 ssxr ${⊢}{A}\setminus \left\{\mathrm{-\infty }\right\}\subseteq {ℝ}^{*}\to \left({A}\setminus \left\{\mathrm{-\infty }\right\}\subseteq ℝ\vee \mathrm{+\infty }\in \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\vee \mathrm{-\infty }\in \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\right)$
4 df-3or ${⊢}\left({A}\setminus \left\{\mathrm{-\infty }\right\}\subseteq ℝ\vee \mathrm{+\infty }\in \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\vee \mathrm{-\infty }\in \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\right)↔\left(\left({A}\setminus \left\{\mathrm{-\infty }\right\}\subseteq ℝ\vee \mathrm{+\infty }\in \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\right)\vee \mathrm{-\infty }\in \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\right)$
5 neldifsn ${⊢}¬\mathrm{-\infty }\in \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)$
6 5 biorfi ${⊢}\left({A}\setminus \left\{\mathrm{-\infty }\right\}\subseteq ℝ\vee \mathrm{+\infty }\in \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\right)↔\left(\left({A}\setminus \left\{\mathrm{-\infty }\right\}\subseteq ℝ\vee \mathrm{+\infty }\in \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\right)\vee \mathrm{-\infty }\in \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\right)$
7 4 6 bitr4i ${⊢}\left({A}\setminus \left\{\mathrm{-\infty }\right\}\subseteq ℝ\vee \mathrm{+\infty }\in \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\vee \mathrm{-\infty }\in \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\right)↔\left({A}\setminus \left\{\mathrm{-\infty }\right\}\subseteq ℝ\vee \mathrm{+\infty }\in \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\right)$
8 3 7 sylib ${⊢}{A}\setminus \left\{\mathrm{-\infty }\right\}\subseteq {ℝ}^{*}\to \left({A}\setminus \left\{\mathrm{-\infty }\right\}\subseteq ℝ\vee \mathrm{+\infty }\in \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\right)$
9 xrsupsslem ${⊢}\left({A}\setminus \left\{\mathrm{-\infty }\right\}\subseteq {ℝ}^{*}\wedge \left({A}\setminus \left\{\mathrm{-\infty }\right\}\subseteq ℝ\vee \mathrm{+\infty }\in \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\right)\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
10 2 8 9 syl2anc2 ${⊢}{A}\subseteq {ℝ}^{*}\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
11 xrsupexmnf ${⊢}\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \left(\left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\cup \left\{\mathrm{-\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in \left(\left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\cup \left\{\mathrm{-\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
12 snssi ${⊢}\mathrm{-\infty }\in {A}\to \left\{\mathrm{-\infty }\right\}\subseteq {A}$
13 undif ${⊢}\left\{\mathrm{-\infty }\right\}\subseteq {A}↔\left\{\mathrm{-\infty }\right\}\cup \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)={A}$
14 uncom ${⊢}\left\{\mathrm{-\infty }\right\}\cup \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)=\left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\cup \left\{\mathrm{-\infty }\right\}$
15 14 eqeq1i ${⊢}\left\{\mathrm{-\infty }\right\}\cup \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)={A}↔\left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\cup \left\{\mathrm{-\infty }\right\}={A}$
16 13 15 bitri ${⊢}\left\{\mathrm{-\infty }\right\}\subseteq {A}↔\left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\cup \left\{\mathrm{-\infty }\right\}={A}$
17 raleq ${⊢}\left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\cup \left\{\mathrm{-\infty }\right\}={A}\to \left(\forall {y}\in \left(\left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\cup \left\{\mathrm{-\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}¬{x}<{y}↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\right)$
18 rexeq ${⊢}\left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\cup \left\{\mathrm{-\infty }\right\}={A}\to \left(\exists {z}\in \left(\left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\cup \left\{\mathrm{-\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}{y}<{z}↔\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)$
19 18 imbi2d ${⊢}\left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\cup \left\{\mathrm{-\infty }\right\}={A}\to \left(\left({y}<{x}\to \exists {z}\in \left(\left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\cup \left\{\mathrm{-\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}{y}<{z}\right)↔\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
20 19 ralbidv ${⊢}\left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\cup \left\{\mathrm{-\infty }\right\}={A}\to \left(\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in \left(\left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\cup \left\{\mathrm{-\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}{y}<{z}\right)↔\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
21 17 20 anbi12d ${⊢}\left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\cup \left\{\mathrm{-\infty }\right\}={A}\to \left(\left(\forall {y}\in \left(\left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\cup \left\{\mathrm{-\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in \left(\left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\cup \left\{\mathrm{-\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)↔\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)$
22 16 21 sylbi ${⊢}\left\{\mathrm{-\infty }\right\}\subseteq {A}\to \left(\left(\forall {y}\in \left(\left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\cup \left\{\mathrm{-\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in \left(\left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\cup \left\{\mathrm{-\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)↔\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)$
23 12 22 syl ${⊢}\mathrm{-\infty }\in {A}\to \left(\left(\forall {y}\in \left(\left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\cup \left\{\mathrm{-\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in \left(\left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\cup \left\{\mathrm{-\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)↔\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)$
24 23 rexbidv ${⊢}\mathrm{-\infty }\in {A}\to \left(\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \left(\left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\cup \left\{\mathrm{-\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in \left(\left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\cup \left\{\mathrm{-\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)↔\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)$
25 11 24 syl5ib ${⊢}\mathrm{-\infty }\in {A}\to \left(\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in \left({A}\setminus \left\{\mathrm{-\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)\right)$
26 10 25 mpan9 ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge \mathrm{-\infty }\in {A}\right)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$
27 ssxr ${⊢}{A}\subseteq {ℝ}^{*}\to \left({A}\subseteq ℝ\vee \mathrm{+\infty }\in {A}\vee \mathrm{-\infty }\in {A}\right)$
28 df-3or ${⊢}\left({A}\subseteq ℝ\vee \mathrm{+\infty }\in {A}\vee \mathrm{-\infty }\in {A}\right)↔\left(\left({A}\subseteq ℝ\vee \mathrm{+\infty }\in {A}\right)\vee \mathrm{-\infty }\in {A}\right)$
29 27 28 sylib ${⊢}{A}\subseteq {ℝ}^{*}\to \left(\left({A}\subseteq ℝ\vee \mathrm{+\infty }\in {A}\right)\vee \mathrm{-\infty }\in {A}\right)$
30 1 26 29 mpjaodan ${⊢}{A}\subseteq {ℝ}^{*}\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}<{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)\right)$