Metamath Proof Explorer

Theorem lbreu

Description: If a set of reals contains a lower bound, it contains a unique lower bound. (Contributed by NM, 9-Oct-2005)

Ref Expression
Assertion lbreu 
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> E! x e. S A. y e. S x <_ y )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( y = w -> ( x <_ y <-> x <_ w ) )
2 1 rspcv 
 |-  ( w e. S -> ( A. y e. S x <_ y -> x <_ w ) )
3 breq2 
 |-  ( y = x -> ( w <_ y <-> w <_ x ) )
4 3 rspcv 
 |-  ( x e. S -> ( A. y e. S w <_ y -> w <_ x ) )
5 2 4 im2anan9r 
 |-  ( ( x e. S /\ w e. S ) -> ( ( A. y e. S x <_ y /\ A. y e. S w <_ y ) -> ( x <_ w /\ w <_ x ) ) )
6 ssel 
 |-  ( S C_ RR -> ( x e. S -> x e. RR ) )
7 ssel 
 |-  ( S C_ RR -> ( w e. S -> w e. RR ) )
8 6 7 anim12d 
 |-  ( S C_ RR -> ( ( x e. S /\ w e. S ) -> ( x e. RR /\ w e. RR ) ) )
9 8 impcom 
 |-  ( ( ( x e. S /\ w e. S ) /\ S C_ RR ) -> ( x e. RR /\ w e. RR ) )
10 letri3 
 |-  ( ( x e. RR /\ w e. RR ) -> ( x = w <-> ( x <_ w /\ w <_ x ) ) )
11 9 10 syl 
 |-  ( ( ( x e. S /\ w e. S ) /\ S C_ RR ) -> ( x = w <-> ( x <_ w /\ w <_ x ) ) )
12 11 exbiri 
 |-  ( ( x e. S /\ w e. S ) -> ( S C_ RR -> ( ( x <_ w /\ w <_ x ) -> x = w ) ) )
13 12 com23 
 |-  ( ( x e. S /\ w e. S ) -> ( ( x <_ w /\ w <_ x ) -> ( S C_ RR -> x = w ) ) )
14 5 13 syld 
 |-  ( ( x e. S /\ w e. S ) -> ( ( A. y e. S x <_ y /\ A. y e. S w <_ y ) -> ( S C_ RR -> x = w ) ) )
15 14 com3r 
 |-  ( S C_ RR -> ( ( x e. S /\ w e. S ) -> ( ( A. y e. S x <_ y /\ A. y e. S w <_ y ) -> x = w ) ) )
16 15 ralrimivv 
 |-  ( S C_ RR -> A. x e. S A. w e. S ( ( A. y e. S x <_ y /\ A. y e. S w <_ y ) -> x = w ) )
17 16 anim1ci 
 |-  ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> ( E. x e. S A. y e. S x <_ y /\ A. x e. S A. w e. S ( ( A. y e. S x <_ y /\ A. y e. S w <_ y ) -> x = w ) ) )
18 breq1 
 |-  ( x = w -> ( x <_ y <-> w <_ y ) )
19 18 ralbidv 
 |-  ( x = w -> ( A. y e. S x <_ y <-> A. y e. S w <_ y ) )
20 19 reu4 
 |-  ( E! x e. S A. y e. S x <_ y <-> ( E. x e. S A. y e. S x <_ y /\ A. x e. S A. w e. S ( ( A. y e. S x <_ y /\ A. y e. S w <_ y ) -> x = w ) ) )
21 17 20 sylibr 
 |-  ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> E! x e. S A. y e. S x <_ y )