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