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

Metamath Proof Explorer

Theorem xrinfmss2

Description: Any subset of extended reals has an infimum. (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Assertion xrinfmss2 
|- ( A C_ RR* -> E. x e. RR* ( A. y e. A -. x `' < y /\ A. y e. RR* ( y `' < x -> E. z e. A y `' < z ) ) )

Proof

Step Hyp Ref Expression
1 xrinfmss 
 |-  ( A C_ RR* -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) )
2 vex 
 |-  x e. _V
3 vex 
 |-  y e. _V
4 2 3 brcnv 
 |-  ( x `' < y <-> y < x )
5 4 notbii 
 |-  ( -. x `' < y <-> -. y < x )
6 5 ralbii 
 |-  ( A. y e. A -. x `' < y <-> A. y e. A -. y < x )
7 3 2 brcnv 
 |-  ( y `' < x <-> x < y )
8 vex 
 |-  z e. _V
9 3 8 brcnv 
 |-  ( y `' < z <-> z < y )
10 9 rexbii 
 |-  ( E. z e. A y `' < z <-> E. z e. A z < y )
11 7 10 imbi12i 
 |-  ( ( y `' < x -> E. z e. A y `' < z ) <-> ( x < y -> E. z e. A z < y ) )
12 11 ralbii 
 |-  ( A. y e. RR* ( y `' < x -> E. z e. A y `' < z ) <-> A. y e. RR* ( x < y -> E. z e. A z < y ) )
13 6 12 anbi12i 
 |-  ( ( A. y e. A -. x `' < y /\ A. y e. RR* ( y `' < x -> E. z e. A y `' < z ) ) <-> ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) )
14 13 rexbii 
 |-  ( E. x e. RR* ( A. y e. A -. x `' < y /\ A. y e. RR* ( y `' < x -> E. z e. A y `' < z ) ) <-> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) )
15 1 14 sylibr 
 |-  ( A C_ RR* -> E. x e. RR* ( A. y e. A -. x `' < y /\ A. y e. RR* ( y `' < x -> E. z e. A y `' < z ) ) )