Theorem taupilemrplb

Description: A set of positive reals has (in the reals) a lower bound. (Contributed by Jim Kingdon, 19-Feb-2019)

	Ref	Expression
Assertion	taupilemrplb	$$⊢\exists x\in ℝ\forall y\in \left({ℝ}^{+}\cap A\right)x\le y$$

Proof

Step	Hyp	Ref	Expression
1		0re	$$⊢0\in ℝ$$
2		inss1	$$⊢{ℝ}^{+}\cap A\subseteq {ℝ}^{+}$$
3	2	sseli	$$⊢y\in \left({ℝ}^{+}\cap A\right)\to y\in {ℝ}^{+}$$
4	3	rpge0d	$$⊢y\in \left({ℝ}^{+}\cap A\right)\to 0\le y$$
5	4	rgen	$$⊢\forall y\in \left({ℝ}^{+}\cap A\right)0\le y$$
6		breq1	$$⊢x=0\to \left(x\le y\leftrightarrow 0\le y\right)$$
7	6	ralbidv	$$⊢x=0\to \left(\forall y\in \left({ℝ}^{+}\cap A\right)x\le y\leftrightarrow \forall y\in \left({ℝ}^{+}\cap A\right)0\le y\right)$$
8	7	rspcev	$$⊢\left(0\in ℝ\wedge \forall y\in \left({ℝ}^{+}\cap A\right)0\le y\right)\to \exists x\in ℝ\forall y\in \left({ℝ}^{+}\cap A\right)x\le y$$
9	1 5 8	mp2an	$$⊢\exists x\in ℝ\forall y\in \left({ℝ}^{+}\cap A\right)x\le y$$