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

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 )