Theorem cncfiooicclem1 37765

Description: A continuous function F on an open interval ( A (,) B ) can be extended to a continuous function G on the corresponding closed interval, if it has a finite right limit R in A and a finite left limit L in B. F can be complex valued. This lemma assumes A < B, the invoking theorem drops this assumption. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
cncfiooicclem1.x	|- F/ x ph
cncfiooicclem1.g	|- G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
cncfiooicclem1.a	|- ( ph -> A e. RR )
cncfiooicclem1.b	|- ( ph -> B e. RR )
cncfiooicclem1.altb	|- ( ph -> A < B )
cncfiooicclem1.f	|- ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
cncfiooicclem1.l	|- ( ph -> L e. ( F lim CC B ) )
cncfiooicclem1.r	|- ( ph -> R e. ( F lim CC A ) )

Assertion

Ref	Expression
cncfiooicclem1	|- ( ph -> G e. ( ( A [,] B ) -cn-> CC ) )

Distinct variable groups:   x, A   x, B   x, F   x, L   x, R

Allowed substitution hints:   ph( x)   G( x)

Proof of Theorem cncfiooicclem1

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cncfiooicclem1.x	. . . 4 |- F/ x ph
2		limccl 22823	. . . . . . 7 |- ( F lim CC A ) C_ CC
3		cncfiooicclem1.r	. . . . . . 7 |- ( ph -> R e. ( F lim CC A ) )
4	2, 3	sseldi 3429	. . . . . 6 |- ( ph -> R e. CC )
5	4	ad2antrr 731	. . . . 5 |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ x = A ) -> R e. CC )
6		limccl 22823	. . . . . . . 8 |- ( F lim CC B ) C_ CC
7		cncfiooicclem1.l	. . . . . . . 8 |- ( ph -> L e. ( F lim CC B ) )
8	6, 7	sseldi 3429	. . . . . . 7 |- ( ph -> L e. CC )
9	8	ad3antrrr 735	. . . . . 6 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ x = B ) -> L e. CC )
10		simplll 767	. . . . . . 7 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ph )
11		orel1 384	. . . . . . . . . . 11 |- ( -. x = A -> ( ( x = A \/ x = B ) -> x = B ) )
12	11	con3dimp 443	. . . . . . . . . 10 |- ( ( -. x = A /\ -. x = B ) -> -. ( x = A \/ x = B ) )
13		vex 3047	. . . . . . . . . . 11 |- x e. _V
14	13	elpr 3985	. . . . . . . . . 10 |- ( x e. { A , B } <-> ( x = A \/ x = B ) )
15	12, 14	sylnibr 307	. . . . . . . . 9 |- ( ( -. x = A /\ -. x = B ) -> -. x e. { A , B } )
16	15	adantll 719	. . . . . . . 8 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> -. x e. { A , B } )
17		simpllr 768	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> x e. ( A [,] B ) )
18		cncfiooicclem1.a	. . . . . . . . . . . . 13 |- ( ph -> A e. RR )
19	18	rexrd 9687	. . . . . . . . . . . 12 |- ( ph -> A e. RR* )
20	10, 19	syl 17	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> A e. RR* )
21		cncfiooicclem1.b	. . . . . . . . . . . . 13 |- ( ph -> B e. RR )
22	21	rexrd 9687	. . . . . . . . . . . 12 |- ( ph -> B e. RR* )
23	10, 22	syl 17	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> B e. RR* )
24		cncfiooicclem1.altb	. . . . . . . . . . . . 13 |- ( ph -> A < B )
25	18, 21, 24	ltled 9780	. . . . . . . . . . . 12 |- ( ph -> A <_ B )
26	10, 25	syl 17	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> A <_ B )
27		prunioo 11758	. . . . . . . . . . 11 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
28	20, 23, 26, 27	syl3anc 1267	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
29	17, 28	eleqtrrd 2531	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> x e. ( ( A (,) B ) u. { A , B } ) )
30		elun 3573	. . . . . . . . 9 |- ( x e. ( ( A (,) B ) u. { A , B } ) <-> ( x e. ( A (,) B ) \/ x e. { A , B } ) )
31	29, 30	sylib 200	. . . . . . . 8 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( x e. ( A (,) B ) \/ x e. { A , B } ) )
32		orel2 385	. . . . . . . 8 |- ( -. x e. { A , B } -> ( ( x e. ( A (,) B ) \/ x e. { A , B } ) -> x e. ( A (,) B ) ) )
33	16, 31, 32	sylc 62	. . . . . . 7 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> x e. ( A (,) B ) )
34		cncfiooicclem1.f	. . . . . . . . 9 |- ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
35		cncff 21918	. . . . . . . . 9 |- ( F e. ( ( A (,) B ) -cn-> CC ) -> F : ( A (,) B ) --> CC )
36	34, 35	syl 17	. . . . . . . 8 |- ( ph -> F : ( A (,) B ) --> CC )
37	36	ffvelrnda 6020	. . . . . . 7 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( F ` x ) e. CC )
38	10, 33, 37	syl2anc 666	. . . . . 6 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( F ` x ) e. CC )
39	9, 38	ifclda 3912	. . . . 5 |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> if ( x = B , L , ( F ` x ) ) e. CC )
40	5, 39	ifclda 3912	. . . 4 |- ( ( ph /\ x e. ( A [,] B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC )
41		cncfiooicclem1.g	. . . 4 |- G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
42	1, 40, 41	fmptdf 6046	. . 3 |- ( ph -> G : ( A [,] B ) --> CC )
43		elun 3573	. . . . . . 7 |- ( y e. ( ( A (,) B ) u. { A , B } ) <-> ( y e. ( A (,) B ) \/ y e. { A , B } ) )
44	19, 22, 25, 27	syl3anc 1267	. . . . . . . 8 |- ( ph -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
45	44	eleq2d 2513	. . . . . . 7 |- ( ph -> ( y e. ( ( A (,) B ) u. { A , B } ) <-> y e. ( A [,] B ) ) )
46	43, 45	syl5bbr 263	. . . . . 6 |- ( ph -> ( ( y e. ( A (,) B ) \/ y e. { A , B } ) <-> y e. ( A [,] B ) ) )
47	46	biimpar 488	. . . . 5 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( y e. ( A (,) B ) \/ y e. { A , B } ) )
48		ioossicc 11717	. . . . . . . . . . . . 13 |- ( A (,) B ) C_ ( A [,] B )
49		fssres 5747	. . . . . . . . . . . . 13 |- ( ( G : ( A [,] B ) --> CC /\ ( A (,) B ) C_ ( A [,] B ) ) -> ( G |` ( A (,) B ) ) : ( A (,) B ) --> CC )
50	42, 48, 49	sylancl 667	. . . . . . . . . . . 12 |- ( ph -> ( G |` ( A (,) B ) ) : ( A (,) B ) --> CC )
51	50	feqmptd 5916	. . . . . . . . . . 11 |- ( ph -> ( G |` ( A (,) B ) ) = ( y e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` y ) ) )
52		nfmpt1 4491	. . . . . . . . . . . . . . . 16 |- F/_ x ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
53	41, 52	nfcxfr 2589	. . . . . . . . . . . . . . 15 |- F/_ x G
54		nfcv 2591	. . . . . . . . . . . . . . 15 |- F/_ x ( A (,) B )
55	53, 54	nfres 5106	. . . . . . . . . . . . . 14 |- F/_ x ( G |` ( A (,) B ) )
56		nfcv 2591	. . . . . . . . . . . . . 14 |- F/_ x y
57	55, 56	nffv 5870	. . . . . . . . . . . . 13 |- F/_ x ( ( G |` ( A (,) B ) ) ` y )
58		nfcv 2591	. . . . . . . . . . . . . 14 |- F/_ y ( G |` ( A (,) B ) )
59		nfcv 2591	. . . . . . . . . . . . . 14 |- F/_ y x
60	58, 59	nffv 5870	. . . . . . . . . . . . 13 |- F/_ y ( ( G |` ( A (,) B ) ) ` x )
61		fveq2 5863	. . . . . . . . . . . . 13 |- ( y = x -> ( ( G |` ( A (,) B ) ) ` y ) = ( ( G |` ( A (,) B ) ) ` x ) )
62	57, 60, 61	cbvmpt 4493	. . . . . . . . . . . 12 |- ( y e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` y ) ) = ( x e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` x ) )
63	62	a1i 11	. . . . . . . . . . 11 |- ( ph -> ( y e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` y ) ) = ( x e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` x ) ) )
64		fvres 5877	. . . . . . . . . . . . . 14 |- ( x e. ( A (,) B ) -> ( ( G |` ( A (,) B ) ) ` x ) = ( G ` x ) )
65	64	adantl 468	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( G |` ( A (,) B ) ) ` x ) = ( G ` x ) )
66		simpr 463	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( A (,) B ) )
67	48, 66	sseldi 3429	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( A [,] B ) )
68	4	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( A (,) B ) ) -> R e. CC )
69	8	ad2antrr 731	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( A (,) B ) ) /\ x = B ) -> L e. CC )
70	37	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( A (,) B ) ) /\ -. x = B ) -> ( F ` x ) e. CC )
71	69, 70	ifclda 3912	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = B , L , ( F ` x ) ) e. CC )
72	68, 71	ifcld 3923	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC )
73	41	fvmpt2 5955	. . . . . . . . . . . . . 14 |- ( ( x e. ( A [,] B ) /\ if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC ) -> ( G ` x ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
74	67, 72, 73	syl2anc 666	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( G ` x ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
75		elioo4g 11692	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. ( A (,) B ) <-> ( ( A e. RR* /\ B e. RR* /\ x e. RR ) /\ ( A < x /\ x < B ) ) )
76	75	biimpi 198	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( A (,) B ) -> ( ( A e. RR* /\ B e. RR* /\ x e. RR ) /\ ( A < x /\ x < B ) ) )
77	76	simpld 461	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( A (,) B ) -> ( A e. RR* /\ B e. RR* /\ x e. RR ) )
78	77	simp1d 1019	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( A (,) B ) -> A e. RR* )
79		elioore 11663	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( A (,) B ) -> x e. RR )
80	79	rexrd 9687	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( A (,) B ) -> x e. RR* )
81		eliooord 11691	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( A (,) B ) -> ( A < x /\ x < B ) )
82	81	simpld 461	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( A (,) B ) -> A < x )
83		xrltne 11457	. . . . . . . . . . . . . . . . . 18 |- ( ( A e. RR* /\ x e. RR* /\ A < x ) -> x =/= A )
84	78, 80, 82, 83	syl3anc 1267	. . . . . . . . . . . . . . . . 17 |- ( x e. ( A (,) B ) -> x =/= A )
85	84	adantl 468	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( A (,) B ) ) -> x =/= A )
86	85	neneqd 2628	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( A (,) B ) ) -> -. x = A )
87	86	iffalsed 3891	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
88	81	simprd 465	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( A (,) B ) -> x < B )
89	79, 88	ltned 9768	. . . . . . . . . . . . . . . . 17 |- ( x e. ( A (,) B ) -> x =/= B )
90	89	neneqd 2628	. . . . . . . . . . . . . . . 16 |- ( x e. ( A (,) B ) -> -. x = B )
91	90	iffalsed 3891	. . . . . . . . . . . . . . 15 |- ( x e. ( A (,) B ) -> if ( x = B , L , ( F ` x ) ) = ( F ` x ) )
92	91	adantl 468	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = B , L , ( F ` x ) ) = ( F ` x ) )
93	87, 92	eqtrd 2484	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = ( F ` x ) )
94	65, 74, 93	3eqtrd 2488	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( G |` ( A (,) B ) ) ` x ) = ( F ` x ) )
95	1, 94	mpteq2da 4487	. . . . . . . . . . 11 |- ( ph -> ( x e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` x ) ) = ( x e. ( A (,) B ) |-> ( F ` x ) ) )
96	51, 63, 95	3eqtrd 2488	. . . . . . . . . 10 |- ( ph -> ( G |` ( A (,) B ) ) = ( x e. ( A (,) B ) |-> ( F ` x ) ) )
97	36	feqmptd 5916	. . . . . . . . . . 11 |- ( ph -> F = ( x e. ( A (,) B ) |-> ( F ` x ) ) )
98		ioosscn 37585	. . . . . . . . . . . . 13 |- ( A (,) B ) C_ CC
99	98	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( A (,) B ) C_ CC )
100		ssid 3450	. . . . . . . . . . . 12 |- CC C_ CC
101		eqid 2450	. . . . . . . . . . . . 13 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
102		eqid 2450	. . . . . . . . . . . . 13 |- ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) )
103	101	cnfldtop 21797	. . . . . . . . . . . . . . 15 |- ( TopOpen ` ℂfld ) e. Top
104		unicntop 37365	. . . . . . . . . . . . . . . 16 |- CC = U. ( TopOpen ` ℂfld )
105	104	restid 15325	. . . . . . . . . . . . . . 15 |- ( ( TopOpen ` ℂfld ) e. Top -> ( ( TopOpen ` ℂfld ) ↾t CC ) = ( TopOpen ` ℂfld ) )
106	103, 105	ax-mp 5	. . . . . . . . . . . . . 14 |- ( ( TopOpen ` ℂfld ) ↾t CC ) = ( TopOpen ` ℂfld )
107	106	eqcomi 2459	. . . . . . . . . . . . 13 |- ( TopOpen ` ℂfld ) = ( ( TopOpen ` ℂfld ) ↾t CC )
108	101, 102, 107	cncfcn 21934	. . . . . . . . . . . 12 |- ( ( ( A (,) B ) C_ CC /\ CC C_ CC ) -> ( ( A (,) B ) -cn-> CC ) = ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
109	99, 100, 108	sylancl 667	. . . . . . . . . . 11 |- ( ph -> ( ( A (,) B ) -cn-> CC ) = ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
110	34, 97, 109	3eltr3d 2542	. . . . . . . . . 10 |- ( ph -> ( x e. ( A (,) B ) |-> ( F ` x ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
111	96, 110	eqeltrd 2528	. . . . . . . . 9 |- ( ph -> ( G |` ( A (,) B ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
112	104	restuni 20171	. . . . . . . . . . 11 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ ( A (,) B ) C_ CC ) -> ( A (,) B ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) )
113	103, 98, 112	mp2an 677	. . . . . . . . . 10 |- ( A (,) B ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) )
114	113	cncnpi 20287	. . . . . . . . 9 |- ( ( ( G |` ( A (,) B ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) /\ y e. ( A (,) B ) ) -> ( G |` ( A (,) B ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
115	111, 114	sylan 474	. . . . . . . 8 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( G |` ( A (,) B ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
116	103	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( TopOpen ` ℂfld ) e. Top )
117	48	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( A (,) B ) C_ ( A [,] B ) )
118		ovex 6316	. . . . . . . . . . . . 13 |- ( A [,] B ) e. _V
119	118	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( A [,] B ) e. _V )
120		restabs 20174	. . . . . . . . . . . 12 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ ( A (,) B ) C_ ( A [,] B ) /\ ( A [,] B ) e. _V ) -> ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) )
121	116, 117, 119, 120	syl3anc 1267	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) )
122	121	eqcomd 2456	. . . . . . . . . 10 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) = ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) )
123	122	oveq1d 6303	. . . . . . . . 9 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) )
124	123	fveq1d 5865	. . . . . . . 8 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) = ( ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
125	115, 124	eleqtrd 2530	. . . . . . 7 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( G |` ( A (,) B ) ) e. ( ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
126		resttop 20169	. . . . . . . . . 10 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ ( A [,] B ) e. _V ) -> ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) e. Top )
127	103, 118, 126	mp2an 677	. . . . . . . . 9 |- ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) e. Top
128	127	a1i 11	. . . . . . . 8 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) e. Top )
129	48	a1i 11	. . . . . . . . . 10 |- ( ph -> ( A (,) B ) C_ ( A [,] B ) )
130	18, 21	iccssred 37596	. . . . . . . . . . . 12 |- ( ph -> ( A [,] B ) C_ RR )
131		ax-resscn 9593	. . . . . . . . . . . 12 |- RR C_ CC
132	130, 131	syl6ss 3443	. . . . . . . . . . 11 |- ( ph -> ( A [,] B ) C_ CC )
133	104	restuni 20171	. . . . . . . . . . 11 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ ( A [,] B ) C_ CC ) -> ( A [,] B ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
134	103, 132, 133	sylancr 668	. . . . . . . . . 10 |- ( ph -> ( A [,] B ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
135	129, 134	sseqtrd 3467	. . . . . . . . 9 |- ( ph -> ( A (,) B ) C_ U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
136	135	adantr 467	. . . . . . . 8 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( A (,) B ) C_ U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
137		retop 21775	. . . . . . . . . . . . . 14 |- ( topGen ` ran (,) ) e. Top
138	137	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( topGen ` ran (,) ) e. Top )
139		ioossre 11693	. . . . . . . . . . . . . . 15 |- ( A (,) B ) C_ RR
140		difss 3559	. . . . . . . . . . . . . . 15 |- ( RR \ ( A [,] B ) ) C_ RR
141	139, 140	unssi 3608	. . . . . . . . . . . . . 14 |- ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) C_ RR
142	141	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) C_ RR )
143		ssun1 3596	. . . . . . . . . . . . . 14 |- ( A (,) B ) C_ ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) )
144	143	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( A (,) B ) C_ ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) )
145		uniretop 21776	. . . . . . . . . . . . . 14 |- RR = U. ( topGen ` ran (,) )
146	145	ntrss 20063	. . . . . . . . . . . . 13 |- ( ( ( topGen ` ran (,) ) e. Top /\ ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) C_ RR /\ ( A (,) B ) C_ ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) C_ ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
147	138, 142, 144, 146	syl3anc 1267	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) C_ ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
148		simpr 463	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( A (,) B ) )
149		ioontr 37605	. . . . . . . . . . . . 13 |- ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B )
150	148, 149	syl6eleqr 2539	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) )
151	147, 150	sseldd 3432	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
152	48, 148	sseldi 3429	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( A [,] B ) )
153	151, 152	elind 3617	. . . . . . . . . 10 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) i^i ( A [,] B ) ) )
154	130	adantr 467	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( A [,] B ) C_ RR )
155		eqid 2450	. . . . . . . . . . . 12 |- ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) = ( ( topGen ` ran (,) ) ↾t ( A [,] B ) )
156	145, 155	restntr 20191	. . . . . . . . . . 11 |- ( ( ( topGen ` ran (,) ) e. Top /\ ( A [,] B ) C_ RR /\ ( A (,) B ) C_ ( A [,] B ) ) -> ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) = ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) i^i ( A [,] B ) ) )
157	138, 154, 117, 156	syl3anc 1267	. . . . . . . . . 10 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) = ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) i^i ( A [,] B ) ) )
158	153, 157	eleqtrrd 2531	. . . . . . . . 9 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) )
159	101	tgioo2 21814	. . . . . . . . . . . . . . 15 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
160	159	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR ) )
161	160	oveq1d 6303	. . . . . . . . . . . . 13 |- ( ph -> ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) = ( ( ( TopOpen ` ℂfld ) ↾t RR ) ↾t ( A [,] B ) ) )
162	103	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> ( TopOpen ` ℂfld ) e. Top )
163		reex 9627	. . . . . . . . . . . . . . 15 |- RR e. _V
164	163	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> RR e. _V )
165		restabs 20174	. . . . . . . . . . . . . 14 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ ( A [,] B ) C_ RR /\ RR e. _V ) -> ( ( ( TopOpen ` ℂfld ) ↾t RR ) ↾t ( A [,] B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
166	162, 130, 164, 165	syl3anc 1267	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( TopOpen ` ℂfld ) ↾t RR ) ↾t ( A [,] B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
167	161, 166	eqtrd 2484	. . . . . . . . . . . 12 |- ( ph -> ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
168	167	fveq2d 5867	. . . . . . . . . . 11 |- ( ph -> ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) = ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) )
169	168	fveq1d 5865	. . . . . . . . . 10 |- ( ph -> ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) = ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) )
170	169	adantr 467	. . . . . . . . 9 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) = ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) )
171	158, 170	eleqtrd 2530	. . . . . . . 8 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) )
172	134	feq2d 5713	. . . . . . . . . 10 |- ( ph -> ( G : ( A [,] B ) --> CC <-> G : U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) --> CC ) )
173	42, 172	mpbid 214	. . . . . . . . 9 |- ( ph -> G : U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) --> CC )
174	173	adantr 467	. . . . . . . 8 |- ( ( ph /\ y e. ( A (,) B ) ) -> G : U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) --> CC )
175		eqid 2450	. . . . . . . . 9 |- U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) )
176	175, 104	cnprest 20298	. . . . . . . 8 |- ( ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) e. Top /\ ( A (,) B ) C_ U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) /\ ( y e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) /\ G : U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) --> CC ) ) -> ( G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) <-> ( G |` ( A (,) B ) ) e. ( ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) ) )
177	128, 136, 171, 174, 176	syl22anc 1268	. . . . . . 7 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) <-> ( G |` ( A (,) B ) ) e. ( ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) ) )
178	125, 177	mpbird 236	. . . . . 6 |- ( ( ph /\ y e. ( A (,) B ) ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
179		elpri 3984	. . . . . . 7 |- ( y e. { A , B } -> ( y = A \/ y = B ) )
180		lbicc2 11745	. . . . . . . . . . . . . 14 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
181	19, 22, 25, 180	syl3anc 1267	. . . . . . . . . . . . 13 |- ( ph -> A e. ( A [,] B ) )
182		iftrue 3886	. . . . . . . . . . . . . 14 |- ( x = A -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = R )
183	182, 41	fvmptg 5944	. . . . . . . . . . . . 13 |- ( ( A e. ( A [,] B ) /\ R e. ( F lim CC A ) ) -> ( G ` A ) = R )
184	181, 3, 183	syl2anc 666	. . . . . . . . . . . 12 |- ( ph -> ( G ` A ) = R )
185	97	eqcomd 2456	. . . . . . . . . . . . . . . 16 |- ( ph -> ( x e. ( A (,) B ) |-> ( F ` x ) ) = F )
186	96, 185	eqtr2d 2485	. . . . . . . . . . . . . . 15 |- ( ph -> F = ( G |` ( A (,) B ) ) )
187	186	oveq1d 6303	. . . . . . . . . . . . . 14 |- ( ph -> ( F lim CC A ) = ( ( G |` ( A (,) B ) ) lim CC A ) )
188	3, 187	eleqtrd 2530	. . . . . . . . . . . . 13 |- ( ph -> R e. ( ( G |` ( A (,) B ) ) lim CC A ) )
189	18, 21, 24, 42	limciccioolb 37695	. . . . . . . . . . . . 13 |- ( ph -> ( ( G |` ( A (,) B ) ) lim CC A ) = ( G lim CC A ) )
190	188, 189	eleqtrd 2530	. . . . . . . . . . . 12 |- ( ph -> R e. ( G lim CC A ) )
191	184, 190	eqeltrd 2528	. . . . . . . . . . 11 |- ( ph -> ( G ` A ) e. ( G lim CC A ) )
192		eqid 2450	. . . . . . . . . . . . 13 |- ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) )
193	101, 192	cnplimc 22835	. . . . . . . . . . . 12 |- ( ( ( A [,] B ) C_ CC /\ A e. ( A [,] B ) ) -> ( G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) <-> ( G : ( A [,] B ) --> CC /\ ( G ` A ) e. ( G lim CC A ) ) ) )
194	132, 181, 193	syl2anc 666	. . . . . . . . . . 11 |- ( ph -> ( G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) <-> ( G : ( A [,] B ) --> CC /\ ( G ` A ) e. ( G lim CC A ) ) ) )
195	42, 191, 194	mpbir2and 932	. . . . . . . . . 10 |- ( ph -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) )
196	195	adantr 467	. . . . . . . . 9 |- ( ( ph /\ y = A ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) )
197		fveq2 5863	. . . . . . . . . . 11 |- ( y = A -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) )
198	197	eqcomd 2456	. . . . . . . . . 10 |- ( y = A -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
199	198	adantl 468	. . . . . . . . 9 |- ( ( ph /\ y = A ) -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
200	196, 199	eleqtrd 2530	. . . . . . . 8 |- ( ( ph /\ y = A ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
201	21	leidd 10177	. . . . . . . . . . . . . . 15 |- ( ph -> B <_ B )
202	18, 21, 21, 25, 201	eliccd 37595	. . . . . . . . . . . . . 14 |- ( ph -> B e. ( A [,] B ) )
203		eqid 2450	. . . . . . . . . . . . . . . . . 18 |- B = B
204	203	iftruei 3887	. . . . . . . . . . . . . . . . 17 |- if ( B = B , L , ( F ` B ) ) = L
205	204, 8	syl5eqel 2532	. . . . . . . . . . . . . . . 16 |- ( ph -> if ( B = B , L , ( F ` B ) ) e. CC )
206	4, 205	ifcld 3923	. . . . . . . . . . . . . . 15 |- ( ph -> if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) e. CC )
207	202, 206	jca 535	. . . . . . . . . . . . . 14 |- ( ph -> ( B e. ( A [,] B ) /\ if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) e. CC ) )
208		nfv 1760	. . . . . . . . . . . . . . . 16 |- F/ x ( B e. ( A [,] B ) /\ if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) e. CC )
209		nfcv 2591	. . . . . . . . . . . . . . . . . 18 |- F/_ x B
210	53, 209	nffv 5870	. . . . . . . . . . . . . . . . 17 |- F/_ x ( G ` B )
211	210	nfeq1 2604	. . . . . . . . . . . . . . . 16 |- F/ x ( G ` B ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) )
212	208, 211	nfim 2002	. . . . . . . . . . . . . . 15 |- F/ x ( ( B e. ( A [,] B ) /\ if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) e. CC ) -> ( G ` B ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
213		eleq1 2516	. . . . . . . . . . . . . . . . 17 |- ( x = B -> ( x e. ( A [,] B ) <-> B e. ( A [,] B ) ) )
214	182	adantl 468	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = B /\ x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = R )
215		eqtr2 2470	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x = B /\ x = A ) -> B = A )
216		iftrue 3886	. . . . . . . . . . . . . . . . . . . . . 22 |- ( B = A -> if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) = R )
217	216	eqcomd 2456	. . . . . . . . . . . . . . . . . . . . 21 |- ( B = A -> R = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
218	215, 217	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = B /\ x = A ) -> R = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
219	214, 218	eqtrd 2484	. . . . . . . . . . . . . . . . . . 19 |- ( ( x = B /\ x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
220		iffalse 3889	. . . . . . . . . . . . . . . . . . . . 21 |- ( -. x = A -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
221	220	adantl 468	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = B /\ -. x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
222		iftrue 3886	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = B -> if ( x = B , L , ( F ` x ) ) = L )
223	222	adantr 467	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = B /\ -. x = A ) -> if ( x = B , L , ( F ` x ) ) = L )
224		df-ne 2623	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x =/= A <-> -. x = A )
225		pm13.18 2704	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( x = B /\ x =/= A ) -> B =/= A )
226	224, 225	sylan2br 479	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( x = B /\ -. x = A ) -> B =/= A )
227	226	neneqd 2628	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( x = B /\ -. x = A ) -> -. B = A )
228	227	iffalsed 3891	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x = B /\ -. x = A ) -> if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) = if ( B = B , L , ( F ` B ) ) )
229	228, 204	syl6req 2501	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = B /\ -. x = A ) -> L = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
230	221, 223, 229	3eqtrd 2488	. . . . . . . . . . . . . . . . . . 19 |- ( ( x = B /\ -. x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
231	219, 230	pm2.61dan 799	. . . . . . . . . . . . . . . . . 18 |- ( x = B -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
232	231	eleq1d 2512	. . . . . . . . . . . . . . . . 17 |- ( x = B -> ( if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC <-> if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) e. CC ) )
233	213, 232	anbi12d 716	. . . . . . . . . . . . . . . 16 |- ( x = B -> ( ( x e. ( A [,] B ) /\ if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC ) <-> ( B e. ( A [,] B ) /\ if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) e. CC ) ) )
234		fveq2 5863	. . . . . . . . . . . . . . . . 17 |- ( x = B -> ( G ` x ) = ( G ` B ) )
235	234, 231	eqeq12d 2465	. . . . . . . . . . . . . . . 16 |- ( x = B -> ( ( G ` x ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) <-> ( G ` B ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) ) )
236	233, 235	imbi12d 322	. . . . . . . . . . . . . . 15 |- ( x = B -> ( ( ( x e. ( A [,] B ) /\ if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC ) -> ( G ` x ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) ) <-> ( ( B e. ( A [,] B ) /\ if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) e. CC ) -> ( G ` B ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) ) ) )
237	212, 236, 73	vtoclg1f 3105	. . . . . . . . . . . . . 14 |- ( B e. ( A [,] B ) -> ( ( B e. ( A [,] B ) /\ if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) e. CC ) -> ( G ` B ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) ) )
238	202, 207, 237	sylc 62	. . . . . . . . . . . . 13 |- ( ph -> ( G ` B ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
239	18, 24	gtned 9767	. . . . . . . . . . . . . . 15 |- ( ph -> B =/= A )
240	239	neneqd 2628	. . . . . . . . . . . . . 14 |- ( ph -> -. B = A )
241	240	iffalsed 3891	. . . . . . . . . . . . 13 |- ( ph -> if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) = if ( B = B , L , ( F ` B ) ) )
242	204	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> if ( B = B , L , ( F ` B ) ) = L )
243	238, 241, 242	3eqtrd 2488	. . . . . . . . . . . 12 |- ( ph -> ( G ` B ) = L )
244	186	oveq1d 6303	. . . . . . . . . . . . . 14 |- ( ph -> ( F lim CC B ) = ( ( G |` ( A (,) B ) ) lim CC B ) )
245	7, 244	eleqtrd 2530	. . . . . . . . . . . . 13 |- ( ph -> L e. ( ( G |` ( A (,) B ) ) lim CC B ) )
246	18, 21, 24, 42	limcicciooub 37711	. . . . . . . . . . . . 13 |- ( ph -> ( ( G |` ( A (,) B ) ) lim CC B ) = ( G lim CC B ) )
247	245, 246	eleqtrd 2530	. . . . . . . . . . . 12 |- ( ph -> L e. ( G lim CC B ) )
248	243, 247	eqeltrd 2528	. . . . . . . . . . 11 |- ( ph -> ( G ` B ) e. ( G lim CC B ) )
249	101, 192	cnplimc 22835	. . . . . . . . . . . 12 |- ( ( ( A [,] B ) C_ CC /\ B e. ( A [,] B ) ) -> ( G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` B ) <-> ( G : ( A [,] B ) --> CC /\ ( G ` B ) e. ( G lim CC B ) ) ) )
250	132, 202, 249	syl2anc 666	. . . . . . . . . . 11 |- ( ph -> ( G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` B ) <-> ( G : ( A [,] B ) --> CC /\ ( G ` B ) e. ( G lim CC B ) ) ) )
251	42, 248, 250	mpbir2and 932	. . . . . . . . . 10 |- ( ph -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` B ) )
252	251	adantr 467	. . . . . . . . 9 |- ( ( ph /\ y = B ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` B ) )
253		fveq2 5863	. . . . . . . . . . 11 |- ( y = B -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` B ) )
254	253	eqcomd 2456	. . . . . . . . . 10 |- ( y = B -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` B ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
255	254	adantl 468	. . . . . . . . 9 |- ( ( ph /\ y = B ) -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` B ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
256	252, 255	eleqtrd 2530	. . . . . . . 8 |- ( ( ph /\ y = B ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
257	200, 256	jaodan 793	. . . . . . 7 |- ( ( ph /\ ( y = A \/ y = B ) ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
258	179, 257	sylan2 477	. . . . . 6 |- ( ( ph /\ y e. { A , B } ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
259	178, 258	jaodan 793	. . . . 5 |- ( ( ph /\ ( y e. ( A (,) B ) \/ y e. { A , B } ) ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
260	47, 259	syldan 473	. . . 4 |- ( ( ph /\ y e. ( A [,] B ) ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
261	260	ralrimiva 2801	. . 3 |- ( ph -> A. y e. ( A [,] B ) G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
262	101	cnfldtopon 21796	. . . . 5 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
263		resttopon 20170	. . . . 5 |- ( ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) /\ ( A [,] B ) C_ CC ) -> ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) e. (TopOn ` ( A [,] B ) ) )
264	262, 132, 263	sylancr 668	. . . 4 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) e. (TopOn ` ( A [,] B ) ) )
265		cncnp 20289	. . . 4 |- ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) e. (TopOn ` ( A [,] B ) ) /\ ( TopOpen ` ℂfld ) e. (TopOn ` CC ) ) -> ( G e. ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) Cn ( TopOpen ` ℂfld ) ) <-> ( G : ( A [,] B ) --> CC /\ A. y e. ( A [,] B ) G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) ) ) )
266	264, 262, 265	sylancl 667	. . 3 |- ( ph -> ( G e. ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) Cn ( TopOpen ` ℂfld ) ) <-> ( G : ( A [,] B ) --> CC /\ A. y e. ( A [,] B ) G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) ) ) )
267	42, 261, 266	mpbir2and 932	. 2 |- ( ph -> G e. ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) Cn ( TopOpen ` ℂfld ) ) )
268	101, 192, 107	cncfcn 21934	. . 3 |- ( ( ( A [,] B ) C_ CC /\ CC C_ CC ) -> ( ( A [,] B ) -cn-> CC ) = ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) Cn ( TopOpen ` ℂfld ) ) )
269	132, 100, 268	sylancl 667	. 2 |- ( ph -> ( ( A [,] B ) -cn-> CC ) = ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) Cn ( TopOpen ` ℂfld ) ) )
270	267, 269	eleqtrrd 2531	1 |- ( ph -> G e. ( ( A [,] B ) -cn-> CC ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   \/ wo 370   /\ wa 371   /\ w3a 984   = wceq 1443   F/wnf 1666   e. wcel 1886   =/= wne 2621   A.wral 2736   _Vcvv 3044   \ cdif 3400   u. cun 3401   i^i cin 3402   C_ wss 3403   ifcif 3880   {cpr 3969   U.cuni 4197   class class class wbr 4401   |-> cmpt 4460   ran crn 4834   |` cres 4835   -->wf 5577   ` cfv 5581  (class class class)co 6288   CCcc 9534   RRcr 9535   RR*cxr 9671   < clt 9672   <_ cle 9673   (,)cioo 11632   [,]cicc 11635   ↾_t crest 15312   TopOpenctopn 15313   topGenctg 15329  ℂ_fldccnfld 18963   Topctop 19910  TopOnctopon 19911   intcnt 20025   Cn ccn 20233   CnP ccnp 20234   -cn->ccncf 21901   lim CC climc 22810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-cnex 9592  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-mulcom 9600  ax-addass 9601  ax-mulass 9602  ax-distr 9603  ax-i2m1 9604  ax-1ne0 9605  ax-1rid 9606  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609  ax-pre-lttri 9610  ax-pre-lttrn 9611  ax-pre-ltadd 9612  ax-pre-mulgt0 9613  ax-pre-sup 9614

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-int 4234  df-iun 4279  df-iin 4280  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-om 6690  df-1st 6790  df-2nd 6791  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-1o 7179  df-oadd 7183  df-er 7360  df-map 7471  df-pm 7472  df-en 7567  df-dom 7568  df-sdom 7569  df-fin 7570  df-fi 7922  df-sup 7953  df-inf 7954  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-sub 9859  df-neg 9860  df-div 10267  df-nn 10607  df-2 10665  df-3 10666  df-4 10667  df-5 10668  df-6 10669  df-7 10670  df-8 10671  df-9 10672  df-10 10673  df-n0 10867  df-z 10935  df-dec 11049  df-uz 11157  df-q 11262  df-rp 11300  df-xneg 11406  df-xadd 11407  df-xmul 11408  df-ioo 11636  df-ioc 11637  df-ico 11638  df-icc 11639  df-fz 11782  df-seq 12211  df-exp 12270  df-cj 13155  df-re 13156  df-im 13157  df-sqrt 13291  df-abs 13292  df-struct 15116  df-ndx 15117  df-slot 15118  df-base 15119  df-plusg 15196  df-mulr 15197  df-starv 15198  df-tset 15202  df-ple 15203  df-ds 15205  df-unif 15206  df-rest 15314  df-topn 15315  df-topgen 15335  df-psmet 18955  df-xmet 18956  df-met 18957  df-bl 18958  df-mopn 18959  df-cnfld 18964  df-top 19914  df-bases 19915  df-topon 19916  df-topsp 19917  df-cld 20027  df-ntr 20028  df-cls 20029  df-cn 20236  df-cnp 20237  df-xms 21328  df-ms 21329  df-cncf 21903  df-limc 22814

This theorem is referenced by:  cncfiooicc  37766