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 )