Metamath Proof Explorer


Theorem suprzcl2

Description: The supremum of a bounded-above set of integers is a member of the set. (This version of suprzcl avoids ax-pre-sup .) (Contributed by Mario Carneiro, 21-Apr-2015) (Revised by Mario Carneiro, 24-Dec-2016)

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

Proof

Step Hyp Ref Expression
1 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 ) ) )
2 ssel2
 |-  ( ( A C_ ZZ /\ x e. A ) -> x e. ZZ )
3 2 zred
 |-  ( ( A C_ ZZ /\ x e. A ) -> x e. RR )
4 ltso
 |-  < Or RR
5 4 a1i
 |-  ( T. -> < Or RR )
6 5 eqsup
 |-  ( T. -> ( ( x e. RR /\ A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) -> sup ( A , RR , < ) = x ) )
7 6 mptru
 |-  ( ( x e. RR /\ A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) -> sup ( A , RR , < ) = x )
8 7 3expib
 |-  ( x e. RR -> ( ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) -> sup ( A , RR , < ) = x ) )
9 3 8 syl
 |-  ( ( A C_ ZZ /\ x e. A ) -> ( ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) -> sup ( A , RR , < ) = x ) )
10 simpr
 |-  ( ( A C_ ZZ /\ x e. A ) -> x e. A )
11 eleq1
 |-  ( sup ( A , RR , < ) = x -> ( sup ( A , RR , < ) e. A <-> x e. A ) )
12 10 11 syl5ibrcom
 |-  ( ( A C_ ZZ /\ x e. A ) -> ( sup ( A , RR , < ) = x -> sup ( A , RR , < ) e. A ) )
13 9 12 syld
 |-  ( ( A C_ ZZ /\ x e. A ) -> ( ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) -> sup ( A , RR , < ) e. A ) )
14 13 rexlimdva
 |-  ( A C_ ZZ -> ( E. x e. A ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) -> sup ( A , RR , < ) e. A ) )
15 14 3ad2ant1
 |-  ( ( 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 ) ) -> sup ( A , RR , < ) e. A ) )
16 1 15 mpd
 |-  ( ( A C_ ZZ /\ A =/= (/) /\ E. x e. ZZ A. y e. A y <_ x ) -> sup ( A , RR , < ) e. A )