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 C_ CC
	cncfres.2	|- B C_ CC
	cncfres.3	|- F = ( x e. CC |-> C )
	cncfres.4	|- G = ( x e. A |-> C )
	cncfres.5	|- ( x e. A -> C e. B )
	cncfres.6	|- F e. ( CC -cn-> CC )
	cncfres.7	|- J = ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) )
	cncfres.8	|- K = ( MetOpen ` ( ( abs o. - ) |` ( B X. B ) ) )
Assertion	cncfres	|- G e. ( J Cn K )

Proof

Step	Hyp	Ref	Expression
1		cncfres.1	|- A C_ CC
2		cncfres.2	|- B C_ CC
3		cncfres.3	|- F = ( x e. CC |-> C )
4		cncfres.4	|- G = ( x e. A |-> C )
5		cncfres.5	|- ( x e. A -> C e. B )
6		cncfres.6	|- F e. ( CC -cn-> CC )
7		cncfres.7	|- J = ( MetOpen ` ( ( abs o. - ) |` ( A X. A ) ) )
8		cncfres.8	|- K = ( MetOpen ` ( ( abs o. - ) |` ( B X. B ) ) )
9	4 5	fmpti	|- G : A --> B
10		resmpt	|- ( A C_ CC -> ( ( x e. CC |-> C ) |` A ) = ( x e. A |-> C ) )
11	1 10	ax-mp	|- ( ( x e. CC |-> C ) |` A ) = ( x e. A |-> C )
12	4 11	eqtr4i	|- G = ( ( x e. CC |-> C ) |` A )
13	3 6	eqeltrri	|- ( x e. CC |-> C ) e. ( CC -cn-> CC )
14		rescncf	|- ( A C_ CC -> ( ( x e. CC |-> C ) e. ( CC -cn-> CC ) -> ( ( x e. CC |-> C ) |` A ) e. ( A -cn-> CC ) ) )
15	1 13 14	mp2	|- ( ( x e. CC |-> C ) |` A ) e. ( A -cn-> CC )
16	12 15	eqeltri	|- G e. ( A -cn-> CC )
17		cncffvrn	|- ( ( B C_ CC /\ G e. ( A -cn-> CC ) ) -> ( G e. ( A -cn-> B ) <-> G : A --> B ) )
18	2 16 17	mp2an	|- ( G e. ( A -cn-> B ) <-> G : A --> B )
19	9 18	mpbir	|- G e. ( A -cn-> B )
20		eqid	|- ( ( abs o. - ) |` ( A X. A ) ) = ( ( abs o. - ) |` ( A X. A ) )
21		eqid	|- ( ( abs o. - ) |` ( B X. B ) ) = ( ( abs o. - ) |` ( B X. B ) )
22	20 21 7 8	cncfmet	|- ( ( A C_ CC /\ B C_ CC ) -> ( A -cn-> B ) = ( J Cn K ) )
23	1 2 22	mp2an	|- ( A -cn-> B ) = ( J Cn K )
24	19 23	eleqtri	|- G e. ( J Cn K )