This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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* , < ) )