Theorem cncfres

Description: A continuous function on complex numbers restricted to a subset. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 12-Sep-2015)

	Ref	Expression
Hypotheses	cncfres.1	$$⊢A\subseteq ℂ$$
	cncfres.2	$$⊢B\subseteq ℂ$$
	cncfres.3	$$⊢F=\left(x\in ℂ⟼C\right)$$
	cncfres.4	$$⊢G=\left(x\in A⟼C\right)$$
	cncfres.5	$$⊢x\in A\to C\in B$$
	cncfres.6	$$⊢F:ℂ\underset{cn}{⟶}ℂ$$
	cncfres.7	$$⊢J=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(A\times A\right)}\right)$$
	cncfres.8	$$⊢K=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(B\times B\right)}\right)$$
Assertion	cncfres	$$⊢G\in \left(J\mathrm{Cn}K\right)$$

Proof

Step	Hyp	Ref	Expression
1		cncfres.1	$$⊢A\subseteq ℂ$$
2		cncfres.2	$$⊢B\subseteq ℂ$$
3		cncfres.3	$$⊢F=\left(x\in ℂ⟼C\right)$$
4		cncfres.4	$$⊢G=\left(x\in A⟼C\right)$$
5		cncfres.5	$$⊢x\in A\to C\in B$$
6		cncfres.6	$$⊢F:ℂ\underset{cn}{⟶}ℂ$$
7		cncfres.7	$$⊢J=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(A\times A\right)}\right)$$
8		cncfres.8	$$⊢K=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(B\times B\right)}\right)$$
9	4 5	fmpti	$$⊢G:A⟶B$$
10		resmpt	$$⊢A\subseteq ℂ\to {\left(x\in ℂ⟼C\right)\upharpoonright }_A=\left(x\in A⟼C\right)$$
11	1 10	ax-mp	$$⊢{\left(x\in ℂ⟼C\right)\upharpoonright }_A=\left(x\in A⟼C\right)$$
12	4 11	eqtr4i	$$⊢G={\left(x\in ℂ⟼C\right)\upharpoonright }_A$$
13	3 6	eqeltrri	$$⊢\left(x\in ℂ⟼C\right):ℂ\underset{cn}{⟶}ℂ$$
14		rescncf	$$⊢A\subseteq ℂ\to \left(\left(x\in ℂ⟼C\right):ℂ\underset{cn}{⟶}ℂ\to \left({\left(x\in ℂ⟼C\right)\upharpoonright }_A\right):A\underset{cn}{⟶}ℂ\right)$$
15	1 13 14	mp2	$$⊢\left({\left(x\in ℂ⟼C\right)\upharpoonright }_A\right):A\underset{cn}{⟶}ℂ$$
16	12 15	eqeltri	$$⊢G:A\underset{cn}{⟶}ℂ$$
17		cncffvrn	$$⊢\left(B\subseteq ℂ\wedge G:A\underset{cn}{⟶}ℂ\right)\to \left(G:A\underset{cn}{⟶}B\leftrightarrow G:A⟶B\right)$$
18	2 16 17	mp2an	$$⊢G:A\underset{cn}{⟶}B\leftrightarrow G:A⟶B$$
19	9 18	mpbir	$$⊢G:A\underset{cn}{⟶}B$$
20		eqid	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(A\times A\right)}={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(A\times A\right)}$$
21		eqid	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(B\times B\right)}={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{\left(B\times B\right)}$$
22	20 21 7 8	cncfmet	$$⊢\left(A\subseteq ℂ\wedge B\subseteq ℂ\right)\to A\underset{cn}{⟶}B=J\mathrm{Cn}K$$
23	1 2 22	mp2an	$$⊢A\underset{cn}{⟶}B=J\mathrm{Cn}K$$
24	19 23	eleqtri	$$⊢G\in \left(J\mathrm{Cn}K\right)$$