This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lble

Description: If a set of reals contains a lower bound, the lower bound is less than or equal to all members of the set. (Contributed by NM, 9-Oct-2005) (Proof shortened by Mario Carneiro, 24-Dec-2016)

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

Proof

Step Hyp Ref Expression
1 lbreu 
 |-  ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> E! x e. S A. y e. S x <_ y )
2 nfcv 
 |-  F/_ x S
3 nfriota1 
 |-  F/_ x ( iota_ x e. S A. y e. S x <_ y )
4 nfcv 
 |-  F/_ x <_
5 nfcv 
 |-  F/_ x y
6 3 4 5 nfbr 
 |-  F/ x ( iota_ x e. S A. y e. S x <_ y ) <_ y
7 2 6 nfralw 
 |-  F/ x A. y e. S ( iota_ x e. S A. y e. S x <_ y ) <_ y
8 eqid 
 |-  ( iota_ x e. S A. y e. S x <_ y ) = ( iota_ x e. S A. y e. S x <_ y )
9 nfra1 
 |-  F/ y A. y e. S x <_ y
10 nfcv 
 |-  F/_ y S
11 9 10 nfriota 
 |-  F/_ y ( iota_ x e. S A. y e. S x <_ y )
12 11 nfeq2 
 |-  F/ y x = ( iota_ x e. S A. y e. S x <_ y )
13 breq1 
 |-  ( x = ( iota_ x e. S A. y e. S x <_ y ) -> ( x <_ y <-> ( iota_ x e. S A. y e. S x <_ y ) <_ y ) )
14 12 13 ralbid 
 |-  ( x = ( iota_ x e. S A. y e. S x <_ y ) -> ( A. y e. S x <_ y <-> A. y e. S ( iota_ x e. S A. y e. S x <_ y ) <_ y ) )
15 7 8 14 riotaprop 
 |-  ( E! x e. S A. y e. S x <_ y -> ( ( iota_ x e. S A. y e. S x <_ y ) e. S /\ A. y e. S ( iota_ x e. S A. y e. S x <_ y ) <_ y ) )
16 1 15 syl 
 |-  ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> ( ( iota_ x e. S A. y e. S x <_ y ) e. S /\ A. y e. S ( iota_ x e. S A. y e. S x <_ y ) <_ y ) )
17 16 simprd 
 |-  ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> A. y e. S ( iota_ x e. S A. y e. S x <_ y ) <_ y )
18 nfcv 
 |-  F/_ y <_
19 nfcv 
 |-  F/_ y A
20 11 18 19 nfbr 
 |-  F/ y ( iota_ x e. S A. y e. S x <_ y ) <_ A
21 breq2 
 |-  ( y = A -> ( ( iota_ x e. S A. y e. S x <_ y ) <_ y <-> ( iota_ x e. S A. y e. S x <_ y ) <_ A ) )
22 20 21 rspc 
 |-  ( A e. S -> ( A. y e. S ( iota_ x e. S A. y e. S x <_ y ) <_ y -> ( iota_ x e. S A. y e. S x <_ y ) <_ A ) )
23 17 22 mpan9 
 |-  ( ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) /\ A e. S ) -> ( iota_ x e. S A. y e. S x <_ y ) <_ A )
24 23 3impa 
 |-  ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y /\ A e. S ) -> ( iota_ x e. S A. y e. S x <_ y ) <_ A )