Theorem cncfiooicclem1 37597

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 22822	. . . . . . 7 |- ( F lim CC A ) C_ CC
3		cncfiooicclem1.r	. . . . . . 7 |- ( ph -> R e. ( F lim CC A ) )
4	2, 3	sseldi 3463	. . . . . 6 |- ( ph -> R e. CC )
5	4	ad2antrr 731	. . . . 5 |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ x = A ) -> R e. CC )
6		limccl 22822	. . . . . . . 8 |- ( F lim CC B ) C_ CC
7		cncfiooicclem1.l	. . . . . . . 8 |- ( ph -> L e. ( F lim CC B ) )
8	6, 7	sseldi 3463	. . . . . . 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 3085	. . . . . . . . . . 11 |- x e. _V
14	13	elpr 4015	. . . . . . . . . 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 9692	. . . . . . . . . . . 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 9692	. . . . . . . . . . . 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 9785	. . . . . . . . . . . 12 |- ( ph -> A <_ B )
26	10, 25	syl 17	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> A <_ B )
27		prunioo 11763	. . . . . . . . . . 11 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
28	20, 23, 26, 27	syl3anc 1265	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
29	17, 28	eleqtrrd 2514	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> x e. ( ( A (,) B ) u. { A , B } ) )
30		elun 3607	. . . . . . . . 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 63	. . . . . . 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 21917	. . . . . . . . 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 6035	. . . . . . 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 3942	. . . . 5 |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> if ( x = B , L , ( F ` x ) ) e. CC )
40	5, 39	ifclda 3942	. . . 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 6061	. . 3 |- ( ph -> G : ( A [,] B ) --> CC )
43		elun 3607	. . . . . . 7 |- ( y e. ( ( A (,) B ) u. { A , B } ) <-> ( y e. ( A (,) B ) \/ y e. { A , B } ) )
44	19, 22, 25, 27	syl3anc 1265	. . . . . . . 8 |- ( ph -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
45	44	eleq2d 2493	. . . . . . 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 11722	. . . . . . . . . . . . 13 |- ( A (,) B ) C_ ( A [,] B )
49		fssres 5764	. . . . . . . . . . . . 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 5932	. . . . . . . . . . 11 |- ( ph -> ( G |` ( A (,) B ) ) = ( y e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` y ) ) )
52		nfmpt1 4511	. . . . . . . . . . . . . . . 16 |- F/_ x ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
53	41, 52	nfcxfr 2583	. . . . . . . . . . . . . . 15 |- F/_ x G
54		nfcv 2585	. . . . . . . . . . . . . . 15 |- F/_ x ( A (,) B )
55	53, 54	nfres 5124	. . . . . . . . . . . . . 14 |- F/_ x ( G |` ( A (,) B ) )
56		nfcv 2585	. . . . . . . . . . . . . 14 |- F/_ x y
57	55, 56	nffv 5886	. . . . . . . . . . . . 13 |- F/_ x ( ( G |` ( A (,) B ) ) ` y )
58		nfcv 2585	. . . . . . . . . . . . . 14 |- F/_ y ( G |` ( A (,) B ) )
59		nfcv 2585	. . . . . . . . . . . . . 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 4513	. . . . . . . . . . . 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 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 3463	. . . . . . . . . . . . . 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 3942	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = B , L , ( F ` x ) ) e. CC )
72	68, 71	ifcld 3953	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC )
73	41	fvmpt2 5971	. . . . . . . . . . . . . 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 11697	. . . . . . . . . . . . . . . . . . . . 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 1018	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( A (,) B ) -> A e. RR* )
79		elioore 11668	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( A (,) B ) -> x e. RR )
80	79	rexrd 9692	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( A (,) B ) -> x e. RR* )
81		eliooord 11696	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( A (,) B ) -> ( A < x /\ x < B ) )
82	81	simpld 461	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( A (,) B ) -> A < x )
83		xrltne 11462	. . . . . . . . . . . . . . . . . 18 |- ( ( A e. RR* /\ x e. RR* /\ A < x ) -> x =/= A )
84	78, 80, 82, 83	syl3anc 1265	. . . . . . . . . . . . . . . . 17 |- ( x e. ( A (,) B ) -> x =/= A )
85	84	adantl 468	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( A (,) B ) ) -> x =/= A )
86	85	neneqd 2626	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( A (,) B ) ) -> -. x = A )
87	86	iffalsed 3921	. . . . . . . . . . . . . 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 9773	. . . . . . . . . . . . . . . . 17 |- ( x e. ( A (,) B ) -> x =/= B )
90	89	neneqd 2626	. . . . . . . . . . . . . . . 16 |- ( x e. ( A (,) B ) -> -. x = B )
91	90	iffalsed 3921	. . . . . . . . . . . . . . 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 2464	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = ( F ` x ) )
94	65, 74, 93	3eqtrd 2468	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( G |` ( A (,) B ) ) ` x ) = ( F ` x ) )
95	1, 94	mpteq2da 4507	. . . . . . . . . . 11 |- ( ph -> ( x e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` x ) ) = ( x e. ( A (,) B ) |-> ( F ` x ) ) )
96	51, 63, 95	3eqtrd 2468	. . . . . . . . . 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 37428	. . . . . . . . . . . . 13 |- ( A (,) B ) C_ CC
99	98	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( A (,) B ) C_ CC )
100		ssid 3484	. . . . . . . . . . . 12 |- CC C_ CC
101		eqid 2423	. . . . . . . . . . . . 13 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
102		eqid 2423	. . . . . . . . . . . . 13 |- ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) )
103	101	cnfldtop 21796	. . . . . . . . . . . . . . 15 |- ( TopOpen ` ℂfld ) e. Top
104		unicntop 37238	. . . . . . . . . . . . . . . 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 2436	. . . . . . . . . . . . 13 |- ( TopOpen ` ℂfld ) = ( ( TopOpen ` ℂfld ) ↾t CC )
108	101, 102, 107	cncfcn 21933	. . . . . . . . . . . 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 2525	. . . . . . . . . 10 |- ( ph -> ( x e. ( A (,) B ) |-> ( F ` x ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
111	96, 110	eqeltrd 2511	. . . . . . . . 9 |- ( ph -> ( G |` ( A (,) B ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
112	104	restuni 20170	. . . . . . . . . . 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 20286	. . . . . . . . 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 6331	. . . . . . . . . . . . 13 |- ( A [,] B ) e. _V
119	118	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( A [,] B ) e. _V )
120		restabs 20173	. . . . . . . . . . . 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 1265	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) )
122	121	eqcomd 2431	. . . . . . . . . 10 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) = ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) )
123	122	oveq1d 6318	. . . . . . . . 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 2513	. . . . . . 7 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( G |` ( A (,) B ) ) e. ( ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
126		resttop 20168	. . . . . . . . . 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 37439	. . . . . . . . . . . 12 |- ( ph -> ( A [,] B ) C_ RR )
131		ax-resscn 9598	. . . . . . . . . . . 12 |- RR C_ CC
132	130, 131	syl6ss 3477	. . . . . . . . . . 11 |- ( ph -> ( A [,] B ) C_ CC )
133	104	restuni 20170	. . . . . . . . . . 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 3501	. . . . . . . . 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 21774	. . . . . . . . . . . . . 14 |- ( topGen ` ran (,) ) e. Top
138	137	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( topGen ` ran (,) ) e. Top )
139		ioossre 11698	. . . . . . . . . . . . . . 15 |- ( A (,) B ) C_ RR
140		difss 3593	. . . . . . . . . . . . . . 15 |- ( RR \ ( A [,] B ) ) C_ RR
141	139, 140	unssi 3642	. . . . . . . . . . . . . 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 3630	. . . . . . . . . . . . . 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 21775	. . . . . . . . . . . . . 14 |- RR = U. ( topGen ` ran (,) )
146	145	ntrss 20062	. . . . . . . . . . . . 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 1265	. . . . . . . . . . . 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 37448	. . . . . . . . . . . . 13 |- ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B )
150	148, 149	syl6eleqr 2522	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) )
151	147, 150	sseldd 3466	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
152	48, 148	sseldi 3463	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( A [,] B ) )
153	151, 152	elind 3651	. . . . . . . . . 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 2423	. . . . . . . . . . . 12 |- ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) = ( ( topGen ` ran (,) ) ↾t ( A [,] B ) )
156	145, 155	restntr 20190	. . . . . . . . . . 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 1265	. . . . . . . . . 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 2514	. . . . . . . . 9 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) )
159	101	tgioo2 21813	. . . . . . . . . . . . . . 15 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
160	159	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR ) )
161	160	oveq1d 6318	. . . . . . . . . . . . 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 9632	. . . . . . . . . . . . . . 15 |- RR e. _V
164	163	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> RR e. _V )
165		restabs 20173	. . . . . . . . . . . . . 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 1265	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( TopOpen ` ℂfld ) ↾t RR ) ↾t ( A [,] B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
167	161, 166	eqtrd 2464	. . . . . . . . . . . 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 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 2513	. . . . . . . 8 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) )
172	134	feq2d 5731	. . . . . . . . . 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 2423	. . . . . . . . 9 |- U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) )
176	175, 104	cnprest 20297	. . . . . . . 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 1266	. . . . . . 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 4014	. . . . . . 7 |- ( y e. { A , B } -> ( y = A \/ y = B ) )
180		lbicc2 11750	. . . . . . . . . . . . . 14 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
181	19, 22, 25, 180	syl3anc 1265	. . . . . . . . . . . . 13 |- ( ph -> A e. ( A [,] B ) )
182		iftrue 3916	. . . . . . . . . . . . . 14 |- ( x = A -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = R )
183	182, 41	fvmptg 5960	. . . . . . . . . . . . 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 2431	. . . . . . . . . . . . . . . 16 |- ( ph -> ( x e. ( A (,) B ) |-> ( F ` x ) ) = F )
186	96, 185	eqtr2d 2465	. . . . . . . . . . . . . . 15 |- ( ph -> F = ( G |` ( A (,) B ) ) )
187	186	oveq1d 6318	. . . . . . . . . . . . . 14 |- ( ph -> ( F lim CC A ) = ( ( G |` ( A (,) B ) ) lim CC A ) )
188	3, 187	eleqtrd 2513	. . . . . . . . . . . . 13 |- ( ph -> R e. ( ( G |` ( A (,) B ) ) lim CC A ) )
189	18, 21, 24, 42	limciccioolb 37527	. . . . . . . . . . . . 13 |- ( ph -> ( ( G |` ( A (,) B ) ) lim CC A ) = ( G lim CC A ) )
190	188, 189	eleqtrd 2513	. . . . . . . . . . . 12 |- ( ph -> R e. ( G lim CC A ) )
191	184, 190	eqeltrd 2511	. . . . . . . . . . 11 |- ( ph -> ( G ` A ) e. ( G lim CC A ) )
192		eqid 2423	. . . . . . . . . . . . 13 |- ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) )
193	101, 192	cnplimc 22834	. . . . . . . . . . . 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 931	. . . . . . . . . 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 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 2431	. . . . . . . . . 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 2513	. . . . . . . 8 |- ( ( ph /\ y = A ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
201	21	leidd 10182	. . . . . . . . . . . . . . 15 |- ( ph -> B <_ B )
202	18, 21, 21, 25, 201	eliccd 37438	. . . . . . . . . . . . . 14 |- ( ph -> B e. ( A [,] B ) )
203		eqid 2423	. . . . . . . . . . . . . . . . . 18 |- B = B
204	203	iftruei 3917	. . . . . . . . . . . . . . . . 17 |- if ( B = B , L , ( F ` B ) ) = L
205	204, 8	syl5eqel 2515	. . . . . . . . . . . . . . . 16 |- ( ph -> if ( B = B , L , ( F ` B ) ) e. CC )
206	4, 205	ifcld 3953	. . . . . . . . . . . . . . 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 1752	. . . . . . . . . . . . . . . 16 |- F/ x ( B e. ( A [,] B ) /\ if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) e. CC )
209		nfcv 2585	. . . . . . . . . . . . . . . . . 18 |- F/_ x B
210	53, 209	nffv 5886	. . . . . . . . . . . . . . . . 17 |- F/_ x ( G ` B )
211	210	nfeq1 2600	. . . . . . . . . . . . . . . 16 |- F/ x ( G ` B ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) )
212	208, 211	nfim 1977	. . . . . . . . . . . . . . 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 2495	. . . . . . . . . . . . . . . . 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 2450	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x = B /\ x = A ) -> B = A )
216		iftrue 3916	. . . . . . . . . . . . . . . . . . . . . 22 |- ( B = A -> if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) = R )
217	216	eqcomd 2431	. . . . . . . . . . . . . . . . . . . . 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 2464	. . . . . . . . . . . . . . . . . . 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 3919	. . . . . . . . . . . . . . . . . . . . 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 3916	. . . . . . . . . . . . . . . . . . . . 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 2621	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x =/= A <-> -. x = A )
225		pm13.18 2736	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( x = B /\ x =/= A ) -> B =/= A )
226	224, 225	sylan2br 479	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( x = B /\ -. x = A ) -> B =/= A )
227	226	neneqd 2626	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( x = B /\ -. x = A ) -> -. B = A )
228	227	iffalsed 3921	. . . . . . . . . . . . . . . . . . . . 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 2481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = B /\ -. x = A ) -> L = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
230	221, 223, 229	3eqtrd 2468	. . . . . . . . . . . . . . . . . . 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 2492	. . . . . . . . . . . . . . . . 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 5879	. . . . . . . . . . . . . . . . 17 |- ( x = B -> ( G ` x ) = ( G ` B ) )
235	234, 231	eqeq12d 2445	. . . . . . . . . . . . . . . 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 3139	. . . . . . . . . . . . . 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 63	. . . . . . . . . . . . 13 |- ( ph -> ( G ` B ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
239	18, 24	gtned 9772	. . . . . . . . . . . . . . 15 |- ( ph -> B =/= A )
240	239	neneqd 2626	. . . . . . . . . . . . . 14 |- ( ph -> -. B = A )
241	240	iffalsed 3921	. . . . . . . . . . . . 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 2468	. . . . . . . . . . . 12 |- ( ph -> ( G ` B ) = L )
244	186	oveq1d 6318	. . . . . . . . . . . . . 14 |- ( ph -> ( F lim CC B ) = ( ( G |` ( A (,) B ) ) lim CC B ) )
245	7, 244	eleqtrd 2513	. . . . . . . . . . . . 13 |- ( ph -> L e. ( ( G |` ( A (,) B ) ) lim CC B ) )
246	18, 21, 24, 42	limcicciooub 37543	. . . . . . . . . . . . 13 |- ( ph -> ( ( G |` ( A (,) B ) ) lim CC B ) = ( G lim CC B ) )
247	245, 246	eleqtrd 2513	. . . . . . . . . . . 12 |- ( ph -> L e. ( G lim CC B ) )
248	243, 247	eqeltrd 2511	. . . . . . . . . . 11 |- ( ph -> ( G ` B ) e. ( G lim CC B ) )
249	101, 192	cnplimc 22834	. . . . . . . . . . . 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 931	. . . . . . . . . 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 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 2431	. . . . . . . . . 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 2513	. . . . . . . 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 2840	. . 3 |- ( ph -> A. y e. ( A [,] B ) G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
262	101	cnfldtopon 21795	. . . . 5 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
263		resttopon 20169	. . . . 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 20288	. . . 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 931	. 2 |- ( ph -> G e. ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) Cn ( TopOpen ` ℂfld ) ) )
268	101, 192, 107	cncfcn 21933	. . 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 2514	1 |- ( ph -> G e. ( ( A [,] B ) -cn-> CC ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   \/ wo 370   /\ wa 371   /\ w3a 983   = wceq 1438   F/wnf 1664   e. wcel 1869   =/= wne 2619   A.wral 2776   _Vcvv 3082   \ cdif 3434   u. cun 3435   i^i cin 3436   C_ wss 3437   ifcif 3910   {cpr 3999   U.cuni 4217   class class class wbr 4421   |-> cmpt 4480   ran crn 4852   |` cres 4853   -->wf 5595   ` cfv 5599  (class class class)co 6303   CCcc 9539   RRcr 9540   RR*cxr 9676   < clt 9677   <_ cle 9678   (,)cioo 11637   [,]cicc 11640   ↾_t crest 15312   TopOpenctopn 15313   topGenctg 15329  ℂ_fldccnfld 18963   Topctop 19909  TopOnctopon 19910   intcnt 20024   Cn ccn 20232   CnP ccnp 20233   -cn->ccncf 21900   lim CC climc 22809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-rep 4534  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595  ax-cnex 9597  ax-resscn 9598  ax-1cn 9599  ax-icn 9600  ax-addcl 9601  ax-addrcl 9602  ax-mulcl 9603  ax-mulrcl 9604  ax-mulcom 9605  ax-addass 9606  ax-mulass 9607  ax-distr 9608  ax-i2m1 9609  ax-1ne0 9610  ax-1rid 9611  ax-rnegex 9612  ax-rrecex 9613  ax-cnre 9614  ax-pre-lttri 9615  ax-pre-lttrn 9616  ax-pre-ltadd 9617  ax-pre-mulgt0 9618  ax-pre-sup 9619

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-ral 2781  df-rex 2782  df-reu 2783  df-rmo 2784  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-tp 4002  df-op 4004  df-uni 4218  df-int 4254  df-iun 4299  df-iin 4300  df-br 4422  df-opab 4481  df-mpt 4482  df-tr 4517  df-eprel 4762  df-id 4766  df-po 4772  df-so 4773  df-fr 4810  df-we 4812  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-pred 5397  df-ord 5443  df-on 5444  df-lim 5445  df-suc 5446  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-riota 6265  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-om 6705  df-1st 6805  df-2nd 6806  df-wrecs 7034  df-recs 7096  df-rdg 7134  df-1o 7188  df-oadd 7192  df-er 7369  df-map 7480  df-pm 7481  df-en 7576  df-dom 7577  df-sdom 7578  df-fin 7579  df-fi 7929  df-sup 7960  df-inf 7961  df-pnf 9679  df-mnf 9680  df-xr 9681  df-ltxr 9682  df-le 9683  df-sub 9864  df-neg 9865  df-div 10272  df-nn 10612  df-2 10670  df-3 10671  df-4 10672  df-5 10673  df-6 10674  df-7 10675  df-8 10676  df-9 10677  df-10 10678  df-n0 10872  df-z 10940  df-dec 11054  df-uz 11162  df-q 11267  df-rp 11305  df-xneg 11411  df-xadd 11412  df-xmul 11413  df-ioo 11641  df-ioc 11642  df-ico 11643  df-icc 11644  df-fz 11787  df-seq 12215  df-exp 12274  df-cj 13156  df-re 13157  df-im 13158  df-sqrt 13292  df-abs 13293  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 19913  df-bases 19914  df-topon 19915  df-topsp 19916  df-cld 20026  df-ntr 20027  df-cls 20028  df-cn 20235  df-cnp 20236  df-xms 21327  df-ms 21328  df-cncf 21902  df-limc 22813

This theorem is referenced by:  cncfiooicc  37598