# Metamath Proof Explorer

## Theorem xrinfmss2

Description: Any subset of extended reals has an infimum. (Contributed by Mario Carneiro, 16-Mar-2014)

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

### Proof

Step Hyp Ref Expression
1 xrinfmss ${⊢}{A}\subseteq {ℝ}^{*}\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{x}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
2 vex ${⊢}{x}\in \mathrm{V}$
3 vex ${⊢}{y}\in \mathrm{V}$
4 2 3 brcnv ${⊢}{x}{<}^{-1}{y}↔{y}<{x}$
5 4 notbii ${⊢}¬{x}{<}^{-1}{y}↔¬{y}<{x}$
6 5 ralbii ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}^{-1}{y}↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{x}$
7 3 2 brcnv ${⊢}{y}{<}^{-1}{x}↔{x}<{y}$
8 vex ${⊢}{z}\in \mathrm{V}$
9 3 8 brcnv ${⊢}{y}{<}^{-1}{z}↔{z}<{y}$
10 9 rexbii ${⊢}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{<}^{-1}{z}↔\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}$
11 7 10 imbi12i ${⊢}\left({y}{<}^{-1}{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{<}^{-1}{z}\right)↔\left({x}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)$
12 11 ralbii ${⊢}\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}{<}^{-1}{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{<}^{-1}{z}\right)↔\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)$
13 6 12 anbi12i ${⊢}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}^{-1}{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}{<}^{-1}{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{<}^{-1}{z}\right)\right)↔\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{x}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
14 13 rexbii ${⊢}\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}^{-1}{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}{<}^{-1}{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{<}^{-1}{z}\right)\right)↔\exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{x}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$
15 1 14 sylibr ${⊢}{A}\subseteq {ℝ}^{*}\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{x}{<}^{-1}{y}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({y}{<}^{-1}{x}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{<}^{-1}{z}\right)\right)$