Metamath Proof Explorer

Theorem supminf

Description: The supremum of a bounded-above set of reals is the negation of the infimum of that set's image under negation. (Contributed by Paul Chapman, 21-Mar-2011) ( Revised by AV, 13-Sep-2020.)

Ref Expression
Assertion supminf 
|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) = -u inf ( { z e. RR | -u z e. A } , RR , < ) )

Proof

Step Hyp Ref Expression
1 ssrab2 
 |-  { z e. RR | -u z e. A } C_ RR
2 negn0 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> { z e. RR | -u z e. A } =/= (/) )
3 ublbneg 
 |-  ( E. x e. RR A. y e. A y <_ x -> E. x e. RR A. y e. { z e. RR | -u z e. A } x <_ y )
4 infrenegsup 
 |-  ( ( { z e. RR | -u z e. A } C_ RR /\ { z e. RR | -u z e. A } =/= (/) /\ E. x e. RR A. y e. { z e. RR | -u z e. A } x <_ y ) -> inf ( { z e. RR | -u z e. A } , RR , < ) = -u sup ( { w e. RR | -u w e. { z e. RR | -u z e. A } } , RR , < ) )
5 1 2 3 4 mp3an3an 
 |-  ( ( ( A C_ RR /\ A =/= (/) ) /\ E. x e. RR A. y e. A y <_ x ) -> inf ( { z e. RR | -u z e. A } , RR , < ) = -u sup ( { w e. RR | -u w e. { z e. RR | -u z e. A } } , RR , < ) )
6 5 3impa 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> inf ( { z e. RR | -u z e. A } , RR , < ) = -u sup ( { w e. RR | -u w e. { z e. RR | -u z e. A } } , RR , < ) )
7 elrabi 
 |-  ( x e. { w e. RR | -u w e. { z e. RR | -u z e. A } } -> x e. RR )
8 7 adantl 
 |-  ( ( A C_ RR /\ x e. { w e. RR | -u w e. { z e. RR | -u z e. A } } ) -> x e. RR )
9 ssel2 
 |-  ( ( A C_ RR /\ x e. A ) -> x e. RR )
10 negeq 
 |-  ( w = x -> -u w = -u x )
11 10 eleq1d 
 |-  ( w = x -> ( -u w e. { z e. RR | -u z e. A } <-> -u x e. { z e. RR | -u z e. A } ) )
12 11 elrab3 
 |-  ( x e. RR -> ( x e. { w e. RR | -u w e. { z e. RR | -u z e. A } } <-> -u x e. { z e. RR | -u z e. A } ) )
13 renegcl 
 |-  ( x e. RR -> -u x e. RR )
14 negeq 
 |-  ( z = -u x -> -u z = -u -u x )
15 14 eleq1d 
 |-  ( z = -u x -> ( -u z e. A <-> -u -u x e. A ) )
16 15 elrab3 
 |-  ( -u x e. RR -> ( -u x e. { z e. RR | -u z e. A } <-> -u -u x e. A ) )
17 13 16 syl 
 |-  ( x e. RR -> ( -u x e. { z e. RR | -u z e. A } <-> -u -u x e. A ) )
18 recn 
 |-  ( x e. RR -> x e. CC )
19 18 negnegd 
 |-  ( x e. RR -> -u -u x = x )
20 19 eleq1d 
 |-  ( x e. RR -> ( -u -u x e. A <-> x e. A ) )
21 12 17 20 3bitrd 
 |-  ( x e. RR -> ( x e. { w e. RR | -u w e. { z e. RR | -u z e. A } } <-> x e. A ) )
22 21 adantl 
 |-  ( ( A C_ RR /\ x e. RR ) -> ( x e. { w e. RR | -u w e. { z e. RR | -u z e. A } } <-> x e. A ) )
23 8 9 22 eqrdav 
 |-  ( A C_ RR -> { w e. RR | -u w e. { z e. RR | -u z e. A } } = A )
24 23 supeq1d 
 |-  ( A C_ RR -> sup ( { w e. RR | -u w e. { z e. RR | -u z e. A } } , RR , < ) = sup ( A , RR , < ) )
25 24 3ad2ant1 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( { w e. RR | -u w e. { z e. RR | -u z e. A } } , RR , < ) = sup ( A , RR , < ) )
26 25 negeqd 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> -u sup ( { w e. RR | -u w e. { z e. RR | -u z e. A } } , RR , < ) = -u sup ( A , RR , < ) )
27 6 26 eqtrd 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> inf ( { z e. RR | -u z e. A } , RR , < ) = -u sup ( A , RR , < ) )
28 infrecl 
 |-  ( ( { z e. RR | -u z e. A } C_ RR /\ { z e. RR | -u z e. A } =/= (/) /\ E. x e. RR A. y e. { z e. RR | -u z e. A } x <_ y ) -> inf ( { z e. RR | -u z e. A } , RR , < ) e. RR )
29 1 2 3 28 mp3an3an 
 |-  ( ( ( A C_ RR /\ A =/= (/) ) /\ E. x e. RR A. y e. A y <_ x ) -> inf ( { z e. RR | -u z e. A } , RR , < ) e. RR )
30 29 3impa 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> inf ( { z e. RR | -u z e. A } , RR , < ) e. RR )
31 suprcl 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) e. RR )
32 recn 
 |-  ( inf ( { z e. RR | -u z e. A } , RR , < ) e. RR -> inf ( { z e. RR | -u z e. A } , RR , < ) e. CC )
33 recn 
 |-  ( sup ( A , RR , < ) e. RR -> sup ( A , RR , < ) e. CC )
34 negcon2 
 |-  ( ( inf ( { z e. RR | -u z e. A } , RR , < ) e. CC /\ sup ( A , RR , < ) e. CC ) -> ( inf ( { z e. RR | -u z e. A } , RR , < ) = -u sup ( A , RR , < ) <-> sup ( A , RR , < ) = -u inf ( { z e. RR | -u z e. A } , RR , < ) ) )
35 32 33 34 syl2an 
 |-  ( ( inf ( { z e. RR | -u z e. A } , RR , < ) e. RR /\ sup ( A , RR , < ) e. RR ) -> ( inf ( { z e. RR | -u z e. A } , RR , < ) = -u sup ( A , RR , < ) <-> sup ( A , RR , < ) = -u inf ( { z e. RR | -u z e. A } , RR , < ) ) )
36 30 31 35 syl2anc 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> ( inf ( { z e. RR | -u z e. A } , RR , < ) = -u sup ( A , RR , < ) <-> sup ( A , RR , < ) = -u inf ( { z e. RR | -u z e. A } , RR , < ) ) )
37 27 36 mpbid 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) = -u inf ( { z e. RR | -u z e. A } , RR , < ) )