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

Metamath Proof Explorer

Theorem supsr

Proof