# Metamath Proof Explorer

## Theorem xrinfmexpnf

Description: Adding plus infinity to a set does not affect the existence of its infimum. (Contributed by NM, 19-Jan-2006)

Ref Expression
Assertion xrinfmexpnf ${⊢}\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)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \left({A}\cup \left\{\mathrm{+\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}¬{y}<{x}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}<{y}\to \exists {z}\in \left({A}\cup \left\{\mathrm{+\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 elun ${⊢}{y}\in \left({A}\cup \left\{\mathrm{+\infty }\right\}\right)↔\left({y}\in {A}\vee {y}\in \left\{\mathrm{+\infty }\right\}\right)$
2 simpr ${⊢}\left({x}\in {ℝ}^{*}\wedge \left({y}\in {A}\to ¬{y}<{x}\right)\right)\to \left({y}\in {A}\to ¬{y}<{x}\right)$
3 velsn ${⊢}{y}\in \left\{\mathrm{+\infty }\right\}↔{y}=\mathrm{+\infty }$
4 pnfnlt ${⊢}{x}\in {ℝ}^{*}\to ¬\mathrm{+\infty }<{x}$
5 breq1 ${⊢}{y}=\mathrm{+\infty }\to \left({y}<{x}↔\mathrm{+\infty }<{x}\right)$
6 5 notbid ${⊢}{y}=\mathrm{+\infty }\to \left(¬{y}<{x}↔¬\mathrm{+\infty }<{x}\right)$
7 4 6 syl5ibrcom ${⊢}{x}\in {ℝ}^{*}\to \left({y}=\mathrm{+\infty }\to ¬{y}<{x}\right)$
8 3 7 syl5bi ${⊢}{x}\in {ℝ}^{*}\to \left({y}\in \left\{\mathrm{+\infty }\right\}\to ¬{y}<{x}\right)$
9 8 adantr ${⊢}\left({x}\in {ℝ}^{*}\wedge \left({y}\in {A}\to ¬{y}<{x}\right)\right)\to \left({y}\in \left\{\mathrm{+\infty }\right\}\to ¬{y}<{x}\right)$
10 2 9 jaod ${⊢}\left({x}\in {ℝ}^{*}\wedge \left({y}\in {A}\to ¬{y}<{x}\right)\right)\to \left(\left({y}\in {A}\vee {y}\in \left\{\mathrm{+\infty }\right\}\right)\to ¬{y}<{x}\right)$
11 1 10 syl5bi ${⊢}\left({x}\in {ℝ}^{*}\wedge \left({y}\in {A}\to ¬{y}<{x}\right)\right)\to \left({y}\in \left({A}\cup \left\{\mathrm{+\infty }\right\}\right)\to ¬{y}<{x}\right)$
12 11 ex ${⊢}{x}\in {ℝ}^{*}\to \left(\left({y}\in {A}\to ¬{y}<{x}\right)\to \left({y}\in \left({A}\cup \left\{\mathrm{+\infty }\right\}\right)\to ¬{y}<{x}\right)\right)$
13 12 ralimdv2 ${⊢}{x}\in {ℝ}^{*}\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}<{x}\to \forall {y}\in \left({A}\cup \left\{\mathrm{+\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}¬{y}<{x}\right)$
14 elun1 ${⊢}{z}\in {A}\to {z}\in \left({A}\cup \left\{\mathrm{+\infty }\right\}\right)$
15 14 anim1i ${⊢}\left({z}\in {A}\wedge {z}<{y}\right)\to \left({z}\in \left({A}\cup \left\{\mathrm{+\infty }\right\}\right)\wedge {z}<{y}\right)$
16 15 reximi2 ${⊢}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\to \exists {z}\in \left({A}\cup \left\{\mathrm{+\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}{z}<{y}$
17 16 imim2i ${⊢}\left({x}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\to \left({x}<{y}\to \exists {z}\in \left({A}\cup \left\{\mathrm{+\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}{z}<{y}\right)$
18 17 ralimi ${⊢}\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}<{y}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\to \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}<{y}\to \exists {z}\in \left({A}\cup \left\{\mathrm{+\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}{z}<{y}\right)$
19 13 18 anim12d1 ${⊢}{x}\in {ℝ}^{*}\to \left(\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)\to \left(\forall {y}\in \left({A}\cup \left\{\mathrm{+\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}¬{y}<{x}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}<{y}\to \exists {z}\in \left({A}\cup \left\{\mathrm{+\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)\right)$
20 19 reximia ${⊢}\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)\to \exists {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in \left({A}\cup \left\{\mathrm{+\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}¬{y}<{x}\wedge \forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}<{y}\to \exists {z}\in \left({A}\cup \left\{\mathrm{+\infty }\right\}\right)\phantom{\rule{.4em}{0ex}}{z}<{y}\right)\right)$