Metamath Proof Explorer

Theorem zsupss

Description: Any nonempty bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-sup .) (Contributed by Mario Carneiro, 21-Apr-2015)

Ref Expression
Assertion 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. B ( y < x -> E. z e. A y < z ) ) )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( y = m -> ( y <_ x <-> m <_ x ) )
2 1 cbvralvw 
 |-  ( A. y e. A y <_ x <-> A. m e. A m <_ x )
3 breq2 
 |-  ( x = n -> ( m <_ x <-> m <_ n ) )
4 3 ralbidv 
 |-  ( x = n -> ( A. m e. A m <_ x <-> A. m e. A m <_ n ) )
5 2 4 bitrid 
 |-  ( x = n -> ( A. y e. A y <_ x <-> A. m e. A m <_ n ) )
6 5 cbvrexvw 
 |-  ( E. x e. ZZ A. y e. A y <_ x <-> E. n e. ZZ A. m e. A m <_ n )
7 simp1rl 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ w e. ZZ /\ -u w e. A ) -> n e. ZZ )
8 7 znegcld 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ w e. ZZ /\ -u w e. A ) -> -u n e. ZZ )
9 simp2 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ w e. ZZ /\ -u w e. A ) -> w e. ZZ )
10 9 zred 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ w e. ZZ /\ -u w e. A ) -> w e. RR )
11 7 zred 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ w e. ZZ /\ -u w e. A ) -> n e. RR )
12 breq1 
 |-  ( m = -u w -> ( m <_ n <-> -u w <_ n ) )
13 simp1rr 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ w e. ZZ /\ -u w e. A ) -> A. m e. A m <_ n )
14 simp3 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ w e. ZZ /\ -u w e. A ) -> -u w e. A )
15 12 13 14 rspcdva 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ w e. ZZ /\ -u w e. A ) -> -u w <_ n )
16 10 11 15 lenegcon1d 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ w e. ZZ /\ -u w e. A ) -> -u n <_ w )
17 eluz2 
 |-  ( w e. ( ZZ>= ` -u n ) <-> ( -u n e. ZZ /\ w e. ZZ /\ -u n <_ w ) )
18 8 9 16 17 syl3anbrc 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ w e. ZZ /\ -u w e. A ) -> w e. ( ZZ>= ` -u n ) )
19 18 rabssdv 
 |-  ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) -> { w e. ZZ | -u w e. A } C_ ( ZZ>= ` -u n ) )
20 n0 
 |-  ( A =/= (/) <-> E. n n e. A )
21 ssel2 
 |-  ( ( A C_ ZZ /\ n e. A ) -> n e. ZZ )
22 21 znegcld 
 |-  ( ( A C_ ZZ /\ n e. A ) -> -u n e. ZZ )
23 21 zcnd 
 |-  ( ( A C_ ZZ /\ n e. A ) -> n e. CC )
24 23 negnegd 
 |-  ( ( A C_ ZZ /\ n e. A ) -> -u -u n = n )
25 simpr 
 |-  ( ( A C_ ZZ /\ n e. A ) -> n e. A )
26 24 25 eqeltrd 
 |-  ( ( A C_ ZZ /\ n e. A ) -> -u -u n e. A )
27 negeq 
 |-  ( w = -u n -> -u w = -u -u n )
28 27 eleq1d 
 |-  ( w = -u n -> ( -u w e. A <-> -u -u n e. A ) )
29 28 rspcev 
 |-  ( ( -u n e. ZZ /\ -u -u n e. A ) -> E. w e. ZZ -u w e. A )
30 22 26 29 syl2anc 
 |-  ( ( A C_ ZZ /\ n e. A ) -> E. w e. ZZ -u w e. A )
31 30 ex 
 |-  ( A C_ ZZ -> ( n e. A -> E. w e. ZZ -u w e. A ) )
32 31 exlimdv 
 |-  ( A C_ ZZ -> ( E. n n e. A -> E. w e. ZZ -u w e. A ) )
33 32 imp 
 |-  ( ( A C_ ZZ /\ E. n n e. A ) -> E. w e. ZZ -u w e. A )
34 20 33 sylan2b 
 |-  ( ( A C_ ZZ /\ A =/= (/) ) -> E. w e. ZZ -u w e. A )
35 34 adantr 
 |-  ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) -> E. w e. ZZ -u w e. A )
36 rabn0 
 |-  ( { w e. ZZ | -u w e. A } =/= (/) <-> E. w e. ZZ -u w e. A )
37 35 36 sylibr 
 |-  ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) -> { w e. ZZ | -u w e. A } =/= (/) )
38 infssuzcl 
 |-  ( ( { w e. ZZ | -u w e. A } C_ ( ZZ>= ` -u n ) /\ { w e. ZZ | -u w e. A } =/= (/) ) -> inf ( { w e. ZZ | -u w e. A } , RR , < ) e. { w e. ZZ | -u w e. A } )
39 19 37 38 syl2anc 
 |-  ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) -> inf ( { w e. ZZ | -u w e. A } , RR , < ) e. { w e. ZZ | -u w e. A } )
40 negeq 
 |-  ( n = inf ( { w e. ZZ | -u w e. A } , RR , < ) -> -u n = -u inf ( { w e. ZZ | -u w e. A } , RR , < ) )
41 40 eleq1d 
 |-  ( n = inf ( { w e. ZZ | -u w e. A } , RR , < ) -> ( -u n e. A <-> -u inf ( { w e. ZZ | -u w e. A } , RR , < ) e. A ) )
42 negeq 
 |-  ( w = n -> -u w = -u n )
43 42 eleq1d 
 |-  ( w = n -> ( -u w e. A <-> -u n e. A ) )
44 43 cbvrabv 
 |-  { w e. ZZ | -u w e. A } = { n e. ZZ | -u n e. A }
45 41 44 elrab2 
 |-  ( inf ( { w e. ZZ | -u w e. A } , RR , < ) e. { w e. ZZ | -u w e. A } <-> ( inf ( { w e. ZZ | -u w e. A } , RR , < ) e. ZZ /\ -u inf ( { w e. ZZ | -u w e. A } , RR , < ) e. A ) )
46 45 simprbi 
 |-  ( inf ( { w e. ZZ | -u w e. A } , RR , < ) e. { w e. ZZ | -u w e. A } -> -u inf ( { w e. ZZ | -u w e. A } , RR , < ) e. A )
47 39 46 syl 
 |-  ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) -> -u inf ( { w e. ZZ | -u w e. A } , RR , < ) e. A )
48 simpll 
 |-  ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) -> A C_ ZZ )
49 48 sselda 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ y e. A ) -> y e. ZZ )
50 49 zred 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ y e. A ) -> y e. RR )
51 ssrab2 
 |-  { w e. ZZ | -u w e. A } C_ ZZ
52 39 adantr 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ y e. A ) -> inf ( { w e. ZZ | -u w e. A } , RR , < ) e. { w e. ZZ | -u w e. A } )
53 51 52 sselid 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ y e. A ) -> inf ( { w e. ZZ | -u w e. A } , RR , < ) e. ZZ )
54 53 znegcld 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ y e. A ) -> -u inf ( { w e. ZZ | -u w e. A } , RR , < ) e. ZZ )
55 54 zred 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ y e. A ) -> -u inf ( { w e. ZZ | -u w e. A } , RR , < ) e. RR )
56 53 zred 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ y e. A ) -> inf ( { w e. ZZ | -u w e. A } , RR , < ) e. RR )
57 19 adantr 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ y e. A ) -> { w e. ZZ | -u w e. A } C_ ( ZZ>= ` -u n ) )
58 negeq 
 |-  ( w = -u y -> -u w = -u -u y )
59 58 eleq1d 
 |-  ( w = -u y -> ( -u w e. A <-> -u -u y e. A ) )
60 49 znegcld 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ y e. A ) -> -u y e. ZZ )
61 49 zcnd 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ y e. A ) -> y e. CC )
62 61 negnegd 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ y e. A ) -> -u -u y = y )
63 simpr 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ y e. A ) -> y e. A )
64 62 63 eqeltrd 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ y e. A ) -> -u -u y e. A )
65 59 60 64 elrabd 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ y e. A ) -> -u y e. { w e. ZZ | -u w e. A } )
66 infssuzle 
 |-  ( ( { w e. ZZ | -u w e. A } C_ ( ZZ>= ` -u n ) /\ -u y e. { w e. ZZ | -u w e. A } ) -> inf ( { w e. ZZ | -u w e. A } , RR , < ) <_ -u y )
67 57 65 66 syl2anc 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ y e. A ) -> inf ( { w e. ZZ | -u w e. A } , RR , < ) <_ -u y )
68 56 50 67 lenegcon2d 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ y e. A ) -> y <_ -u inf ( { w e. ZZ | -u w e. A } , RR , < ) )
69 50 55 68 lensymd 
 |-  ( ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) /\ y e. A ) -> -. -u inf ( { w e. ZZ | -u w e. A } , RR , < ) < y )
70 69 ralrimiva 
 |-  ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) -> A. y e. A -. -u inf ( { w e. ZZ | -u w e. A } , RR , < ) < y )
71 breq2 
 |-  ( z = -u inf ( { w e. ZZ | -u w e. A } , RR , < ) -> ( y < z <-> y < -u inf ( { w e. ZZ | -u w e. A } , RR , < ) ) )
72 71 rspcev 
 |-  ( ( -u inf ( { w e. ZZ | -u w e. A } , RR , < ) e. A /\ y < -u inf ( { w e. ZZ | -u w e. A } , RR , < ) ) -> E. z e. A y < z )
73 72 ex 
 |-  ( -u inf ( { w e. ZZ | -u w e. A } , RR , < ) e. A -> ( y < -u inf ( { w e. ZZ | -u w e. A } , RR , < ) -> E. z e. A y < z ) )
74 47 73 syl 
 |-  ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) -> ( y < -u inf ( { w e. ZZ | -u w e. A } , RR , < ) -> E. z e. A y < z ) )
75 74 ralrimivw 
 |-  ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) -> A. y e. B ( y < -u inf ( { w e. ZZ | -u w e. A } , RR , < ) -> E. z e. A y < z ) )
76 breq1 
 |-  ( x = -u inf ( { w e. ZZ | -u w e. A } , RR , < ) -> ( x < y <-> -u inf ( { w e. ZZ | -u w e. A } , RR , < ) < y ) )
77 76 notbid 
 |-  ( x = -u inf ( { w e. ZZ | -u w e. A } , RR , < ) -> ( -. x < y <-> -. -u inf ( { w e. ZZ | -u w e. A } , RR , < ) < y ) )
78 77 ralbidv 
 |-  ( x = -u inf ( { w e. ZZ | -u w e. A } , RR , < ) -> ( A. y e. A -. x < y <-> A. y e. A -. -u inf ( { w e. ZZ | -u w e. A } , RR , < ) < y ) )
79 breq2 
 |-  ( x = -u inf ( { w e. ZZ | -u w e. A } , RR , < ) -> ( y < x <-> y < -u inf ( { w e. ZZ | -u w e. A } , RR , < ) ) )
80 79 imbi1d 
 |-  ( x = -u inf ( { w e. ZZ | -u w e. A } , RR , < ) -> ( ( y < x -> E. z e. A y < z ) <-> ( y < -u inf ( { w e. ZZ | -u w e. A } , RR , < ) -> E. z e. A y < z ) ) )
81 80 ralbidv 
 |-  ( x = -u inf ( { w e. ZZ | -u w e. A } , RR , < ) -> ( A. y e. B ( y < x -> E. z e. A y < z ) <-> A. y e. B ( y < -u inf ( { w e. ZZ | -u w e. A } , RR , < ) -> E. z e. A y < z ) ) )
82 78 81 anbi12d 
 |-  ( x = -u inf ( { w e. ZZ | -u w e. A } , RR , < ) -> ( ( A. y e. A -. x < y /\ A. y e. B ( y < x -> E. z e. A y < z ) ) <-> ( A. y e. A -. -u inf ( { w e. ZZ | -u w e. A } , RR , < ) < y /\ A. y e. B ( y < -u inf ( { w e. ZZ | -u w e. A } , RR , < ) -> E. z e. A y < z ) ) ) )
83 82 rspcev 
 |-  ( ( -u inf ( { w e. ZZ | -u w e. A } , RR , < ) e. A /\ ( A. y e. A -. -u inf ( { w e. ZZ | -u w e. A } , RR , < ) < y /\ A. y e. B ( y < -u inf ( { w e. ZZ | -u w e. A } , RR , < ) -> E. z e. A y < z ) ) ) -> E. x e. A ( A. y e. A -. x < y /\ A. y e. B ( y < x -> E. z e. A y < z ) ) )
84 47 70 75 83 syl12anc 
 |-  ( ( ( A C_ ZZ /\ A =/= (/) ) /\ ( n e. ZZ /\ A. m e. A m <_ n ) ) -> E. x e. A ( A. y e. A -. x < y /\ A. y e. B ( y < x -> E. z e. A y < z ) ) )
85 84 rexlimdvaa 
 |-  ( ( A C_ ZZ /\ A =/= (/) ) -> ( E. n e. ZZ A. m e. A m <_ n -> E. x e. A ( A. y e. A -. x < y /\ A. y e. B ( y < x -> E. z e. A y < z ) ) ) )
86 6 85 biimtrid 
 |-  ( ( 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. B ( y < x -> E. z e. A y < z ) ) ) )
87 86 3impia 
 |-  ( ( 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. B ( y < x -> E. z e. A y < z ) ) )