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=\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$$
Assertion	infcvgaux1i	$$⊢\left(R\subseteq ℝ\wedge R\ne \varnothing \wedge \exists z\in ℝ\forall w\in Rw\le z\right)$$

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	2	renegcld	$$⊢y\in X\to -A\in ℝ$$
6		eleq1	$$⊢x=-A\to \left(x\in ℝ\leftrightarrow -A\in ℝ\right)$$
7	5 6	syl5ibrcom	$$⊢y\in X\to \left(x=-A\to x\in ℝ\right)$$
8	7	rexlimiv	$$⊢\exists y\in Xx=-A\to x\in ℝ$$
9	8	abssi	$$⊢\left\{x|\exists y\in Xx=-A\right\}\subseteq ℝ$$
10	1 9	eqsstri	$$⊢R\subseteq ℝ$$
11		eqid	$$⊢-⦋Z/y⦌A=-⦋Z/y⦌A$$
12	11	nfth	$$⊢Ⅎy-⦋Z/y⦌A=-⦋Z/y⦌A$$
13		csbeq1a	$$⊢y=Z\to A=⦋Z/y⦌A$$
14	13	negeqd	$$⊢y=Z\to -A=-⦋Z/y⦌A$$
15	14	eqeq2d	$$⊢y=Z\to \left(-⦋Z/y⦌A=-A\leftrightarrow -⦋Z/y⦌A=-⦋Z/y⦌A\right)$$
16	12 15	rspce	$$⊢\left(Z\in X\wedge -⦋Z/y⦌A=-⦋Z/y⦌A\right)\to \exists y\in X-⦋Z/y⦌A=-A$$
17	3 11 16	mp2an	$$⊢\exists y\in X-⦋Z/y⦌A=-A$$
18		negex	$$⊢-⦋Z/y⦌A\in \mathrm{V}$$
19		nfcsb1v	$$⊢\underset{\_}{Ⅎ}y⦋Z/y⦌A$$
20	19	nfneg	$$⊢\underset{\_}{Ⅎ}y\left(-⦋Z/y⦌A\right)$$
21	20	nfeq2	$$⊢Ⅎyx=-⦋Z/y⦌A$$
22		eqeq1	$$⊢x=-⦋Z/y⦌A\to \left(x=-A\leftrightarrow -⦋Z/y⦌A=-A\right)$$
23	21 22	rexbid	$$⊢x=-⦋Z/y⦌A\to \left(\exists y\in Xx=-A\leftrightarrow \exists y\in X-⦋Z/y⦌A=-A\right)$$
24	18 23	elab	$$⊢-⦋Z/y⦌A\in \left\{x|\exists y\in Xx=-A\right\}\leftrightarrow \exists y\in X-⦋Z/y⦌A=-A$$
25	17 24	mpbir	$$⊢-⦋Z/y⦌A\in \left\{x|\exists y\in Xx=-A\right\}$$
26	25 1	eleqtrri	$$⊢-⦋Z/y⦌A\in R$$
27	26	ne0ii	$$⊢R\ne \varnothing$$
28	10 27 4	3pm3.2i	$$⊢\left(R\subseteq ℝ\wedge R\ne \varnothing \wedge \exists z\in ℝ\forall w\in Rw\le z\right)$$