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 ) ) )