Theorem cncfiooicclem1 31878

Description: A continuous function F on an open interval ( A (,) B ) can be extended to a continuous function G on the corresponding close 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 22405	. . . . . . 7 |- ( F lim CC A ) C_ CC
3		cncfiooicclem1.r	. . . . . . 7 |- ( ph -> R e. ( F lim CC A ) )
4	2, 3	sseldi 3497	. . . . . 6 |- ( ph -> R e. CC )
5	4	ad2antrr 725	. . . . 5 |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ x = A ) -> R e. CC )
6		limccl 22405	. . . . . . . 8 |- ( F lim CC B ) C_ CC
7		cncfiooicclem1.l	. . . . . . . 8 |- ( ph -> L e. ( F lim CC B ) )
8	6, 7	sseldi 3497	. . . . . . 7 |- ( ph -> L e. CC )
9	8	ad3antrrr 729	. . . . . 6 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ x = B ) -> L e. CC )
10		simplll 759	. . . . . . 7 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ph )
11		orel1 382	. . . . . . . . . . 11 |- ( -. x = A -> ( ( x = A \/ x = B ) -> x = B ) )
12	11	con3dimp 441	. . . . . . . . . 10 |- ( ( -. x = A /\ -. x = B ) -> -. ( x = A \/ x = B ) )
13		vex 3112	. . . . . . . . . . 11 |- x e. _V
14	13	elpr 4050	. . . . . . . . . 10 |- ( x e. { A , B } <-> ( x = A \/ x = B ) )
15	12, 14	sylnibr 305	. . . . . . . . 9 |- ( ( -. x = A /\ -. x = B ) -> -. x e. { A , B } )
16	15	adantll 713	. . . . . . . 8 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> -. x e. { A , B } )
17		simpllr 760	. . . . . . . . . 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 9660	. . . . . . . . . . . 12 |- ( ph -> A e. RR* )
20	10, 19	syl 16	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> A e. RR* )
21		cncfiooicclem1.b	. . . . . . . . . . . . 13 |- ( ph -> B e. RR )
22	21	rexrd 9660	. . . . . . . . . . . 12 |- ( ph -> B e. RR* )
23	10, 22	syl 16	. . . . . . . . . . 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 9750	. . . . . . . . . . . 12 |- ( ph -> A <_ B )
26	10, 25	syl 16	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> A <_ B )
27		prunioo 11674	. . . . . . . . . . 11 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
28	20, 23, 26, 27	syl3anc 1228	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
29	17, 28	eleqtrrd 2548	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> x e. ( ( A (,) B ) u. { A , B } ) )
30		elun 3641	. . . . . . . . 9 |- ( x e. ( ( A (,) B ) u. { A , B } ) <-> ( x e. ( A (,) B ) \/ x e. { A , B } ) )
31	29, 30	sylib 196	. . . . . . . 8 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( x e. ( A (,) B ) \/ x e. { A , B } ) )
32		orel2 383	. . . . . . . 8 |- ( -. x e. { A , B } -> ( ( x e. ( A (,) B ) \/ x e. { A , B } ) -> x e. ( A (,) B ) ) )
33	16, 31, 32	sylc 60	. . . . . . 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 21523	. . . . . . . . 9 |- ( F e. ( ( A (,) B ) -cn-> CC ) -> F : ( A (,) B ) --> CC )
36	34, 35	syl 16	. . . . . . . 8 |- ( ph -> F : ( A (,) B ) --> CC )
37	36	ffvelrnda 6032	. . . . . . 7 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( F ` x ) e. CC )
38	10, 33, 37	syl2anc 661	. . . . . 6 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( F ` x ) e. CC )
39	9, 38	ifclda 3976	. . . . 5 |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> if ( x = B , L , ( F ` x ) ) e. CC )
40	5, 39	ifclda 3976	. . . 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 6057	. . 3 |- ( ph -> G : ( A [,] B ) --> CC )
43		elun 3641	. . . . . . 7 |- ( y e. ( ( A (,) B ) u. { A , B } ) <-> ( y e. ( A (,) B ) \/ y e. { A , B } ) )
44	19, 22, 25, 27	syl3anc 1228	. . . . . . . 8 |- ( ph -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
45	44	eleq2d 2527	. . . . . . 7 |- ( ph -> ( y e. ( ( A (,) B ) u. { A , B } ) <-> y e. ( A [,] B ) ) )
46	43, 45	syl5bbr 259	. . . . . 6 |- ( ph -> ( ( y e. ( A (,) B ) \/ y e. { A , B } ) <-> y e. ( A [,] B ) ) )
47	46	biimpar 485	. . . . 5 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( y e. ( A (,) B ) \/ y e. { A , B } ) )
48		ioossicc 11635	. . . . . . . . . . . . 13 |- ( A (,) B ) C_ ( A [,] B )
49		fssres 5757	. . . . . . . . . . . . 13 |- ( ( G : ( A [,] B ) --> CC /\ ( A (,) B ) C_ ( A [,] B ) ) -> ( G |` ( A (,) B ) ) : ( A (,) B ) --> CC )
50	42, 48, 49	sylancl 662	. . . . . . . . . . . 12 |- ( ph -> ( G |` ( A (,) B ) ) : ( A (,) B ) --> CC )
51	50	feqmptd 5926	. . . . . . . . . . 11 |- ( ph -> ( G |` ( A (,) B ) ) = ( y e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` y ) ) )
52		nfmpt1 4546	. . . . . . . . . . . . . . . 16 |- F/_ x ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
53	41, 52	nfcxfr 2617	. . . . . . . . . . . . . . 15 |- F/_ x G
54		nfcv 2619	. . . . . . . . . . . . . . 15 |- F/_ x ( A (,) B )
55	53, 54	nfres 5285	. . . . . . . . . . . . . 14 |- F/_ x ( G |` ( A (,) B ) )
56		nfcv 2619	. . . . . . . . . . . . . 14 |- F/_ x y
57	55, 56	nffv 5879	. . . . . . . . . . . . 13 |- F/_ x ( ( G |` ( A (,) B ) ) ` y )
58		nfcv 2619	. . . . . . . . . . . . . 14 |- F/_ y ( G |` ( A (,) B ) )
59		nfcv 2619	. . . . . . . . . . . . . 14 |- F/_ y x
60	58, 59	nffv 5879	. . . . . . . . . . . . 13 |- F/_ y ( ( G |` ( A (,) B ) ) ` x )
61		fveq2 5872	. . . . . . . . . . . . 13 |- ( y = x -> ( ( G |` ( A (,) B ) ) ` y ) = ( ( G |` ( A (,) B ) ) ` x ) )
62	57, 60, 61	cbvmpt 4547	. . . . . . . . . . . 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 5886	. . . . . . . . . . . . . 14 |- ( x e. ( A (,) B ) -> ( ( G |` ( A (,) B ) ) ` x ) = ( G ` x ) )
65	64	adantl 466	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( G |` ( A (,) B ) ) ` x ) = ( G ` x ) )
66		simpr 461	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( A (,) B ) )
67	48, 66	sseldi 3497	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( A [,] B ) )
68	4	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( A (,) B ) ) -> R e. CC )
69	8	ad2antrr 725	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( A (,) B ) ) /\ x = B ) -> L e. CC )
70	37	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( A (,) B ) ) /\ -. x = B ) -> ( F ` x ) e. CC )
71	69, 70	ifclda 3976	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = B , L , ( F ` x ) ) e. CC )
72	68, 71	ifcld 3987	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC )
73	41	fvmpt2 5964	. . . . . . . . . . . . . 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 661	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( G ` x ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
75		elioo4g 11610	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. ( A (,) B ) <-> ( ( A e. RR* /\ B e. RR* /\ x e. RR ) /\ ( A < x /\ x < B ) ) )
76	75	biimpi 194	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( A (,) B ) -> ( ( A e. RR* /\ B e. RR* /\ x e. RR ) /\ ( A < x /\ x < B ) ) )
77	76	simpld 459	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( A (,) B ) -> ( A e. RR* /\ B e. RR* /\ x e. RR ) )
78	77	simp1d 1008	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( A (,) B ) -> A e. RR* )
79		elioore 11584	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( A (,) B ) -> x e. RR )
80	79	rexrd 9660	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( A (,) B ) -> x e. RR* )
81		eliooord 11609	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( A (,) B ) -> ( A < x /\ x < B ) )
82	81	simpld 459	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( A (,) B ) -> A < x )
83		xrltne 11391	. . . . . . . . . . . . . . . . . 18 |- ( ( A e. RR* /\ x e. RR* /\ A < x ) -> x =/= A )
84	78, 80, 82, 83	syl3anc 1228	. . . . . . . . . . . . . . . . 17 |- ( x e. ( A (,) B ) -> x =/= A )
85	84	adantl 466	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( A (,) B ) ) -> x =/= A )
86	85	neneqd 2659	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( A (,) B ) ) -> -. x = A )
87	86	iffalsed 3955	. . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( A (,) B ) -> x < B )
89	79, 88	ltned 9738	. . . . . . . . . . . . . . . . 17 |- ( x e. ( A (,) B ) -> x =/= B )
90	89	neneqd 2659	. . . . . . . . . . . . . . . 16 |- ( x e. ( A (,) B ) -> -. x = B )
91	90	iffalsed 3955	. . . . . . . . . . . . . . 15 |- ( x e. ( A (,) B ) -> if ( x = B , L , ( F ` x ) ) = ( F ` x ) )
92	91	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = B , L , ( F ` x ) ) = ( F ` x ) )
93	87, 92	eqtrd 2498	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = ( F ` x ) )
94	65, 74, 93	3eqtrd 2502	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( G |` ( A (,) B ) ) ` x ) = ( F ` x ) )
95	1, 94	mpteq2da 4542	. . . . . . . . . . 11 |- ( ph -> ( x e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` x ) ) = ( x e. ( A (,) B ) |-> ( F ` x ) ) )
96	51, 63, 95	3eqtrd 2502	. . . . . . . . . 10 |- ( ph -> ( G |` ( A (,) B ) ) = ( x e. ( A (,) B ) |-> ( F ` x ) ) )
97	36	feqmptd 5926	. . . . . . . . . . 11 |- ( ph -> F = ( x e. ( A (,) B ) |-> ( F ` x ) ) )
98		ioosscn 31709	. . . . . . . . . . . . 13 |- ( A (,) B ) C_ CC
99	98	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( A (,) B ) C_ CC )
100		ssid 3518	. . . . . . . . . . . 12 |- CC C_ CC
101		eqid 2457	. . . . . . . . . . . . 13 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
102		eqid 2457	. . . . . . . . . . . . 13 |- ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) )
103	101	cnfldtop 21417	. . . . . . . . . . . . . . 15 |- ( TopOpen ` ℂfld ) e. Top
104		unicntop 31613	. . . . . . . . . . . . . . . 16 |- CC = U. ( TopOpen ` ℂfld )
105	104	restid 14851	. . . . . . . . . . . . . . 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 2470	. . . . . . . . . . . . 13 |- ( TopOpen ` ℂfld ) = ( ( TopOpen ` ℂfld ) ↾t CC )
108	101, 102, 107	cncfcn 21539	. . . . . . . . . . . 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 662	. . . . . . . . . . 11 |- ( ph -> ( ( A (,) B ) -cn-> CC ) = ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
110	34, 97, 109	3eltr3d 2559	. . . . . . . . . 10 |- ( ph -> ( x e. ( A (,) B ) |-> ( F ` x ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
111	96, 110	eqeltrd 2545	. . . . . . . . 9 |- ( ph -> ( G |` ( A (,) B ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
112	104	restuni 19790	. . . . . . . . . . 11 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ ( A (,) B ) C_ CC ) -> ( A (,) B ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) )
113	103, 98, 112	mp2an 672	. . . . . . . . . 10 |- ( A (,) B ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) )
114	113	cncnpi 19906	. . . . . . . . 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 471	. . . . . . . 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 6324	. . . . . . . . . . . . 13 |- ( A [,] B ) e. _V
119	118	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( A [,] B ) e. _V )
120		restabs 19793	. . . . . . . . . . . 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 1228	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) )
122	121	eqcomd 2465	. . . . . . . . . 10 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) = ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) )
123	122	oveq1d 6311	. . . . . . . . 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 5874	. . . . . . . 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 2547	. . . . . . 7 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( G |` ( A (,) B ) ) e. ( ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
126		resttop 19788	. . . . . . . . . 10 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ ( A [,] B ) e. _V ) -> ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) e. Top )
127	103, 118, 126	mp2an 672	. . . . . . . . 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 31721	. . . . . . . . . . . 12 |- ( ph -> ( A [,] B ) C_ RR )
131		ax-resscn 9566	. . . . . . . . . . . 12 |- RR C_ CC
132	130, 131	syl6ss 3511	. . . . . . . . . . 11 |- ( ph -> ( A [,] B ) C_ CC )
133	104	restuni 19790	. . . . . . . . . . 11 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ ( A [,] B ) C_ CC ) -> ( A [,] B ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
134	103, 132, 133	sylancr 663	. . . . . . . . . 10 |- ( ph -> ( A [,] B ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
135	129, 134	sseqtrd 3535	. . . . . . . . 9 |- ( ph -> ( A (,) B ) C_ U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
136	135	adantr 465	. . . . . . . 8 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( A (,) B ) C_ U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
137		retop 21394	. . . . . . . . . . . . . 14 |- ( topGen ` ran (,) ) e. Top
138	137	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( topGen ` ran (,) ) e. Top )
139		ioossre 11611	. . . . . . . . . . . . . . 15 |- ( A (,) B ) C_ RR
140		difss 3627	. . . . . . . . . . . . . . 15 |- ( RR \ ( A [,] B ) ) C_ RR
141	139, 140	unssi 3675	. . . . . . . . . . . . . 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 3663	. . . . . . . . . . . . . 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 21395	. . . . . . . . . . . . . 14 |- RR = U. ( topGen ` ran (,) )
146	145	ntrss 19683	. . . . . . . . . . . . 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 1228	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) C_ ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
148		simpr 461	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( A (,) B ) )
149		ioontr 31731	. . . . . . . . . . . . 13 |- ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B )
150	148, 149	syl6eleqr 2556	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) )
151	147, 150	sseldd 3500	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
152	48, 148	sseldi 3497	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( A [,] B ) )
153	151, 152	elind 3684	. . . . . . . . . 10 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) i^i ( A [,] B ) ) )
154	130	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( A [,] B ) C_ RR )
155		eqid 2457	. . . . . . . . . . . 12 |- ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) = ( ( topGen ` ran (,) ) ↾t ( A [,] B ) )
156	145, 155	restntr 19810	. . . . . . . . . . 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 1228	. . . . . . . . . 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 2548	. . . . . . . . 9 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) )
159	101	tgioo2 21434	. . . . . . . . . . . . . . 15 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
160	159	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR ) )
161	160	oveq1d 6311	. . . . . . . . . . . . 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 9600	. . . . . . . . . . . . . . 15 |- RR e. _V
164	163	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> RR e. _V )
165		restabs 19793	. . . . . . . . . . . . . 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 1228	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( TopOpen ` ℂfld ) ↾t RR ) ↾t ( A [,] B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
167	161, 166	eqtrd 2498	. . . . . . . . . . . 12 |- ( ph -> ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
168	167	fveq2d 5876	. . . . . . . . . . 11 |- ( ph -> ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) = ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) )
169	168	fveq1d 5874	. . . . . . . . . 10 |- ( ph -> ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) = ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) )
170	169	adantr 465	. . . . . . . . 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 2547	. . . . . . . 8 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) )
172	134	feq2d 5724	. . . . . . . . . 10 |- ( ph -> ( G : ( A [,] B ) --> CC <-> G : U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) --> CC ) )
173	42, 172	mpbid 210	. . . . . . . . 9 |- ( ph -> G : U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) --> CC )
174	173	adantr 465	. . . . . . . 8 |- ( ( ph /\ y e. ( A (,) B ) ) -> G : U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) --> CC )
175		eqid 2457	. . . . . . . . 9 |- U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) )
176	175, 104	cnprest 19917	. . . . . . . 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 1229	. . . . . . 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 232	. . . . . 6 |- ( ( ph /\ y e. ( A (,) B ) ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
179		elpri 4052	. . . . . . 7 |- ( y e. { A , B } -> ( y = A \/ y = B ) )
180		lbicc2 11661	. . . . . . . . . . . . . 14 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
181	19, 22, 25, 180	syl3anc 1228	. . . . . . . . . . . . 13 |- ( ph -> A e. ( A [,] B ) )
182		iftrue 3950	. . . . . . . . . . . . . 14 |- ( x = A -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = R )
183	182, 41	fvmptg 5954	. . . . . . . . . . . . 13 |- ( ( A e. ( A [,] B ) /\ R e. ( F lim CC A ) ) -> ( G ` A ) = R )
184	181, 3, 183	syl2anc 661	. . . . . . . . . . . 12 |- ( ph -> ( G ` A ) = R )
185	97	eqcomd 2465	. . . . . . . . . . . . . . . 16 |- ( ph -> ( x e. ( A (,) B ) |-> ( F ` x ) ) = F )
186	96, 185	eqtr2d 2499	. . . . . . . . . . . . . . 15 |- ( ph -> F = ( G |` ( A (,) B ) ) )
187	186	oveq1d 6311	. . . . . . . . . . . . . 14 |- ( ph -> ( F lim CC A ) = ( ( G |` ( A (,) B ) ) lim CC A ) )
188	3, 187	eleqtrd 2547	. . . . . . . . . . . . 13 |- ( ph -> R e. ( ( G |` ( A (,) B ) ) lim CC A ) )
189	18, 21, 24, 42	limciccioolb 31809	. . . . . . . . . . . . 13 |- ( ph -> ( ( G |` ( A (,) B ) ) lim CC A ) = ( G lim CC A ) )
190	188, 189	eleqtrd 2547	. . . . . . . . . . . 12 |- ( ph -> R e. ( G lim CC A ) )
191	184, 190	eqeltrd 2545	. . . . . . . . . . 11 |- ( ph -> ( G ` A ) e. ( G lim CC A ) )
192		eqid 2457	. . . . . . . . . . . . 13 |- ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) )
193	101, 192	cnplimc 22417	. . . . . . . . . . . 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 661	. . . . . . . . . . 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 922	. . . . . . . . . 10 |- ( ph -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) )
196	195	adantr 465	. . . . . . . . 9 |- ( ( ph /\ y = A ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) )
197		fveq2 5872	. . . . . . . . . . 11 |- ( y = A -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) )
198	197	eqcomd 2465	. . . . . . . . . 10 |- ( y = A -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
199	198	adantl 466	. . . . . . . . 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 2547	. . . . . . . 8 |- ( ( ph /\ y = A ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
201	21	leidd 10140	. . . . . . . . . . . . . . 15 |- ( ph -> B <_ B )
202	18, 21, 21, 25, 201	eliccd 31720	. . . . . . . . . . . . . 14 |- ( ph -> B e. ( A [,] B ) )
203		eqid 2457	. . . . . . . . . . . . . . . . . 18 |- B = B
204	203	iftruei 3951	. . . . . . . . . . . . . . . . 17 |- if ( B = B , L , ( F ` B ) ) = L
205	204, 8	syl5eqel 2549	. . . . . . . . . . . . . . . 16 |- ( ph -> if ( B = B , L , ( F ` B ) ) e. CC )
206	4, 205	ifcld 3987	. . . . . . . . . . . . . . 15 |- ( ph -> if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) e. CC )
207	202, 206	jca 532	. . . . . . . . . . . . . 14 |- ( ph -> ( B e. ( A [,] B ) /\ if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) e. CC ) )
208		nfv 1708	. . . . . . . . . . . . . . . 16 |- F/ x ( B e. ( A [,] B ) /\ if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) e. CC )
209		nfcv 2619	. . . . . . . . . . . . . . . . . 18 |- F/_ x B
210	53, 209	nffv 5879	. . . . . . . . . . . . . . . . 17 |- F/_ x ( G ` B )
211	210	nfeq1 2634	. . . . . . . . . . . . . . . 16 |- F/ x ( G ` B ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) )
212	208, 211	nfim 1921	. . . . . . . . . . . . . . 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 2529	. . . . . . . . . . . . . . . . 17 |- ( x = B -> ( x e. ( A [,] B ) <-> B e. ( A [,] B ) ) )
214	182	adantl 466	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = B /\ x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = R )
215		eqtr2 2484	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x = B /\ x = A ) -> B = A )
216		iftrue 3950	. . . . . . . . . . . . . . . . . . . . . 22 |- ( B = A -> if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) = R )
217	216	eqcomd 2465	. . . . . . . . . . . . . . . . . . . . 21 |- ( B = A -> R = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
218	215, 217	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = B /\ x = A ) -> R = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
219	214, 218	eqtrd 2498	. . . . . . . . . . . . . . . . . . 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 3953	. . . . . . . . . . . . . . . . . . . . 21 |- ( -. x = A -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
221	220	adantl 466	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = B /\ -. x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
222		iftrue 3950	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = B -> if ( x = B , L , ( F ` x ) ) = L )
223	222	adantr 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = B /\ -. x = A ) -> if ( x = B , L , ( F ` x ) ) = L )
224		df-ne 2654	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x =/= A <-> -. x = A )
225		pm13.18 2768	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( x = B /\ x =/= A ) -> B =/= A )
226	224, 225	sylan2br 476	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( x = B /\ -. x = A ) -> B =/= A )
227	226	neneqd 2659	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( x = B /\ -. x = A ) -> -. B = A )
228	227	iffalsed 3955	. . . . . . . . . . . . . . . . . . . . 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 2515	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = B /\ -. x = A ) -> L = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
230	221, 223, 229	3eqtrd 2502	. . . . . . . . . . . . . . . . . . 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 791	. . . . . . . . . . . . . . . . . 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 2526	. . . . . . . . . . . . . . . . 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 710	. . . . . . . . . . . . . . . 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 5872	. . . . . . . . . . . . . . . . 17 |- ( x = B -> ( G ` x ) = ( G ` B ) )
235	234, 231	eqeq12d 2479	. . . . . . . . . . . . . . . 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 320	. . . . . . . . . . . . . . 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 3166	. . . . . . . . . . . . . 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 60	. . . . . . . . . . . . 13 |- ( ph -> ( G ` B ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
239	18, 24	gtned 9737	. . . . . . . . . . . . . . 15 |- ( ph -> B =/= A )
240	239	neneqd 2659	. . . . . . . . . . . . . 14 |- ( ph -> -. B = A )
241	240	iffalsed 3955	. . . . . . . . . . . . 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 2502	. . . . . . . . . . . 12 |- ( ph -> ( G ` B ) = L )
244	186	oveq1d 6311	. . . . . . . . . . . . . 14 |- ( ph -> ( F lim CC B ) = ( ( G |` ( A (,) B ) ) lim CC B ) )
245	7, 244	eleqtrd 2547	. . . . . . . . . . . . 13 |- ( ph -> L e. ( ( G |` ( A (,) B ) ) lim CC B ) )
246	18, 21, 24, 42	limcicciooub 31825	. . . . . . . . . . . . 13 |- ( ph -> ( ( G |` ( A (,) B ) ) lim CC B ) = ( G lim CC B ) )
247	245, 246	eleqtrd 2547	. . . . . . . . . . . 12 |- ( ph -> L e. ( G lim CC B ) )
248	243, 247	eqeltrd 2545	. . . . . . . . . . 11 |- ( ph -> ( G ` B ) e. ( G lim CC B ) )
249	101, 192	cnplimc 22417	. . . . . . . . . . . 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 661	. . . . . . . . . . 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 922	. . . . . . . . . 10 |- ( ph -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` B ) )
252	251	adantr 465	. . . . . . . . 9 |- ( ( ph /\ y = B ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` B ) )
253		fveq2 5872	. . . . . . . . . . 11 |- ( y = B -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` B ) )
254	253	eqcomd 2465	. . . . . . . . . 10 |- ( y = B -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` B ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
255	254	adantl 466	. . . . . . . . 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 2547	. . . . . . . 8 |- ( ( ph /\ y = B ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
257	200, 256	jaodan 785	. . . . . . 7 |- ( ( ph /\ ( y = A \/ y = B ) ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
258	179, 257	sylan2 474	. . . . . 6 |- ( ( ph /\ y e. { A , B } ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
259	178, 258	jaodan 785	. . . . 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 470	. . . 4 |- ( ( ph /\ y e. ( A [,] B ) ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
261	260	ralrimiva 2871	. . 3 |- ( ph -> A. y e. ( A [,] B ) G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
262	101	cnfldtopon 21416	. . . . 5 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
263		resttopon 19789	. . . . 5 |- ( ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) /\ ( A [,] B ) C_ CC ) -> ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) e. (TopOn ` ( A [,] B ) ) )
264	262, 132, 263	sylancr 663	. . . 4 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) e. (TopOn ` ( A [,] B ) ) )
265		cncnp 19908	. . . 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 662	. . 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 922	. 2 |- ( ph -> G e. ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) Cn ( TopOpen ` ℂfld ) ) )
268	101, 192, 107	cncfcn 21539	. . 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 662	. 2 |- ( ph -> ( ( A [,] B ) -cn-> CC ) = ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) Cn ( TopOpen ` ℂfld ) ) )
270	267, 269	eleqtrrd 2548	1 |- ( ph -> G e. ( ( A [,] B ) -cn-> CC ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   /\ w3a 973   = wceq 1395   F/wnf 1617   e. wcel 1819   =/= wne 2652   A.wral 2807   _Vcvv 3109   \ cdif 3468   u. cun 3469   i^i cin 3470   C_ wss 3471   ifcif 3944   {cpr 4034   U.cuni 4251   class class class wbr 4456   |-> cmpt 4515   ran crn 5009   |` cres 5010   -->wf 5590   ` cfv 5594  (class class class)co 6296   CCcc 9507   RRcr 9508   RR*cxr 9644   < clt 9645   <_ cle 9646   (,)cioo 11554   [,]cicc 11557   ↾_t crest 14838   TopOpenctopn 14839   topGenctg 14855  ℂ_fldccnfld 18547   Topctop 19521  TopOnctopon 19522   intcnt 19645   Cn ccn 19852   CnP ccnp 19853   -cn->ccncf 21506   lim CC climc 22392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-cnex 9565  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-mulcom 9573  ax-addass 9574  ax-mulass 9575  ax-distr 9576  ax-i2m1 9577  ax-1ne0 9578  ax-1rid 9579  ax-rnegex 9580  ax-rrecex 9581  ax-cnre 9582  ax-pre-lttri 9583  ax-pre-lttrn 9584  ax-pre-ltadd 9585  ax-pre-mulgt0 9586  ax-pre-sup 9587

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-int 4289  df-iun 4334  df-iin 4335  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6700  df-1st 6799  df-2nd 6800  df-recs 7060  df-rdg 7094  df-1o 7148  df-oadd 7152  df-er 7329  df-map 7440  df-pm 7441  df-en 7536  df-dom 7537  df-sdom 7538  df-fin 7539  df-fi 7889  df-sup 7919  df-pnf 9647  df-mnf 9648  df-xr 9649  df-ltxr 9650  df-le 9651  df-sub 9826  df-neg 9827  df-div 10228  df-nn 10557  df-2 10615  df-3 10616  df-4 10617  df-5 10618  df-6 10619  df-7 10620  df-8 10621  df-9 10622  df-10 10623  df-n0 10817  df-z 10886  df-dec 11001  df-uz 11107  df-q 11208  df-rp 11246  df-xneg 11343  df-xadd 11344  df-xmul 11345  df-ioo 11558  df-ioc 11559  df-ico 11560  df-icc 11561  df-fz 11698  df-seq 12111  df-exp 12170  df-cj 12944  df-re 12945  df-im 12946  df-sqrt 13080  df-abs 13081  df-struct 14646  df-ndx 14647  df-slot 14648  df-base 14649  df-plusg 14725  df-mulr 14726  df-starv 14727  df-tset 14731  df-ple 14732  df-ds 14734  df-unif 14735  df-rest 14840  df-topn 14841  df-topgen 14861  df-psmet 18538  df-xmet 18539  df-met 18540  df-bl 18541  df-mopn 18542  df-cnfld 18548  df-top 19526  df-bases 19528  df-topon 19529  df-topsp 19530  df-cld 19647  df-ntr 19648  df-cls 19649  df-cn 19855  df-cnp 19856  df-xms 20949  df-ms 20950  df-cncf 21508  df-limc 22396

This theorem is referenced by:  cncfiooicc  31879