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 )