Metamath Proof Explorer

Theorem iccsupr

Description: A nonempty subset of a closed real interval satisfies the conditions for the existence of its supremum (see suprcl ). (Contributed by Paul Chapman, 21-Jan-2008)

Ref Expression
Assertion iccsupr 
|- ( ( ( A e. RR /\ B e. RR ) /\ S C_ ( A [,] B ) /\ C e. S ) -> ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. y e. S y <_ x ) )

Proof

Step Hyp Ref Expression
1 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
2 sstr 
 |-  ( ( S C_ ( A [,] B ) /\ ( A [,] B ) C_ RR ) -> S C_ RR )
3 2 ancoms 
 |-  ( ( ( A [,] B ) C_ RR /\ S C_ ( A [,] B ) ) -> S C_ RR )
4 1 3 sylan 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ S C_ ( A [,] B ) ) -> S C_ RR )
5 4 3adant3 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ S C_ ( A [,] B ) /\ C e. S ) -> S C_ RR )
6 ne0i 
 |-  ( C e. S -> S =/= (/) )
7 6 3ad2ant3 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ S C_ ( A [,] B ) /\ C e. S ) -> S =/= (/) )
8 simplr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ S C_ ( A [,] B ) ) -> B e. RR )
9 ssel 
 |-  ( S C_ ( A [,] B ) -> ( y e. S -> y e. ( A [,] B ) ) )
10 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( y e. ( A [,] B ) <-> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
11 10 biimpd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( y e. ( A [,] B ) -> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
12 9 11 sylan9r 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ S C_ ( A [,] B ) ) -> ( y e. S -> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
13 12 imp 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ S C_ ( A [,] B ) ) /\ y e. S ) -> ( y e. RR /\ A <_ y /\ y <_ B ) )
14 13 simp3d 
 |-  ( ( ( ( A e. RR /\ B e. RR ) /\ S C_ ( A [,] B ) ) /\ y e. S ) -> y <_ B )
15 14 ralrimiva 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ S C_ ( A [,] B ) ) -> A. y e. S y <_ B )
16 brralrspcev 
 |-  ( ( B e. RR /\ A. y e. S y <_ B ) -> E. x e. RR A. y e. S y <_ x )
17 8 15 16 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ S C_ ( A [,] B ) ) -> E. x e. RR A. y e. S y <_ x )
18 17 3adant3 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ S C_ ( A [,] B ) /\ C e. S ) -> E. x e. RR A. y e. S y <_ x )
19 5 7 18 3jca 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ S C_ ( A [,] B ) /\ C e. S ) -> ( S C_ RR /\ S =/= (/) /\ E. x e. RR A. y e. S y <_ x ) )