Theorem infcvgaux2i

Description: Auxiliary theorem for applications of supcvg . (Contributed by NM, 4-Mar-2008)

	Ref	Expression
Hypotheses	infcvg.1	$$⊢R=\left\{x|\exists y\in Xx=-A\right\}$$
	infcvg.2	$$⊢y\in X\to A\in ℝ$$
	infcvg.3	$$⊢Z\in X$$
	infcvg.4	$$⊢\exists z\in ℝ\forall w\in Rw\le z$$
	infcvg.5a	$$⊢S=-sup\left(R,ℝ,<\right)$$
	infcvg.13	$$⊢y=C\to A=B$$
Assertion	infcvgaux2i	$$⊢C\in X\to S\le B$$

Proof

Step	Hyp	Ref	Expression
1		infcvg.1	$$⊢R=\left\{x|\exists y\in Xx=-A\right\}$$
2		infcvg.2	$$⊢y\in X\to A\in ℝ$$
3		infcvg.3	$$⊢Z\in X$$
4		infcvg.4	$$⊢\exists z\in ℝ\forall w\in Rw\le z$$
5		infcvg.5a	$$⊢S=-sup\left(R,ℝ,<\right)$$
6		infcvg.13	$$⊢y=C\to A=B$$
7		eqid	$$⊢-B=-B$$
8	6	negeqd	$$⊢y=C\to -A=-B$$
9	8	rspceeqv	$$⊢\left(C\in X\wedge -B=-B\right)\to \exists y\in X-B=-A$$
10	7 9	mpan2	$$⊢C\in X\to \exists y\in X-B=-A$$
11		negex	$$⊢-B\in \mathrm{V}$$
12		eqeq1	$$⊢x=-B\to \left(x=-A\leftrightarrow -B=-A\right)$$
13	12	rexbidv	$$⊢x=-B\to \left(\exists y\in Xx=-A\leftrightarrow \exists y\in X-B=-A\right)$$
14	11 13 1	elab2	$$⊢-B\in R\leftrightarrow \exists y\in X-B=-A$$
15	10 14	sylibr	$$⊢C\in X\to -B\in R$$
16	1 2 3 4	infcvgaux1i	$$⊢\left(R\subseteq ℝ\wedge R\ne \varnothing \wedge \exists z\in ℝ\forall w\in Rw\le z\right)$$
17	16	suprubii	$$⊢-B\in R\to -B\le sup\left(R,ℝ,<\right)$$
18	15 17	syl	$$⊢C\in X\to -B\le sup\left(R,ℝ,<\right)$$
19	6	eleq1d	$$⊢y=C\to \left(A\in ℝ\leftrightarrow B\in ℝ\right)$$
20	19 2	vtoclga	$$⊢C\in X\to B\in ℝ$$
21	16	suprclii	$$⊢sup\left(R,ℝ,<\right)\in ℝ$$
22		lenegcon1	$$⊢\left(B\in ℝ\wedge sup\left(R,ℝ,<\right)\in ℝ\right)\to \left(-B\le sup\left(R,ℝ,<\right)\leftrightarrow -sup\left(R,ℝ,<\right)\le B\right)$$
23	20 21 22	sylancl	$$⊢C\in X\to \left(-B\le sup\left(R,ℝ,<\right)\leftrightarrow -sup\left(R,ℝ,<\right)\le B\right)$$
24	18 23	mpbid	$$⊢C\in X\to -sup\left(R,ℝ,<\right)\le B$$
25	5 24	eqbrtrid	$$⊢C\in X\to S\le B$$