Theorem cncfiooicclem1 37868

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 22909	. . . . . . 7 |- ( F lim CC A ) C_ CC
3		cncfiooicclem1.r	. . . . . . 7 |- ( ph -> R e. ( F lim CC A ) )
4	2, 3	sseldi 3416	. . . . . 6 |- ( ph -> R e. CC )
5	4	ad2antrr 740	. . . . 5 |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ x = A ) -> R e. CC )
6		limccl 22909	. . . . . . . 8 |- ( F lim CC B ) C_ CC
7		cncfiooicclem1.l	. . . . . . . 8 |- ( ph -> L e. ( F lim CC B ) )
8	6, 7	sseldi 3416	. . . . . . 7 |- ( ph -> L e. CC )
9	8	ad3antrrr 744	. . . . . 6 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ x = B ) -> L e. CC )
10		simplll 776	. . . . . . 7 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ph )
11		orel1 389	. . . . . . . . . . 11 |- ( -. x = A -> ( ( x = A \/ x = B ) -> x = B ) )
12	11	con3dimp 448	. . . . . . . . . 10 |- ( ( -. x = A /\ -. x = B ) -> -. ( x = A \/ x = B ) )
13		vex 3034	. . . . . . . . . . 11 |- x e. _V
14	13	elpr 3977	. . . . . . . . . 10 |- ( x e. { A , B } <-> ( x = A \/ x = B ) )
15	12, 14	sylnibr 312	. . . . . . . . 9 |- ( ( -. x = A /\ -. x = B ) -> -. x e. { A , B } )
16	15	adantll 728	. . . . . . . 8 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> -. x e. { A , B } )
17		simpllr 777	. . . . . . . . . 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 9708	. . . . . . . . . . . 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 9708	. . . . . . . . . . . 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 9800	. . . . . . . . . . . 12 |- ( ph -> A <_ B )
26	10, 25	syl 17	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> A <_ B )
27		prunioo 11787	. . . . . . . . . . 11 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
28	20, 23, 26, 27	syl3anc 1292	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
29	17, 28	eleqtrrd 2552	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> x e. ( ( A (,) B ) u. { A , B } ) )
30		elun 3565	. . . . . . . . 9 |- ( x e. ( ( A (,) B ) u. { A , B } ) <-> ( x e. ( A (,) B ) \/ x e. { A , B } ) )
31	29, 30	sylib 201	. . . . . . . 8 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( x e. ( A (,) B ) \/ x e. { A , B } ) )
32		orel2 390	. . . . . . . 8 |- ( -. x e. { A , B } -> ( ( x e. ( A (,) B ) \/ x e. { A , B } ) -> x e. ( A (,) B ) ) )
33	16, 31, 32	sylc 61	. . . . . . 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 22003	. . . . . . . . 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 6037	. . . . . . 7 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( F ` x ) e. CC )
38	10, 33, 37	syl2anc 673	. . . . . 6 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( F ` x ) e. CC )
39	9, 38	ifclda 3904	. . . . 5 |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> if ( x = B , L , ( F ` x ) ) e. CC )
40	5, 39	ifclda 3904	. . . 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 6063	. . 3 |- ( ph -> G : ( A [,] B ) --> CC )
43		elun 3565	. . . . . . 7 |- ( y e. ( ( A (,) B ) u. { A , B } ) <-> ( y e. ( A (,) B ) \/ y e. { A , B } ) )
44	19, 22, 25, 27	syl3anc 1292	. . . . . . . 8 |- ( ph -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
45	44	eleq2d 2534	. . . . . . 7 |- ( ph -> ( y e. ( ( A (,) B ) u. { A , B } ) <-> y e. ( A [,] B ) ) )
46	43, 45	syl5bbr 267	. . . . . 6 |- ( ph -> ( ( y e. ( A (,) B ) \/ y e. { A , B } ) <-> y e. ( A [,] B ) ) )
47	46	biimpar 493	. . . . 5 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( y e. ( A (,) B ) \/ y e. { A , B } ) )
48		ioossicc 11745	. . . . . . . . . . . . 13 |- ( A (,) B ) C_ ( A [,] B )
49		fssres 5761	. . . . . . . . . . . . 13 |- ( ( G : ( A [,] B ) --> CC /\ ( A (,) B ) C_ ( A [,] B ) ) -> ( G |` ( A (,) B ) ) : ( A (,) B ) --> CC )
50	42, 48, 49	sylancl 675	. . . . . . . . . . . 12 |- ( ph -> ( G |` ( A (,) B ) ) : ( A (,) B ) --> CC )
51	50	feqmptd 5932	. . . . . . . . . . 11 |- ( ph -> ( G |` ( A (,) B ) ) = ( y e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` y ) ) )
52		nfmpt1 4485	. . . . . . . . . . . . . . . 16 |- F/_ x ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
53	41, 52	nfcxfr 2610	. . . . . . . . . . . . . . 15 |- F/_ x G
54		nfcv 2612	. . . . . . . . . . . . . . 15 |- F/_ x ( A (,) B )
55	53, 54	nfres 5113	. . . . . . . . . . . . . 14 |- F/_ x ( G |` ( A (,) B ) )
56		nfcv 2612	. . . . . . . . . . . . . 14 |- F/_ x y
57	55, 56	nffv 5886	. . . . . . . . . . . . 13 |- F/_ x ( ( G |` ( A (,) B ) ) ` y )
58		nfcv 2612	. . . . . . . . . . . . . 14 |- F/_ y ( G |` ( A (,) B ) )
59		nfcv 2612	. . . . . . . . . . . . . 14 |- F/_ y x
60	58, 59	nffv 5886	. . . . . . . . . . . . 13 |- F/_ y ( ( G |` ( A (,) B ) ) ` x )
61		fveq2 5879	. . . . . . . . . . . . 13 |- ( y = x -> ( ( G |` ( A (,) B ) ) ` y ) = ( ( G |` ( A (,) B ) ) ` x ) )
62	57, 60, 61	cbvmpt 4487	. . . . . . . . . . . 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 5893	. . . . . . . . . . . . . 14 |- ( x e. ( A (,) B ) -> ( ( G |` ( A (,) B ) ) ` x ) = ( G ` x ) )
65	64	adantl 473	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( G |` ( A (,) B ) ) ` x ) = ( G ` x ) )
66		simpr 468	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( A (,) B ) )
67	48, 66	sseldi 3416	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( A [,] B ) )
68	4	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( A (,) B ) ) -> R e. CC )
69	8	ad2antrr 740	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( A (,) B ) ) /\ x = B ) -> L e. CC )
70	37	adantr 472	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( A (,) B ) ) /\ -. x = B ) -> ( F ` x ) e. CC )
71	69, 70	ifclda 3904	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = B , L , ( F ` x ) ) e. CC )
72	68, 71	ifcld 3915	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC )
73	41	fvmpt2 5972	. . . . . . . . . . . . . 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 673	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( G ` x ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
75		elioo4g 11720	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. ( A (,) B ) <-> ( ( A e. RR* /\ B e. RR* /\ x e. RR ) /\ ( A < x /\ x < B ) ) )
76	75	biimpi 199	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( A (,) B ) -> ( ( A e. RR* /\ B e. RR* /\ x e. RR ) /\ ( A < x /\ x < B ) ) )
77	76	simpld 466	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( A (,) B ) -> ( A e. RR* /\ B e. RR* /\ x e. RR ) )
78	77	simp1d 1042	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( A (,) B ) -> A e. RR* )
79		elioore 11691	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( A (,) B ) -> x e. RR )
80	79	rexrd 9708	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( A (,) B ) -> x e. RR* )
81		eliooord 11719	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( A (,) B ) -> ( A < x /\ x < B ) )
82	81	simpld 466	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( A (,) B ) -> A < x )
83		xrltne 11483	. . . . . . . . . . . . . . . . . 18 |- ( ( A e. RR* /\ x e. RR* /\ A < x ) -> x =/= A )
84	78, 80, 82, 83	syl3anc 1292	. . . . . . . . . . . . . . . . 17 |- ( x e. ( A (,) B ) -> x =/= A )
85	84	adantl 473	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( A (,) B ) ) -> x =/= A )
86	85	neneqd 2648	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( A (,) B ) ) -> -. x = A )
87	86	iffalsed 3883	. . . . . . . . . . . . . 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 470	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( A (,) B ) -> x < B )
89	79, 88	ltned 9788	. . . . . . . . . . . . . . . . 17 |- ( x e. ( A (,) B ) -> x =/= B )
90	89	neneqd 2648	. . . . . . . . . . . . . . . 16 |- ( x e. ( A (,) B ) -> -. x = B )
91	90	iffalsed 3883	. . . . . . . . . . . . . . 15 |- ( x e. ( A (,) B ) -> if ( x = B , L , ( F ` x ) ) = ( F ` x ) )
92	91	adantl 473	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = B , L , ( F ` x ) ) = ( F ` x ) )
93	87, 92	eqtrd 2505	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = ( F ` x ) )
94	65, 74, 93	3eqtrd 2509	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( G |` ( A (,) B ) ) ` x ) = ( F ` x ) )
95	1, 94	mpteq2da 4481	. . . . . . . . . . 11 |- ( ph -> ( x e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` x ) ) = ( x e. ( A (,) B ) |-> ( F ` x ) ) )
96	51, 63, 95	3eqtrd 2509	. . . . . . . . . 10 |- ( ph -> ( G |` ( A (,) B ) ) = ( x e. ( A (,) B ) |-> ( F ` x ) ) )
97	36	feqmptd 5932	. . . . . . . . . . 11 |- ( ph -> F = ( x e. ( A (,) B ) |-> ( F ` x ) ) )
98		ioosscn 37687	. . . . . . . . . . . . 13 |- ( A (,) B ) C_ CC
99	98	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( A (,) B ) C_ CC )
100		ssid 3437	. . . . . . . . . . . 12 |- CC C_ CC
101		eqid 2471	. . . . . . . . . . . . 13 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
102		eqid 2471	. . . . . . . . . . . . 13 |- ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) )
103	101	cnfldtop 21882	. . . . . . . . . . . . . . 15 |- ( TopOpen ` ℂfld ) e. Top
104		unicntop 37433	. . . . . . . . . . . . . . . 16 |- CC = U. ( TopOpen ` ℂfld )
105	104	restid 15410	. . . . . . . . . . . . . . 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 2480	. . . . . . . . . . . . 13 |- ( TopOpen ` ℂfld ) = ( ( TopOpen ` ℂfld ) ↾t CC )
108	101, 102, 107	cncfcn 22019	. . . . . . . . . . . 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 675	. . . . . . . . . . 11 |- ( ph -> ( ( A (,) B ) -cn-> CC ) = ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
110	34, 97, 109	3eltr3d 2563	. . . . . . . . . 10 |- ( ph -> ( x e. ( A (,) B ) |-> ( F ` x ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
111	96, 110	eqeltrd 2549	. . . . . . . . 9 |- ( ph -> ( G |` ( A (,) B ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
112	104	restuni 20255	. . . . . . . . . . 11 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ ( A (,) B ) C_ CC ) -> ( A (,) B ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) )
113	103, 98, 112	mp2an 686	. . . . . . . . . 10 |- ( A (,) B ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) )
114	113	cncnpi 20371	. . . . . . . . 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 479	. . . . . . . 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 6336	. . . . . . . . . . . . 13 |- ( A [,] B ) e. _V
119	118	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( A [,] B ) e. _V )
120		restabs 20258	. . . . . . . . . . . 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 1292	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) )
122	121	eqcomd 2477	. . . . . . . . . 10 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) = ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) )
123	122	oveq1d 6323	. . . . . . . . 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 5881	. . . . . . . 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 2551	. . . . . . 7 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( G |` ( A (,) B ) ) e. ( ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
126		resttop 20253	. . . . . . . . . 10 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ ( A [,] B ) e. _V ) -> ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) e. Top )
127	103, 118, 126	mp2an 686	. . . . . . . . 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 37698	. . . . . . . . . . . 12 |- ( ph -> ( A [,] B ) C_ RR )
131		ax-resscn 9614	. . . . . . . . . . . 12 |- RR C_ CC
132	130, 131	syl6ss 3430	. . . . . . . . . . 11 |- ( ph -> ( A [,] B ) C_ CC )
133	104	restuni 20255	. . . . . . . . . . 11 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ ( A [,] B ) C_ CC ) -> ( A [,] B ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
134	103, 132, 133	sylancr 676	. . . . . . . . . 10 |- ( ph -> ( A [,] B ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
135	129, 134	sseqtrd 3454	. . . . . . . . 9 |- ( ph -> ( A (,) B ) C_ U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
136	135	adantr 472	. . . . . . . 8 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( A (,) B ) C_ U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
137		retop 21860	. . . . . . . . . . . . . 14 |- ( topGen ` ran (,) ) e. Top
138	137	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( topGen ` ran (,) ) e. Top )
139		ioossre 11721	. . . . . . . . . . . . . . 15 |- ( A (,) B ) C_ RR
140		difss 3549	. . . . . . . . . . . . . . 15 |- ( RR \ ( A [,] B ) ) C_ RR
141	139, 140	unssi 3600	. . . . . . . . . . . . . 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 3588	. . . . . . . . . . . . . 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 21861	. . . . . . . . . . . . . 14 |- RR = U. ( topGen ` ran (,) )
146	145	ntrss 20147	. . . . . . . . . . . . 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 1292	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) C_ ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
148		simpr 468	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( A (,) B ) )
149		ioontr 37707	. . . . . . . . . . . . 13 |- ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B )
150	148, 149	syl6eleqr 2560	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) )
151	147, 150	sseldd 3419	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
152	48, 148	sseldi 3416	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( A [,] B ) )
153	151, 152	elind 3609	. . . . . . . . . 10 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) i^i ( A [,] B ) ) )
154	130	adantr 472	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( A [,] B ) C_ RR )
155		eqid 2471	. . . . . . . . . . . 12 |- ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) = ( ( topGen ` ran (,) ) ↾t ( A [,] B ) )
156	145, 155	restntr 20275	. . . . . . . . . . 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 1292	. . . . . . . . . 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 2552	. . . . . . . . 9 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) )
159	101	tgioo2 21899	. . . . . . . . . . . . . . 15 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
160	159	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR ) )
161	160	oveq1d 6323	. . . . . . . . . . . . 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 9648	. . . . . . . . . . . . . . 15 |- RR e. _V
164	163	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> RR e. _V )
165		restabs 20258	. . . . . . . . . . . . . 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 1292	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( TopOpen ` ℂfld ) ↾t RR ) ↾t ( A [,] B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
167	161, 166	eqtrd 2505	. . . . . . . . . . . 12 |- ( ph -> ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
168	167	fveq2d 5883	. . . . . . . . . . 11 |- ( ph -> ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) = ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) )
169	168	fveq1d 5881	. . . . . . . . . 10 |- ( ph -> ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) = ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) )
170	169	adantr 472	. . . . . . . . 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 2551	. . . . . . . 8 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) )
172	134	feq2d 5725	. . . . . . . . . 10 |- ( ph -> ( G : ( A [,] B ) --> CC <-> G : U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) --> CC ) )
173	42, 172	mpbid 215	. . . . . . . . 9 |- ( ph -> G : U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) --> CC )
174	173	adantr 472	. . . . . . . 8 |- ( ( ph /\ y e. ( A (,) B ) ) -> G : U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) --> CC )
175		eqid 2471	. . . . . . . . 9 |- U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) )
176	175, 104	cnprest 20382	. . . . . . . 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 1293	. . . . . . 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 240	. . . . . 6 |- ( ( ph /\ y e. ( A (,) B ) ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
179		elpri 3976	. . . . . . 7 |- ( y e. { A , B } -> ( y = A \/ y = B ) )
180		lbicc2 11774	. . . . . . . . . . . . . 14 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
181	19, 22, 25, 180	syl3anc 1292	. . . . . . . . . . . . 13 |- ( ph -> A e. ( A [,] B ) )
182		iftrue 3878	. . . . . . . . . . . . . 14 |- ( x = A -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = R )
183	182, 41	fvmptg 5961	. . . . . . . . . . . . 13 |- ( ( A e. ( A [,] B ) /\ R e. ( F lim CC A ) ) -> ( G ` A ) = R )
184	181, 3, 183	syl2anc 673	. . . . . . . . . . . 12 |- ( ph -> ( G ` A ) = R )
185	97	eqcomd 2477	. . . . . . . . . . . . . . . 16 |- ( ph -> ( x e. ( A (,) B ) |-> ( F ` x ) ) = F )
186	96, 185	eqtr2d 2506	. . . . . . . . . . . . . . 15 |- ( ph -> F = ( G |` ( A (,) B ) ) )
187	186	oveq1d 6323	. . . . . . . . . . . . . 14 |- ( ph -> ( F lim CC A ) = ( ( G |` ( A (,) B ) ) lim CC A ) )
188	3, 187	eleqtrd 2551	. . . . . . . . . . . . 13 |- ( ph -> R e. ( ( G |` ( A (,) B ) ) lim CC A ) )
189	18, 21, 24, 42	limciccioolb 37798	. . . . . . . . . . . . 13 |- ( ph -> ( ( G |` ( A (,) B ) ) lim CC A ) = ( G lim CC A ) )
190	188, 189	eleqtrd 2551	. . . . . . . . . . . 12 |- ( ph -> R e. ( G lim CC A ) )
191	184, 190	eqeltrd 2549	. . . . . . . . . . 11 |- ( ph -> ( G ` A ) e. ( G lim CC A ) )
192		eqid 2471	. . . . . . . . . . . . 13 |- ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) )
193	101, 192	cnplimc 22921	. . . . . . . . . . . 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 673	. . . . . . . . . . 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 936	. . . . . . . . . 10 |- ( ph -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) )
196	195	adantr 472	. . . . . . . . 9 |- ( ( ph /\ y = A ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) )
197		fveq2 5879	. . . . . . . . . . 11 |- ( y = A -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) )
198	197	eqcomd 2477	. . . . . . . . . 10 |- ( y = A -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
199	198	adantl 473	. . . . . . . . 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 2551	. . . . . . . 8 |- ( ( ph /\ y = A ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
201	21	leidd 10201	. . . . . . . . . . . . . . 15 |- ( ph -> B <_ B )
202	18, 21, 21, 25, 201	eliccd 37697	. . . . . . . . . . . . . 14 |- ( ph -> B e. ( A [,] B ) )
203		eqid 2471	. . . . . . . . . . . . . . . . . 18 |- B = B
204	203	iftruei 3879	. . . . . . . . . . . . . . . . 17 |- if ( B = B , L , ( F ` B ) ) = L
205	204, 8	syl5eqel 2553	. . . . . . . . . . . . . . . 16 |- ( ph -> if ( B = B , L , ( F ` B ) ) e. CC )
206	4, 205	ifcld 3915	. . . . . . . . . . . . . . 15 |- ( ph -> if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) e. CC )
207	202, 206	jca 541	. . . . . . . . . . . . . 14 |- ( ph -> ( B e. ( A [,] B ) /\ if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) e. CC ) )
208		nfv 1769	. . . . . . . . . . . . . . . 16 |- F/ x ( B e. ( A [,] B ) /\ if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) e. CC )
209		nfcv 2612	. . . . . . . . . . . . . . . . . 18 |- F/_ x B
210	53, 209	nffv 5886	. . . . . . . . . . . . . . . . 17 |- F/_ x ( G ` B )
211	210	nfeq1 2625	. . . . . . . . . . . . . . . 16 |- F/ x ( G ` B ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) )
212	208, 211	nfim 2023	. . . . . . . . . . . . . . 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 2537	. . . . . . . . . . . . . . . . 17 |- ( x = B -> ( x e. ( A [,] B ) <-> B e. ( A [,] B ) ) )
214	182	adantl 473	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = B /\ x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = R )
215		eqtr2 2491	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x = B /\ x = A ) -> B = A )
216		iftrue 3878	. . . . . . . . . . . . . . . . . . . . . 22 |- ( B = A -> if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) = R )
217	216	eqcomd 2477	. . . . . . . . . . . . . . . . . . . . 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 2505	. . . . . . . . . . . . . . . . . . 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 3881	. . . . . . . . . . . . . . . . . . . . 21 |- ( -. x = A -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
221	220	adantl 473	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = B /\ -. x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
222		iftrue 3878	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = B -> if ( x = B , L , ( F ` x ) ) = L )
223	222	adantr 472	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = B /\ -. x = A ) -> if ( x = B , L , ( F ` x ) ) = L )
224		df-ne 2643	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x =/= A <-> -. x = A )
225		pm13.18 2724	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( x = B /\ x =/= A ) -> B =/= A )
226	224, 225	sylan2br 484	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( x = B /\ -. x = A ) -> B =/= A )
227	226	neneqd 2648	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( x = B /\ -. x = A ) -> -. B = A )
228	227	iffalsed 3883	. . . . . . . . . . . . . . . . . . . . 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 2522	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = B /\ -. x = A ) -> L = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
230	221, 223, 229	3eqtrd 2509	. . . . . . . . . . . . . . . . . . 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 808	. . . . . . . . . . . . . . . . . 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 2533	. . . . . . . . . . . . . . . . 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 725	. . . . . . . . . . . . . . . 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 5879	. . . . . . . . . . . . . . . . 17 |- ( x = B -> ( G ` x ) = ( G ` B ) )
235	234, 231	eqeq12d 2486	. . . . . . . . . . . . . . . 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 327	. . . . . . . . . . . . . . 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 3092	. . . . . . . . . . . . . 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 61	. . . . . . . . . . . . 13 |- ( ph -> ( G ` B ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
239	18, 24	gtned 9787	. . . . . . . . . . . . . . 15 |- ( ph -> B =/= A )
240	239	neneqd 2648	. . . . . . . . . . . . . 14 |- ( ph -> -. B = A )
241	240	iffalsed 3883	. . . . . . . . . . . . 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 2509	. . . . . . . . . . . 12 |- ( ph -> ( G ` B ) = L )
244	186	oveq1d 6323	. . . . . . . . . . . . . 14 |- ( ph -> ( F lim CC B ) = ( ( G |` ( A (,) B ) ) lim CC B ) )
245	7, 244	eleqtrd 2551	. . . . . . . . . . . . 13 |- ( ph -> L e. ( ( G |` ( A (,) B ) ) lim CC B ) )
246	18, 21, 24, 42	limcicciooub 37814	. . . . . . . . . . . . 13 |- ( ph -> ( ( G |` ( A (,) B ) ) lim CC B ) = ( G lim CC B ) )
247	245, 246	eleqtrd 2551	. . . . . . . . . . . 12 |- ( ph -> L e. ( G lim CC B ) )
248	243, 247	eqeltrd 2549	. . . . . . . . . . 11 |- ( ph -> ( G ` B ) e. ( G lim CC B ) )
249	101, 192	cnplimc 22921	. . . . . . . . . . . 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 673	. . . . . . . . . . 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 936	. . . . . . . . . 10 |- ( ph -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` B ) )
252	251	adantr 472	. . . . . . . . 9 |- ( ( ph /\ y = B ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` B ) )
253		fveq2 5879	. . . . . . . . . . 11 |- ( y = B -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` B ) )
254	253	eqcomd 2477	. . . . . . . . . 10 |- ( y = B -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` B ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
255	254	adantl 473	. . . . . . . . 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 2551	. . . . . . . 8 |- ( ( ph /\ y = B ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
257	200, 256	jaodan 802	. . . . . . 7 |- ( ( ph /\ ( y = A \/ y = B ) ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
258	179, 257	sylan2 482	. . . . . 6 |- ( ( ph /\ y e. { A , B } ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
259	178, 258	jaodan 802	. . . . 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 478	. . . 4 |- ( ( ph /\ y e. ( A [,] B ) ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
261	260	ralrimiva 2809	. . 3 |- ( ph -> A. y e. ( A [,] B ) G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
262	101	cnfldtopon 21881	. . . . 5 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
263		resttopon 20254	. . . . 5 |- ( ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) /\ ( A [,] B ) C_ CC ) -> ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) e. (TopOn ` ( A [,] B ) ) )
264	262, 132, 263	sylancr 676	. . . 4 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) e. (TopOn ` ( A [,] B ) ) )
265		cncnp 20373	. . . 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 675	. . 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 936	. 2 |- ( ph -> G e. ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) Cn ( TopOpen ` ℂfld ) ) )
268	101, 192, 107	cncfcn 22019	. . 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 675	. 2 |- ( ph -> ( ( A [,] B ) -cn-> CC ) = ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) Cn ( TopOpen ` ℂfld ) ) )
270	267, 269	eleqtrrd 2552	1 |- ( ph -> G e. ( ( A [,] B ) -cn-> CC ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   \/ wo 375   /\ wa 376   /\ w3a 1007   = wceq 1452   F/wnf 1675   e. wcel 1904   =/= wne 2641   A.wral 2756   _Vcvv 3031   \ cdif 3387   u. cun 3388   i^i cin 3389   C_ wss 3390   ifcif 3872   {cpr 3961   U.cuni 4190   class class class wbr 4395   |-> cmpt 4454   ran crn 4840   |` cres 4841   -->wf 5585   ` cfv 5589  (class class class)co 6308   CCcc 9555   RRcr 9556   RR*cxr 9692   < clt 9693   <_ cle 9694   (,)cioo 11660   [,]cicc 11663   ↾_t crest 15397   TopOpenctopn 15398   topGenctg 15414  ℂ_fldccnfld 19047   Topctop 19994  TopOnctopon 19995   intcnt 20109   Cn ccn 20317   CnP ccnp 20318   -cn->ccncf 21986   lim CC climc 22896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-iin 4272  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-oadd 7204  df-er 7381  df-map 7492  df-pm 7493  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-fi 7943  df-sup 7974  df-inf 7975  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-4 10692  df-5 10693  df-6 10694  df-7 10695  df-8 10696  df-9 10697  df-10 10698  df-n0 10894  df-z 10962  df-dec 11075  df-uz 11183  df-q 11288  df-rp 11326  df-xneg 11432  df-xadd 11433  df-xmul 11434  df-ioo 11664  df-ioc 11665  df-ico 11666  df-icc 11667  df-fz 11811  df-seq 12252  df-exp 12311  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-struct 15201  df-ndx 15202  df-slot 15203  df-base 15204  df-plusg 15281  df-mulr 15282  df-starv 15283  df-tset 15287  df-ple 15288  df-ds 15290  df-unif 15291  df-rest 15399  df-topn 15400  df-topgen 15420  df-psmet 19039  df-xmet 19040  df-met 19041  df-bl 19042  df-mopn 19043  df-cnfld 19048  df-top 19998  df-bases 19999  df-topon 20000  df-topsp 20001  df-cld 20111  df-ntr 20112  df-cls 20113  df-cn 20320  df-cnp 20321  df-xms 21413  df-ms 21414  df-cncf 21988  df-limc 22900

This theorem is referenced by:  cncfiooicc  37869