Metamath Proof Explorer


Theorem suprzub

Description: The supremum of a bounded-above set of integers is greater than any member of the set. (Contributed by Mario Carneiro, 21-Apr-2015)

Ref Expression
Assertion suprzub
|- ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> B <_ sup ( A , RR , < ) )

Proof

Step Hyp Ref Expression
1 simp1
 |-  ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> A C_ ZZ )
2 zssre
 |-  ZZ C_ RR
3 1 2 sstrdi
 |-  ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> A C_ RR )
4 simp3
 |-  ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> B e. A )
5 3 4 sseldd
 |-  ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> B e. RR )
6 4 ne0d
 |-  ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> A =/= (/) )
7 simp2
 |-  ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> E. x e. ZZ A. y e. A y <_ x )
8 suprzcl2
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. ZZ A. y e. A y <_ x ) -> sup ( A , RR , < ) e. A )
9 1 6 7 8 syl3anc
 |-  ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> sup ( A , RR , < ) e. A )
10 3 9 sseldd
 |-  ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> sup ( A , RR , < ) e. RR )
11 ltso
 |-  < Or RR
12 11 a1i
 |-  ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> < Or RR )
13 zsupss
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. ZZ A. y e. A y <_ x ) -> E. x e. A ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )
14 1 6 7 13 syl3anc
 |-  ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> E. x e. A ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )
15 ssrexv
 |-  ( A C_ RR -> ( E. x e. A ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) ) )
16 3 14 15 sylc
 |-  ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )
17 12 16 supub
 |-  ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> ( B e. A -> -. sup ( A , RR , < ) < B ) )
18 4 17 mpd
 |-  ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> -. sup ( A , RR , < ) < B )
19 5 10 18 nltled
 |-  ( ( A C_ ZZ /\ E. x e. ZZ A. y e. A y <_ x /\ B e. A ) -> B <_ sup ( A , RR , < ) )