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 {ℝ}^{*}\left(\forall y\in A\neg y<x\wedge \forall y\in {ℝ}^{*}\left(x<y\to \exists z\in Az<y\right)\right)\to \exists x\in {ℝ}^{*}\left(\forall y\in \left(A\cup \left\{\mathrm{+\infty }\right\}\right)\neg y<x\wedge \forall y\in {ℝ}^{*}\left(x<y\to \exists z\in \left(A\cup \left\{\mathrm{+\infty }\right\}\right)z<y\right)\right)$$

Proof

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