# Metamath Proof Explorer

## Theorem supxrre

Description: The real and extended real suprema match when the real supremum exists. (Contributed by NM, 18-Oct-2005) (Proof shortened by Mario Carneiro, 7-Sep-2014)

Ref Expression
Assertion supxrre ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to sup\left({A},{ℝ}^{*},<\right)=sup\left({A},ℝ,<\right)$

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to {A}\subseteq ℝ$
2 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
3 1 2 sstrdi ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to {A}\subseteq {ℝ}^{*}$
4 supxrcl ${⊢}{A}\subseteq {ℝ}^{*}\to sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}$
5 3 4 syl ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}$
6 suprcl ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to sup\left({A},ℝ,<\right)\in ℝ$
7 6 rexrd ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to sup\left({A},ℝ,<\right)\in {ℝ}^{*}$
8 6 leidd ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to sup\left({A},ℝ,<\right)\le sup\left({A},ℝ,<\right)$
9 suprleub ${⊢}\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\wedge sup\left({A},ℝ,<\right)\in ℝ\right)\to \left(sup\left({A},ℝ,<\right)\le sup\left({A},ℝ,<\right)↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}\le sup\left({A},ℝ,<\right)\right)$
10 6 9 mpdan ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to \left(sup\left({A},ℝ,<\right)\le sup\left({A},ℝ,<\right)↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}\le sup\left({A},ℝ,<\right)\right)$
11 supxrleub ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge sup\left({A},ℝ,<\right)\in {ℝ}^{*}\right)\to \left(sup\left({A},{ℝ}^{*},<\right)\le sup\left({A},ℝ,<\right)↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}\le sup\left({A},ℝ,<\right)\right)$
12 3 7 11 syl2anc ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to \left(sup\left({A},{ℝ}^{*},<\right)\le sup\left({A},ℝ,<\right)↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}\le sup\left({A},ℝ,<\right)\right)$
13 10 12 bitr4d ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to \left(sup\left({A},ℝ,<\right)\le sup\left({A},ℝ,<\right)↔sup\left({A},{ℝ}^{*},<\right)\le sup\left({A},ℝ,<\right)\right)$
14 8 13 mpbid ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to sup\left({A},{ℝ}^{*},<\right)\le sup\left({A},ℝ,<\right)$
15 5 xrleidd ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to sup\left({A},{ℝ}^{*},<\right)\le sup\left({A},{ℝ}^{*},<\right)$
16 supxrleub ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}\right)\to \left(sup\left({A},{ℝ}^{*},<\right)\le sup\left({A},{ℝ}^{*},<\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le sup\left({A},{ℝ}^{*},<\right)\right)$
17 3 5 16 syl2anc ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to \left(sup\left({A},{ℝ}^{*},<\right)\le sup\left({A},{ℝ}^{*},<\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le sup\left({A},{ℝ}^{*},<\right)\right)$
18 simp2 ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to {A}\ne \varnothing$
19 n0 ${⊢}{A}\ne \varnothing ↔\exists {z}\phantom{\rule{.4em}{0ex}}{z}\in {A}$
20 18 19 sylib ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to \exists {z}\phantom{\rule{.4em}{0ex}}{z}\in {A}$
21 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
22 21 a1i ${⊢}\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\wedge {z}\in {A}\right)\to \mathrm{-\infty }\in {ℝ}^{*}$
23 1 sselda ${⊢}\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\wedge {z}\in {A}\right)\to {z}\in ℝ$
24 23 rexrd ${⊢}\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\wedge {z}\in {A}\right)\to {z}\in {ℝ}^{*}$
25 5 adantr ${⊢}\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\wedge {z}\in {A}\right)\to sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}$
26 23 mnfltd ${⊢}\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\wedge {z}\in {A}\right)\to \mathrm{-\infty }<{z}$
27 supxrub ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {z}\in {A}\right)\to {z}\le sup\left({A},{ℝ}^{*},<\right)$
28 3 27 sylan ${⊢}\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\wedge {z}\in {A}\right)\to {z}\le sup\left({A},{ℝ}^{*},<\right)$
29 22 24 25 26 28 xrltletrd ${⊢}\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\wedge {z}\in {A}\right)\to \mathrm{-\infty }
30 20 29 exlimddv ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to \mathrm{-\infty }
31 xrre ${⊢}\left(\left(sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}\wedge sup\left({A},ℝ,<\right)\in ℝ\right)\wedge \left(\mathrm{-\infty }
32 5 6 30 14 31 syl22anc ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to sup\left({A},{ℝ}^{*},<\right)\in ℝ$
33 suprleub ${⊢}\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\wedge sup\left({A},{ℝ}^{*},<\right)\in ℝ\right)\to \left(sup\left({A},ℝ,<\right)\le sup\left({A},{ℝ}^{*},<\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le sup\left({A},{ℝ}^{*},<\right)\right)$
34 32 33 mpdan ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to \left(sup\left({A},ℝ,<\right)\le sup\left({A},{ℝ}^{*},<\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le sup\left({A},{ℝ}^{*},<\right)\right)$
35 17 34 bitr4d ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to \left(sup\left({A},{ℝ}^{*},<\right)\le sup\left({A},{ℝ}^{*},<\right)↔sup\left({A},ℝ,<\right)\le sup\left({A},{ℝ}^{*},<\right)\right)$
36 15 35 mpbid ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to sup\left({A},ℝ,<\right)\le sup\left({A},{ℝ}^{*},<\right)$
37 5 7 14 36 xrletrid ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{y}\le {x}\right)\to sup\left({A},{ℝ}^{*},<\right)=sup\left({A},ℝ,<\right)$