Metamath Proof Explorer

Theorem uzsupss

Description: Any bounded subset of an upper set of integers has a supremum. (Contributed by Mario Carneiro, 22-Jul-2014) (Revised by Mario Carneiro, 21-Apr-2015)

Ref Expression
Hypothesis uzsupss.1 
|- Z = ( ZZ>= ` M )
Assertion uzsupss 
|- ( ( M e. ZZ /\ A C_ Z /\ E. x e. ZZ A. y e. A y <_ x ) -> E. x e. Z ( A. y e. A -. x < y /\ A. y e. Z ( y < x -> E. z e. A y < z ) ) )

Proof

Step Hyp Ref Expression
1 uzsupss.1 
 |-  Z = ( ZZ>= ` M )
2 simpl1 
 |-  ( ( ( M e. ZZ /\ A C_ Z /\ E. x e. ZZ A. y e. A y <_ x ) /\ A = (/) ) -> M e. ZZ )
3 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
4 2 3 syl 
 |-  ( ( ( M e. ZZ /\ A C_ Z /\ E. x e. ZZ A. y e. A y <_ x ) /\ A = (/) ) -> M e. ( ZZ>= ` M ) )
5 4 1 eleqtrrdi 
 |-  ( ( ( M e. ZZ /\ A C_ Z /\ E. x e. ZZ A. y e. A y <_ x ) /\ A = (/) ) -> M e. Z )
6 ral0 
 |-  A. y e. (/) -. M < y
7 simpr 
 |-  ( ( ( M e. ZZ /\ A C_ Z /\ E. x e. ZZ A. y e. A y <_ x ) /\ A = (/) ) -> A = (/) )
8 7 raleqdv 
 |-  ( ( ( M e. ZZ /\ A C_ Z /\ E. x e. ZZ A. y e. A y <_ x ) /\ A = (/) ) -> ( A. y e. A -. M < y <-> A. y e. (/) -. M < y ) )
9 6 8 mpbiri 
 |-  ( ( ( M e. ZZ /\ A C_ Z /\ E. x e. ZZ A. y e. A y <_ x ) /\ A = (/) ) -> A. y e. A -. M < y )
10 eluzle 
 |-  ( y e. ( ZZ>= ` M ) -> M <_ y )
11 eluzel2 
 |-  ( y e. ( ZZ>= ` M ) -> M e. ZZ )
12 eluzelz 
 |-  ( y e. ( ZZ>= ` M ) -> y e. ZZ )
13 zre 
 |-  ( M e. ZZ -> M e. RR )
14 zre 
 |-  ( y e. ZZ -> y e. RR )
15 lenlt 
 |-  ( ( M e. RR /\ y e. RR ) -> ( M <_ y <-> -. y < M ) )
16 13 14 15 syl2an 
 |-  ( ( M e. ZZ /\ y e. ZZ ) -> ( M <_ y <-> -. y < M ) )
17 11 12 16 syl2anc 
 |-  ( y e. ( ZZ>= ` M ) -> ( M <_ y <-> -. y < M ) )
18 10 17 mpbid 
 |-  ( y e. ( ZZ>= ` M ) -> -. y < M )
19 18 1 eleq2s 
 |-  ( y e. Z -> -. y < M )
20 19 pm2.21d 
 |-  ( y e. Z -> ( y < M -> E. z e. A y < z ) )
21 20 rgen 
 |-  A. y e. Z ( y < M -> E. z e. A y < z )
22 21 a1i 
 |-  ( ( ( M e. ZZ /\ A C_ Z /\ E. x e. ZZ A. y e. A y <_ x ) /\ A = (/) ) -> A. y e. Z ( y < M -> E. z e. A y < z ) )
23 breq1 
 |-  ( x = M -> ( x < y <-> M < y ) )
24 23 notbid 
 |-  ( x = M -> ( -. x < y <-> -. M < y ) )
25 24 ralbidv 
 |-  ( x = M -> ( A. y e. A -. x < y <-> A. y e. A -. M < y ) )
26 breq2 
 |-  ( x = M -> ( y < x <-> y < M ) )
27 26 imbi1d 
 |-  ( x = M -> ( ( y < x -> E. z e. A y < z ) <-> ( y < M -> E. z e. A y < z ) ) )
28 27 ralbidv 
 |-  ( x = M -> ( A. y e. Z ( y < x -> E. z e. A y < z ) <-> A. y e. Z ( y < M -> E. z e. A y < z ) ) )
29 25 28 anbi12d 
 |-  ( x = M -> ( ( A. y e. A -. x < y /\ A. y e. Z ( y < x -> E. z e. A y < z ) ) <-> ( A. y e. A -. M < y /\ A. y e. Z ( y < M -> E. z e. A y < z ) ) ) )
30 29 rspcev 
 |-  ( ( M e. Z /\ ( A. y e. A -. M < y /\ A. y e. Z ( y < M -> E. z e. A y < z ) ) ) -> E. x e. Z ( A. y e. A -. x < y /\ A. y e. Z ( y < x -> E. z e. A y < z ) ) )
31 5 9 22 30 syl12anc 
 |-  ( ( ( M e. ZZ /\ A C_ Z /\ E. x e. ZZ A. y e. A y <_ x ) /\ A = (/) ) -> E. x e. Z ( A. y e. A -. x < y /\ A. y e. Z ( y < x -> E. z e. A y < z ) ) )
32 simpl2 
 |-  ( ( ( M e. ZZ /\ A C_ Z /\ E. x e. ZZ A. y e. A y <_ x ) /\ A =/= (/) ) -> A C_ Z )
33 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
34 1 33 eqsstri 
 |-  Z C_ ZZ
35 32 34 sstrdi 
 |-  ( ( ( M e. ZZ /\ A C_ Z /\ E. x e. ZZ A. y e. A y <_ x ) /\ A =/= (/) ) -> A C_ ZZ )
36 simpr 
 |-  ( ( ( M e. ZZ /\ A C_ Z /\ E. x e. ZZ A. y e. A y <_ x ) /\ A =/= (/) ) -> A =/= (/) )
37 simpl3 
 |-  ( ( ( M e. ZZ /\ A C_ Z /\ E. x e. ZZ A. y e. A y <_ x ) /\ A =/= (/) ) -> E. x e. ZZ A. y e. A y <_ x )
38 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. Z ( y < x -> E. z e. A y < z ) ) )
39 35 36 37 38 syl3anc 
 |-  ( ( ( M e. ZZ /\ A C_ Z /\ E. x e. ZZ A. y e. A y <_ x ) /\ A =/= (/) ) -> E. x e. A ( A. y e. A -. x < y /\ A. y e. Z ( y < x -> E. z e. A y < z ) ) )
40 ssrexv 
 |-  ( A C_ Z -> ( E. x e. A ( A. y e. A -. x < y /\ A. y e. Z ( y < x -> E. z e. A y < z ) ) -> E. x e. Z ( A. y e. A -. x < y /\ A. y e. Z ( y < x -> E. z e. A y < z ) ) ) )
41 32 39 40 sylc 
 |-  ( ( ( M e. ZZ /\ A C_ Z /\ E. x e. ZZ A. y e. A y <_ x ) /\ A =/= (/) ) -> E. x e. Z ( A. y e. A -. x < y /\ A. y e. Z ( y < x -> E. z e. A y < z ) ) )
42 31 41 pm2.61dane 
 |-  ( ( M e. ZZ /\ A C_ Z /\ E. x e. ZZ A. y e. A y <_ x ) -> E. x e. Z ( A. y e. A -. x < y /\ A. y e. Z ( y < x -> E. z e. A y < z ) ) )