Theorem infcvgaux1i

Description: Auxiliary theorem for applications of supcvg . Hypothesis for several supremum theorems. (Contributed by NM, 8-Feb-2008)

	Ref	Expression
Hypotheses	infcvg.1	|- R = { x | E. y e. X x = -u A }
	infcvg.2	|- ( y e. X -> A e. RR )
	infcvg.3	|- Z e. X
	infcvg.4	|- E. z e. RR A. w e. R w <_ z
Assertion	infcvgaux1i	|- ( R C_ RR /\ R =/= (/) /\ E. z e. RR A. w e. R w <_ z )

Proof

Step	Hyp	Ref	Expression
1		infcvg.1	|- R = { x | E. y e. X x = -u A }
2		infcvg.2	|- ( y e. X -> A e. RR )
3		infcvg.3	|- Z e. X
4		infcvg.4	|- E. z e. RR A. w e. R w <_ z
5	2	renegcld	|- ( y e. X -> -u A e. RR )
6		eleq1	|- ( x = -u A -> ( x e. RR <-> -u A e. RR ) )
7	5 6	syl5ibrcom	|- ( y e. X -> ( x = -u A -> x e. RR ) )
8	7	rexlimiv	|- ( E. y e. X x = -u A -> x e. RR )
9	8	abssi	|- { x | E. y e. X x = -u A } C_ RR
10	1 9	eqsstri	|- R C_ RR
11		eqid	|- -u [_ Z / y ]_ A = -u [_ Z / y ]_ A
12	11	nfth	|- F/ y -u [_ Z / y ]_ A = -u [_ Z / y ]_ A
13		csbeq1a	|- ( y = Z -> A = [_ Z / y ]_ A )
14	13	negeqd	|- ( y = Z -> -u A = -u [_ Z / y ]_ A )
15	14	eqeq2d	|- ( y = Z -> ( -u [_ Z / y ]_ A = -u A <-> -u [_ Z / y ]_ A = -u [_ Z / y ]_ A ) )
16	12 15	rspce	|- ( ( Z e. X /\ -u [_ Z / y ]_ A = -u [_ Z / y ]_ A ) -> E. y e. X -u [_ Z / y ]_ A = -u A )
17	3 11 16	mp2an	|- E. y e. X -u [_ Z / y ]_ A = -u A
18		negex	|- -u [_ Z / y ]_ A e. _V
19		nfcsb1v	|- F/_ y [_ Z / y ]_ A
20	19	nfneg	|- F/_ y -u [_ Z / y ]_ A
21	20	nfeq2	|- F/ y x = -u [_ Z / y ]_ A
22		eqeq1	|- ( x = -u [_ Z / y ]_ A -> ( x = -u A <-> -u [_ Z / y ]_ A = -u A ) )
23	21 22	rexbid	|- ( x = -u [_ Z / y ]_ A -> ( E. y e. X x = -u A <-> E. y e. X -u [_ Z / y ]_ A = -u A ) )
24	18 23	elab	|- ( -u [_ Z / y ]_ A e. { x | E. y e. X x = -u A } <-> E. y e. X -u [_ Z / y ]_ A = -u A )
25	17 24	mpbir	|- -u [_ Z / y ]_ A e. { x | E. y e. X x = -u A }
26	25 1	eleqtrri	|- -u [_ Z / y ]_ A e. R
27	26	ne0ii	|- R =/= (/)
28	10 27 4	3pm3.2i	|- ( R C_ RR /\ R =/= (/) /\ E. z e. RR A. w e. R w <_ z )