Theorem supsr

Description: A nonempty, bounded set of signed reals has a supremum. (Contributed by NM, 21-May-1996) (Revised by Mario Carneiro, 15-Jun-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	supsr	|- ( ( A =/= (/) /\ E. x e. R. A. y e. A y E. x e. R. ( A. y e. A -. x E. z e. A y

Proof

Step	Hyp	Ref	Expression
1		n0	|- ( A =/= (/) <-> E. u u e. A )
2		ltrelsr	|-
3	2	brel	|- ( y ( y e. R. /\ x e. R. ) )
4	3	simpld	|- ( y y e. R. )
5	4	ralimi	|- ( A. y e. A y A. y e. A y e. R. )
6		dfss3	|- ( A C_ R. <-> A. y e. A y e. R. )
7	5 6	sylibr	|- ( A. y e. A y A C_ R. )
8	7	sseld	|- ( A. y e. A y ( u e. A -> u e. R. ) )
9	8	rexlimivw	|- ( E. x e. R. A. y e. A y ( u e. A -> u e. R. ) )
10	9	impcom	|- ( ( u e. A /\ E. x e. R. A. y e. A y u e. R. )
11		eleq1	|- ( u = if ( u e. R. , u , 1R ) -> ( u e. A <-> if ( u e. R. , u , 1R ) e. A ) )
12	11	anbi1d	|- ( u = if ( u e. R. , u , 1R ) -> ( ( u e. A /\ E. x e. R. A. y e. A y ( if ( u e. R. , u , 1R ) e. A /\ E. x e. R. A. y e. A y
13	12	imbi1d	|- ( u = if ( u e. R. , u , 1R ) -> ( ( ( u e. A /\ E. x e. R. A. y e. A y E. x e. R. ( A. y e. A -. x E. z e. A y ( ( if ( u e. R. , u , 1R ) e. A /\ E. x e. R. A. y e. A y E. x e. R. ( A. y e. A -. x E. z e. A y
14		opeq1	|- ( v = w -> <. v , 1P >. = <. w , 1P >. )
15	14	eceq1d	|- ( v = w -> [ <. v , 1P >. ] ~R = [ <. w , 1P >. ] ~R )
16	15	oveq2d	|- ( v = w -> ( if ( u e. R. , u , 1R ) +R [ <. v , 1P >. ] ~R ) = ( if ( u e. R. , u , 1R ) +R [ <. w , 1P >. ] ~R ) )
17	16	eleq1d	|- ( v = w -> ( ( if ( u e. R. , u , 1R ) +R [ <. v , 1P >. ] ~R ) e. A <-> ( if ( u e. R. , u , 1R ) +R [ <. w , 1P >. ] ~R ) e. A ) )
18	17	cbvabv	|- { v | ( if ( u e. R. , u , 1R ) +R [ <. v , 1P >. ] ~R ) e. A } = { w | ( if ( u e. R. , u , 1R ) +R [ <. w , 1P >. ] ~R ) e. A }
19		1sr	|- 1R e. R.
20	19	elimel	|- if ( u e. R. , u , 1R ) e. R.
21	18 20	supsrlem	|- ( ( if ( u e. R. , u , 1R ) e. A /\ E. x e. R. A. y e. A y E. x e. R. ( A. y e. A -. x E. z e. A y
22	13 21	dedth	|- ( u e. R. -> ( ( u e. A /\ E. x e. R. A. y e. A y E. x e. R. ( A. y e. A -. x E. z e. A y
23	10 22	mpcom	|- ( ( u e. A /\ E. x e. R. A. y e. A y E. x e. R. ( A. y e. A -. x E. z e. A y
24	23	ex	|- ( u e. A -> ( E. x e. R. A. y e. A y E. x e. R. ( A. y e. A -. x E. z e. A y
25	24	exlimiv	|- ( E. u u e. A -> ( E. x e. R. A. y e. A y E. x e. R. ( A. y e. A -. x E. z e. A y
26	1 25	sylbi	|- ( A =/= (/) -> ( E. x e. R. A. y e. A y E. x e. R. ( A. y e. A -. x E. z e. A y
27	26	imp	|- ( ( A =/= (/) /\ E. x e. R. A. y e. A y E. x e. R. ( A. y e. A -. x E. z e. A y