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	|- ( ph -> A C_ RR* )
	infxrlesupxr.2	|- ( ph -> A =/= (/) )
Assertion	infxrlesupxr	|- ( ph -> inf ( A , RR* , < ) <_ sup ( A , RR* , < ) )

Proof

Step	Hyp	Ref	Expression
1		infxrlesupxr.1	|- ( ph -> A C_ RR* )
2		infxrlesupxr.2	|- ( ph -> A =/= (/) )
3		n0	|- ( A =/= (/) <-> E. x x e. A )
4	3	biimpi	|- ( A =/= (/) -> E. x x e. A )
5	2 4	syl	|- ( ph -> E. x x e. A )
6	1	infxrcld	|- ( ph -> inf ( A , RR* , < ) e. RR* )
7	6	adantr	|- ( ( ph /\ x e. A ) -> inf ( A , RR* , < ) e. RR* )
8	1	sselda	|- ( ( ph /\ x e. A ) -> x e. RR* )
9	1	supxrcld	|- ( ph -> sup ( A , RR* , < ) e. RR* )
10	9	adantr	|- ( ( ph /\ x e. A ) -> sup ( A , RR* , < ) e. RR* )
11	1	adantr	|- ( ( ph /\ x e. A ) -> A C_ RR* )
12		simpr	|- ( ( ph /\ x e. A ) -> x e. A )
13		infxrlb	|- ( ( A C_ RR* /\ x e. A ) -> inf ( A , RR* , < ) <_ x )
14	11 12 13	syl2anc	|- ( ( ph /\ x e. A ) -> inf ( A , RR* , < ) <_ x )
15		eqid	|- sup ( A , RR* , < ) = sup ( A , RR* , < )
16	11 12 15	supxrubd	|- ( ( ph /\ x e. A ) -> x <_ sup ( A , RR* , < ) )
17	7 8 10 14 16	xrletrd	|- ( ( ph /\ x e. A ) -> inf ( A , RR* , < ) <_ sup ( A , RR* , < ) )
18	17	ex	|- ( ph -> ( x e. A -> inf ( A , RR* , < ) <_ sup ( A , RR* , < ) ) )
19	18	exlimdv	|- ( ph -> ( E. x x e. A -> inf ( A , RR* , < ) <_ sup ( A , RR* , < ) ) )
20	5 19	mpd	|- ( ph -> inf ( A , RR* , < ) <_ sup ( A , RR* , < ) )