# Metamath Proof Explorer

## Theorem infxrre

Description: The real and extended real infima match when the real infimum exists. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 5-Sep-2020)

Ref Expression
Assertion infxrre ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\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}}{x}\le {y}\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}}{x}\le {y}\right)\to {A}\subseteq {ℝ}^{*}$
4 infxrcl ${⊢}{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}}{x}\le {y}\right)\to sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}$
6 infrecl ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\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}}{x}\le {y}\right)\to sup\left({A},ℝ,<\right)\in {ℝ}^{*}$
8 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}}{x}\le {y}\right)\to sup\left({A},{ℝ}^{*},<\right)\le sup\left({A},{ℝ}^{*},<\right)$
9 infxrgelb ${⊢}\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}}sup\left({A},{ℝ}^{*},<\right)\le {x}\right)$
10 3 5 9 syl2anc ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to \left(sup\left({A},{ℝ}^{*},<\right)\le sup\left({A},{ℝ}^{*},<\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}sup\left({A},{ℝ}^{*},<\right)\le {x}\right)$
11 simp2 ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to {A}\ne \varnothing$
12 n0 ${⊢}{A}\ne \varnothing ↔\exists {z}\phantom{\rule{.4em}{0ex}}{z}\in {A}$
13 11 12 sylib ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to \exists {z}\phantom{\rule{.4em}{0ex}}{z}\in {A}$
14 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}}{x}\le {y}\right)\wedge {z}\in {A}\right)\to sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}$
15 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}}{x}\le {y}\right)\wedge {z}\in {A}\right)\to {z}\in ℝ$
16 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
17 16 a1i ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to \mathrm{-\infty }\in {ℝ}^{*}$
18 6 mnfltd ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to \mathrm{-\infty }
19 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}}{x}\le {y}\right)\to sup\left({A},ℝ,<\right)\le sup\left({A},ℝ,<\right)$
20 infregelb ${⊢}\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\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}}sup\left({A},ℝ,<\right)\le {x}\right)$
21 6 20 mpdan ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to \left(sup\left({A},ℝ,<\right)\le sup\left({A},ℝ,<\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}sup\left({A},ℝ,<\right)\le {x}\right)$
22 infxrgelb ${⊢}\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}}sup\left({A},ℝ,<\right)\le {x}\right)$
23 3 7 22 syl2anc ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to \left(sup\left({A},ℝ,<\right)\le sup\left({A},{ℝ}^{*},<\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}sup\left({A},ℝ,<\right)\le {x}\right)$
24 21 23 bitr4d ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to \left(sup\left({A},ℝ,<\right)\le sup\left({A},ℝ,<\right)↔sup\left({A},ℝ,<\right)\le sup\left({A},{ℝ}^{*},<\right)\right)$
25 19 24 mpbid ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to sup\left({A},ℝ,<\right)\le sup\left({A},{ℝ}^{*},<\right)$
26 17 7 5 18 25 xrltletrd ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to \mathrm{-\infty }
27 26 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}}{x}\le {y}\right)\wedge {z}\in {A}\right)\to \mathrm{-\infty }
28 infxrlb ${⊢}\left({A}\subseteq {ℝ}^{*}\wedge {z}\in {A}\right)\to sup\left({A},{ℝ}^{*},<\right)\le {z}$
29 3 28 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}}{x}\le {y}\right)\wedge {z}\in {A}\right)\to sup\left({A},{ℝ}^{*},<\right)\le {z}$
30 xrre ${⊢}\left(\left(sup\left({A},{ℝ}^{*},<\right)\in {ℝ}^{*}\wedge {z}\in ℝ\right)\wedge \left(\mathrm{-\infty }
31 14 15 27 29 30 syl22anc ${⊢}\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\wedge {z}\in {A}\right)\to sup\left({A},{ℝ}^{*},<\right)\in ℝ$
32 13 31 exlimddv ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to sup\left({A},{ℝ}^{*},<\right)\in ℝ$
33 infregelb ${⊢}\left(\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\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}}sup\left({A},{ℝ}^{*},<\right)\le {x}\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}}{x}\le {y}\right)\to \left(sup\left({A},{ℝ}^{*},<\right)\le sup\left({A},ℝ,<\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}sup\left({A},{ℝ}^{*},<\right)\le {x}\right)$
35 10 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}}{x}\le {y}\right)\to \left(sup\left({A},{ℝ}^{*},<\right)\le sup\left({A},{ℝ}^{*},<\right)↔sup\left({A},{ℝ}^{*},<\right)\le sup\left({A},ℝ,<\right)\right)$
36 8 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}}{x}\le {y}\right)\to sup\left({A},{ℝ}^{*},<\right)\le sup\left({A},ℝ,<\right)$
37 5 7 36 25 xrletrid ${⊢}\left({A}\subseteq ℝ\wedge {A}\ne \varnothing \wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{x}\le {y}\right)\to sup\left({A},{ℝ}^{*},<\right)=sup\left({A},ℝ,<\right)$