Theorem infxrlesupxr

Description: The supremum of a nonempty set is greater than or equal to the infimum. The second condition is needed, see supxrltinfxr . (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	infxrlesupxr.1	$$⊢\phi \to A\subseteq {ℝ}^{*}$$
	infxrlesupxr.2	$$⊢\phi \to A\ne \varnothing$$
Assertion	infxrlesupxr	$$⊢\phi \to inf\left(A,{ℝ}^{*},<\right)\le sup\left(A,{ℝ}^{*},<\right)$$

Proof

Step	Hyp	Ref	Expression
1		infxrlesupxr.1	$$⊢\phi \to A\subseteq {ℝ}^{*}$$
2		infxrlesupxr.2	$$⊢\phi \to A\ne \varnothing$$
3		n0	$$⊢A\ne \varnothing \leftrightarrow \exists xx\in A$$
4	3	biimpi	$$⊢A\ne \varnothing \to \exists xx\in A$$
5	2 4	syl	$$⊢\phi \to \exists xx\in A$$
6	1	infxrcld	$$⊢\phi \to inf\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}$$
7	6	adantr	$$⊢\left(\phi \wedge x\in A\right)\to inf\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}$$
8	1	sselda	$$⊢\left(\phi \wedge x\in A\right)\to x\in {ℝ}^{*}$$
9	1	supxrcld	$$⊢\phi \to sup\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}$$
10	9	adantr	$$⊢\left(\phi \wedge x\in A\right)\to sup\left(A,{ℝ}^{*},<\right)\in {ℝ}^{*}$$
11	1	adantr	$$⊢\left(\phi \wedge x\in A\right)\to A\subseteq {ℝ}^{*}$$
12		simpr	$$⊢\left(\phi \wedge x\in A\right)\to x\in A$$
13		infxrlb	$$⊢\left(A\subseteq {ℝ}^{*}\wedge x\in A\right)\to inf\left(A,{ℝ}^{*},<\right)\le x$$
14	11 12 13	syl2anc	$$⊢\left(\phi \wedge x\in A\right)\to inf\left(A,{ℝ}^{*},<\right)\le x$$
15		eqid	$$⊢sup\left(A,{ℝ}^{*},<\right)=sup\left(A,{ℝ}^{*},<\right)$$
16	11 12 15	supxrubd	$$⊢\left(\phi \wedge x\in A\right)\to x\le sup\left(A,{ℝ}^{*},<\right)$$
17	7 8 10 14 16	xrletrd	$$⊢\left(\phi \wedge x\in A\right)\to inf\left(A,{ℝ}^{*},<\right)\le sup\left(A,{ℝ}^{*},<\right)$$
18	17	ex	$$⊢\phi \to \left(x\in A\to inf\left(A,{ℝ}^{*},<\right)\le sup\left(A,{ℝ}^{*},<\right)\right)$$
19	18	exlimdv	$$⊢\phi \to \left(\exists xx\in A\to inf\left(A,{ℝ}^{*},<\right)\le sup\left(A,{ℝ}^{*},<\right)\right)$$
20	5 19	mpd	$$⊢\phi \to inf\left(A,{ℝ}^{*},<\right)\le sup\left(A,{ℝ}^{*},<\right)$$