Theorem cncfi

Description: Defining property of a continuous function. (Contributed by Mario Carneiro, 30-Apr-2014) (Revised by Mario Carneiro, 25-Aug-2014)

	Ref	Expression
Assertion	cncfi	$$⊢\left(F:A\underset{cn}{⟶}B\wedge C\in A\wedge R\in {ℝ}^{+}\right)\to \exists z\in {ℝ}^{+}\forall w\in A\left(\left|w-C\right|<z\to \left|F\left(w\right)-F\left(C\right)\right|<R\right)$$

Proof

Step	Hyp	Ref	Expression
1		cncfrss	$$⊢F:A\underset{cn}{⟶}B\to A\subseteq ℂ$$
2		cncfrss2	$$⊢F:A\underset{cn}{⟶}B\to B\subseteq ℂ$$
3		elcncf2	$$⊢\left(A\subseteq ℂ\wedge B\subseteq ℂ\right)\to \left(F:A\underset{cn}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \forall x\in A\forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in A\left(\left|w-x\right|<z\to \left|F\left(w\right)-F\left(x\right)\right|<y\right)\right)\right)$$
4	1 2 3	syl2anc	$$⊢F:A\underset{cn}{⟶}B\to \left(F:A\underset{cn}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \forall x\in A\forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in A\left(\left|w-x\right|<z\to \left|F\left(w\right)-F\left(x\right)\right|<y\right)\right)\right)$$
5	4	ibi	$$⊢F:A\underset{cn}{⟶}B\to \left(F:A⟶B\wedge \forall x\in A\forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in A\left(\left|w-x\right|<z\to \left|F\left(w\right)-F\left(x\right)\right|<y\right)\right)$$
6	5	simprd	$$⊢F:A\underset{cn}{⟶}B\to \forall x\in A\forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in A\left(\left|w-x\right|<z\to \left|F\left(w\right)-F\left(x\right)\right|<y\right)$$
7		oveq2	$$⊢x=C\to w-x=w-C$$
8	7	fveq2d	$$⊢x=C\to \left|w-x\right|=\left|w-C\right|$$
9	8	breq1d	$$⊢x=C\to \left(\left|w-x\right|<z\leftrightarrow \left|w-C\right|<z\right)$$
10		fveq2	$$⊢x=C\to F\left(x\right)=F\left(C\right)$$
11	10	oveq2d	$$⊢x=C\to F\left(w\right)-F\left(x\right)=F\left(w\right)-F\left(C\right)$$
12	11	fveq2d	$$⊢x=C\to \left|F\left(w\right)-F\left(x\right)\right|=\left|F\left(w\right)-F\left(C\right)\right|$$
13	12	breq1d	$$⊢x=C\to \left(\left|F\left(w\right)-F\left(x\right)\right|<y\leftrightarrow \left|F\left(w\right)-F\left(C\right)\right|<y\right)$$
14	9 13	imbi12d	$$⊢x=C\to \left(\left(\left|w-x\right|<z\to \left|F\left(w\right)-F\left(x\right)\right|<y\right)\leftrightarrow \left(\left|w-C\right|<z\to \left|F\left(w\right)-F\left(C\right)\right|<y\right)\right)$$
15	14	rexralbidv	$$⊢x=C\to \left(\exists z\in {ℝ}^{+}\forall w\in A\left(\left|w-x\right|<z\to \left|F\left(w\right)-F\left(x\right)\right|<y\right)\leftrightarrow \exists z\in {ℝ}^{+}\forall w\in A\left(\left|w-C\right|<z\to \left|F\left(w\right)-F\left(C\right)\right|<y\right)\right)$$
16		breq2	$$⊢y=R\to \left(\left|F\left(w\right)-F\left(C\right)\right|<y\leftrightarrow \left|F\left(w\right)-F\left(C\right)\right|<R\right)$$
17	16	imbi2d	$$⊢y=R\to \left(\left(\left|w-C\right|<z\to \left|F\left(w\right)-F\left(C\right)\right|<y\right)\leftrightarrow \left(\left|w-C\right|<z\to \left|F\left(w\right)-F\left(C\right)\right|<R\right)\right)$$
18	17	rexralbidv	$$⊢y=R\to \left(\exists z\in {ℝ}^{+}\forall w\in A\left(\left|w-C\right|<z\to \left|F\left(w\right)-F\left(C\right)\right|<y\right)\leftrightarrow \exists z\in {ℝ}^{+}\forall w\in A\left(\left|w-C\right|<z\to \left|F\left(w\right)-F\left(C\right)\right|<R\right)\right)$$
19	15 18	rspc2v	$$⊢\left(C\in A\wedge R\in {ℝ}^{+}\right)\to \left(\forall x\in A\forall y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall w\in A\left(\left|w-x\right|<z\to \left|F\left(w\right)-F\left(x\right)\right|<y\right)\to \exists z\in {ℝ}^{+}\forall w\in A\left(\left|w-C\right|<z\to \left|F\left(w\right)-F\left(C\right)\right|<R\right)\right)$$
20	6 19	mpan9	$$⊢\left(F:A\underset{cn}{⟶}B\wedge \left(C\in A\wedge R\in {ℝ}^{+}\right)\right)\to \exists z\in {ℝ}^{+}\forall w\in A\left(\left|w-C\right|<z\to \left|F\left(w\right)-F\left(C\right)\right|<R\right)$$
21	20	3impb	$$⊢\left(F:A\underset{cn}{⟶}B\wedge C\in A\wedge R\in {ℝ}^{+}\right)\to \exists z\in {ℝ}^{+}\forall w\in A\left(\left|w-C\right|<z\to \left|F\left(w\right)-F\left(C\right)\right|<R\right)$$