Step |
Hyp |
Ref |
Expression |
1 |
|
ltso |
|- < Or RR |
2 |
1
|
a1i |
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> < Or RR ) |
3 |
|
lbcl |
|- ( ( 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 ) |
4 |
|
ssel |
|- ( S C_ RR -> ( ( iota_ x e. S A. y e. S x <_ y ) e. S -> ( iota_ x e. S A. y e. S x <_ y ) e. RR ) ) |
5 |
4
|
adantr |
|- ( ( 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 -> ( iota_ x e. S A. y e. S x <_ y ) e. RR ) ) |
6 |
3 5
|
mpd |
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> ( iota_ x e. S A. y e. S x <_ y ) e. RR ) |
7 |
6
|
adantr |
|- ( ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) /\ z e. S ) -> ( iota_ x e. S A. y e. S x <_ y ) e. RR ) |
8 |
|
ssel2 |
|- ( ( S C_ RR /\ z e. S ) -> z e. RR ) |
9 |
8
|
adantlr |
|- ( ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) /\ z e. S ) -> z e. RR ) |
10 |
|
lble |
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y /\ z e. S ) -> ( iota_ x e. S A. y e. S x <_ y ) <_ z ) |
11 |
10
|
3expa |
|- ( ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) /\ z e. S ) -> ( iota_ x e. S A. y e. S x <_ y ) <_ z ) |
12 |
7 9 11
|
lensymd |
|- ( ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) /\ z e. S ) -> -. z < ( iota_ x e. S A. y e. S x <_ y ) ) |
13 |
2 6 3 12
|
infmin |
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> inf ( S , RR , < ) = ( iota_ x e. S A. y e. S x <_ y ) ) |