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

Metamath Proof Explorer

Theorem infssuzle

Description: The infimum of a subset of an upper set of integers is less than or equal to all members of the subset. (Contributed by NM, 11-Oct-2005) (Revised by AV, 5-Sep-2020)

Ref Expression
Assertion infssuzle 
|- ( ( S C_ ( ZZ>= ` M ) /\ A e. S ) -> inf ( S , RR , < ) <_ A )

Proof

Step Hyp Ref Expression
1 ne0i 
 |-  ( A e. S -> S =/= (/) )
2 uzwo 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ S =/= (/) ) -> E. j e. S A. k e. S j <_ k )
3 1 2 sylan2 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ A e. S ) -> E. j e. S A. k e. S j <_ k )
4 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
5 zssre 
 |-  ZZ C_ RR
6 4 5 sstri 
 |-  ( ZZ>= ` M ) C_ RR
7 sstr 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ ( ZZ>= ` M ) C_ RR ) -> S C_ RR )
8 6 7 mpan2 
 |-  ( S C_ ( ZZ>= ` M ) -> S C_ RR )
9 lbinfle 
 |-  ( ( S C_ RR /\ E. j e. S A. k e. S j <_ k /\ A e. S ) -> inf ( S , RR , < ) <_ A )
10 9 3com23 
 |-  ( ( S C_ RR /\ A e. S /\ E. j e. S A. k e. S j <_ k ) -> inf ( S , RR , < ) <_ A )
11 8 10 syl3an1 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ A e. S /\ E. j e. S A. k e. S j <_ k ) -> inf ( S , RR , < ) <_ A )
12 3 11 mpd3an3 
 |-  ( ( S C_ ( ZZ>= ` M ) /\ A e. S ) -> inf ( S , RR , < ) <_ A )