Theorem cncfiooicclem1 37064

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 22571	. . . . . . 7 |- ( F lim CC A ) C_ CC
3		cncfiooicclem1.r	. . . . . . 7 |- ( ph -> R e. ( F lim CC A ) )
4	2, 3	sseldi 3440	. . . . . 6 |- ( ph -> R e. CC )
5	4	ad2antrr 724	. . . . 5 |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ x = A ) -> R e. CC )
6		limccl 22571	. . . . . . . 8 |- ( F lim CC B ) C_ CC
7		cncfiooicclem1.l	. . . . . . . 8 |- ( ph -> L e. ( F lim CC B ) )
8	6, 7	sseldi 3440	. . . . . . 7 |- ( ph -> L e. CC )
9	8	ad3antrrr 728	. . . . . 6 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ x = B ) -> L e. CC )
10		simplll 760	. . . . . . 7 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ph )
11		orel1 380	. . . . . . . . . . 11 |- ( -. x = A -> ( ( x = A \/ x = B ) -> x = B ) )
12	11	con3dimp 439	. . . . . . . . . 10 |- ( ( -. x = A /\ -. x = B ) -> -. ( x = A \/ x = B ) )
13		vex 3062	. . . . . . . . . . 11 |- x e. _V
14	13	elpr 3990	. . . . . . . . . 10 |- ( x e. { A , B } <-> ( x = A \/ x = B ) )
15	12, 14	sylnibr 303	. . . . . . . . 9 |- ( ( -. x = A /\ -. x = B ) -> -. x e. { A , B } )
16	15	adantll 712	. . . . . . . 8 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> -. x e. { A , B } )
17		simpllr 761	. . . . . . . . . 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 9673	. . . . . . . . . . . 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 9673	. . . . . . . . . . . 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 9765	. . . . . . . . . . . 12 |- ( ph -> A <_ B )
26	10, 25	syl 17	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> A <_ B )
27		prunioo 11703	. . . . . . . . . . 11 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
28	20, 23, 26, 27	syl3anc 1230	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
29	17, 28	eleqtrrd 2493	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> x e. ( ( A (,) B ) u. { A , B } ) )
30		elun 3584	. . . . . . . . 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 381	. . . . . . . 8 |- ( -. x e. { A , B } -> ( ( x e. ( A (,) B ) \/ x e. { A , B } ) -> x e. ( A (,) B ) ) )
33	16, 31, 32	sylc 59	. . . . . . 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 21689	. . . . . . . . 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 6009	. . . . . . 7 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( F ` x ) e. CC )
38	10, 33, 37	syl2anc 659	. . . . . 6 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( F ` x ) e. CC )
39	9, 38	ifclda 3917	. . . . 5 |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> if ( x = B , L , ( F ` x ) ) e. CC )
40	5, 39	ifclda 3917	. . . 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 6035	. . 3 |- ( ph -> G : ( A [,] B ) --> CC )
43		elun 3584	. . . . . . 7 |- ( y e. ( ( A (,) B ) u. { A , B } ) <-> ( y e. ( A (,) B ) \/ y e. { A , B } ) )
44	19, 22, 25, 27	syl3anc 1230	. . . . . . . 8 |- ( ph -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
45	44	eleq2d 2472	. . . . . . 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 483	. . . . 5 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( y e. ( A (,) B ) \/ y e. { A , B } ) )
48		ioossicc 11664	. . . . . . . . . . . . 13 |- ( A (,) B ) C_ ( A [,] B )
49		fssres 5734	. . . . . . . . . . . . 13 |- ( ( G : ( A [,] B ) --> CC /\ ( A (,) B ) C_ ( A [,] B ) ) -> ( G |` ( A (,) B ) ) : ( A (,) B ) --> CC )
50	42, 48, 49	sylancl 660	. . . . . . . . . . . 12 |- ( ph -> ( G |` ( A (,) B ) ) : ( A (,) B ) --> CC )
51	50	feqmptd 5902	. . . . . . . . . . 11 |- ( ph -> ( G |` ( A (,) B ) ) = ( y e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` y ) ) )
52		nfmpt1 4484	. . . . . . . . . . . . . . . 16 |- F/_ x ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
53	41, 52	nfcxfr 2562	. . . . . . . . . . . . . . 15 |- F/_ x G
54		nfcv 2564	. . . . . . . . . . . . . . 15 |- F/_ x ( A (,) B )
55	53, 54	nfres 5096	. . . . . . . . . . . . . 14 |- F/_ x ( G |` ( A (,) B ) )
56		nfcv 2564	. . . . . . . . . . . . . 14 |- F/_ x y
57	55, 56	nffv 5856	. . . . . . . . . . . . 13 |- F/_ x ( ( G |` ( A (,) B ) ) ` y )
58		nfcv 2564	. . . . . . . . . . . . . 14 |- F/_ y ( G |` ( A (,) B ) )
59		nfcv 2564	. . . . . . . . . . . . . 14 |- F/_ y x
60	58, 59	nffv 5856	. . . . . . . . . . . . 13 |- F/_ y ( ( G |` ( A (,) B ) ) ` x )
61		fveq2 5849	. . . . . . . . . . . . 13 |- ( y = x -> ( ( G |` ( A (,) B ) ) ` y ) = ( ( G |` ( A (,) B ) ) ` x ) )
62	57, 60, 61	cbvmpt 4486	. . . . . . . . . . . 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 5863	. . . . . . . . . . . . . 14 |- ( x e. ( A (,) B ) -> ( ( G |` ( A (,) B ) ) ` x ) = ( G ` x ) )
65	64	adantl 464	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( G |` ( A (,) B ) ) ` x ) = ( G ` x ) )
66		simpr 459	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( A (,) B ) )
67	48, 66	sseldi 3440	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( A [,] B ) )
68	4	adantr 463	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( A (,) B ) ) -> R e. CC )
69	8	ad2antrr 724	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( A (,) B ) ) /\ x = B ) -> L e. CC )
70	37	adantr 463	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( A (,) B ) ) /\ -. x = B ) -> ( F ` x ) e. CC )
71	69, 70	ifclda 3917	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = B , L , ( F ` x ) ) e. CC )
72	68, 71	ifcld 3928	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC )
73	41	fvmpt2 5941	. . . . . . . . . . . . . 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 659	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( G ` x ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
75		elioo4g 11639	. . . . . . . . . . . . . . . . . . . . 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 457	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( A (,) B ) -> ( A e. RR* /\ B e. RR* /\ x e. RR ) )
78	77	simp1d 1009	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( A (,) B ) -> A e. RR* )
79		elioore 11612	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( A (,) B ) -> x e. RR )
80	79	rexrd 9673	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( A (,) B ) -> x e. RR* )
81		eliooord 11638	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( A (,) B ) -> ( A < x /\ x < B ) )
82	81	simpld 457	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( A (,) B ) -> A < x )
83		xrltne 11419	. . . . . . . . . . . . . . . . . 18 |- ( ( A e. RR* /\ x e. RR* /\ A < x ) -> x =/= A )
84	78, 80, 82, 83	syl3anc 1230	. . . . . . . . . . . . . . . . 17 |- ( x e. ( A (,) B ) -> x =/= A )
85	84	adantl 464	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( A (,) B ) ) -> x =/= A )
86	85	neneqd 2605	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( A (,) B ) ) -> -. x = A )
87	86	iffalsed 3896	. . . . . . . . . . . . . 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 461	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( A (,) B ) -> x < B )
89	79, 88	ltned 9753	. . . . . . . . . . . . . . . . 17 |- ( x e. ( A (,) B ) -> x =/= B )
90	89	neneqd 2605	. . . . . . . . . . . . . . . 16 |- ( x e. ( A (,) B ) -> -. x = B )
91	90	iffalsed 3896	. . . . . . . . . . . . . . 15 |- ( x e. ( A (,) B ) -> if ( x = B , L , ( F ` x ) ) = ( F ` x ) )
92	91	adantl 464	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = B , L , ( F ` x ) ) = ( F ` x ) )
93	87, 92	eqtrd 2443	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = ( F ` x ) )
94	65, 74, 93	3eqtrd 2447	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( G |` ( A (,) B ) ) ` x ) = ( F ` x ) )
95	1, 94	mpteq2da 4480	. . . . . . . . . . 11 |- ( ph -> ( x e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` x ) ) = ( x e. ( A (,) B ) |-> ( F ` x ) ) )
96	51, 63, 95	3eqtrd 2447	. . . . . . . . . 10 |- ( ph -> ( G |` ( A (,) B ) ) = ( x e. ( A (,) B ) |-> ( F ` x ) ) )
97	36	feqmptd 5902	. . . . . . . . . . 11 |- ( ph -> F = ( x e. ( A (,) B ) |-> ( F ` x ) ) )
98		ioosscn 36896	. . . . . . . . . . . . 13 |- ( A (,) B ) C_ CC
99	98	a1i 11	. . . . . . . . . . . 12 |- ( ph -> ( A (,) B ) C_ CC )
100		ssid 3461	. . . . . . . . . . . 12 |- CC C_ CC
101		eqid 2402	. . . . . . . . . . . . 13 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
102		eqid 2402	. . . . . . . . . . . . 13 |- ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) )
103	101	cnfldtop 21583	. . . . . . . . . . . . . . 15 |- ( TopOpen ` ℂfld ) e. Top
104		unicntop 36807	. . . . . . . . . . . . . . . 16 |- CC = U. ( TopOpen ` ℂfld )
105	104	restid 15048	. . . . . . . . . . . . . . 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 2415	. . . . . . . . . . . . 13 |- ( TopOpen ` ℂfld ) = ( ( TopOpen ` ℂfld ) ↾t CC )
108	101, 102, 107	cncfcn 21705	. . . . . . . . . . . 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 660	. . . . . . . . . . 11 |- ( ph -> ( ( A (,) B ) -cn-> CC ) = ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
110	34, 97, 109	3eltr3d 2504	. . . . . . . . . 10 |- ( ph -> ( x e. ( A (,) B ) |-> ( F ` x ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
111	96, 110	eqeltrd 2490	. . . . . . . . 9 |- ( ph -> ( G |` ( A (,) B ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
112	104	restuni 19956	. . . . . . . . . . 11 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ ( A (,) B ) C_ CC ) -> ( A (,) B ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) )
113	103, 98, 112	mp2an 670	. . . . . . . . . 10 |- ( A (,) B ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) )
114	113	cncnpi 20072	. . . . . . . . 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 469	. . . . . . . 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 6306	. . . . . . . . . . . . 13 |- ( A [,] B ) e. _V
119	118	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( A [,] B ) e. _V )
120		restabs 19959	. . . . . . . . . . . 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 1230	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) )
122	121	eqcomd 2410	. . . . . . . . . 10 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) = ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) )
123	122	oveq1d 6293	. . . . . . . . 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 5851	. . . . . . . 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 2492	. . . . . . 7 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( G |` ( A (,) B ) ) e. ( ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
126		resttop 19954	. . . . . . . . . 10 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ ( A [,] B ) e. _V ) -> ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) e. Top )
127	103, 118, 126	mp2an 670	. . . . . . . . 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 36907	. . . . . . . . . . . 12 |- ( ph -> ( A [,] B ) C_ RR )
131		ax-resscn 9579	. . . . . . . . . . . 12 |- RR C_ CC
132	130, 131	syl6ss 3454	. . . . . . . . . . 11 |- ( ph -> ( A [,] B ) C_ CC )
133	104	restuni 19956	. . . . . . . . . . 11 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ ( A [,] B ) C_ CC ) -> ( A [,] B ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
134	103, 132, 133	sylancr 661	. . . . . . . . . 10 |- ( ph -> ( A [,] B ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
135	129, 134	sseqtrd 3478	. . . . . . . . 9 |- ( ph -> ( A (,) B ) C_ U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
136	135	adantr 463	. . . . . . . 8 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( A (,) B ) C_ U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
137		retop 21560	. . . . . . . . . . . . . 14 |- ( topGen ` ran (,) ) e. Top
138	137	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( topGen ` ran (,) ) e. Top )
139		ioossre 11640	. . . . . . . . . . . . . . 15 |- ( A (,) B ) C_ RR
140		difss 3570	. . . . . . . . . . . . . . 15 |- ( RR \ ( A [,] B ) ) C_ RR
141	139, 140	unssi 3618	. . . . . . . . . . . . . 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 3606	. . . . . . . . . . . . . 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 21561	. . . . . . . . . . . . . 14 |- RR = U. ( topGen ` ran (,) )
146	145	ntrss 19848	. . . . . . . . . . . . 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 1230	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) C_ ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
148		simpr 459	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( A (,) B ) )
149		ioontr 36917	. . . . . . . . . . . . 13 |- ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B )
150	148, 149	syl6eleqr 2501	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) )
151	147, 150	sseldd 3443	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
152	48, 148	sseldi 3440	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( A [,] B ) )
153	151, 152	elind 3627	. . . . . . . . . 10 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) i^i ( A [,] B ) ) )
154	130	adantr 463	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( A [,] B ) C_ RR )
155		eqid 2402	. . . . . . . . . . . 12 |- ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) = ( ( topGen ` ran (,) ) ↾t ( A [,] B ) )
156	145, 155	restntr 19976	. . . . . . . . . . 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 1230	. . . . . . . . . 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 2493	. . . . . . . . 9 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) )
159	101	tgioo2 21600	. . . . . . . . . . . . . . 15 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
160	159	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR ) )
161	160	oveq1d 6293	. . . . . . . . . . . . 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 9613	. . . . . . . . . . . . . . 15 |- RR e. _V
164	163	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> RR e. _V )
165		restabs 19959	. . . . . . . . . . . . . 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 1230	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( TopOpen ` ℂfld ) ↾t RR ) ↾t ( A [,] B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
167	161, 166	eqtrd 2443	. . . . . . . . . . . 12 |- ( ph -> ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
168	167	fveq2d 5853	. . . . . . . . . . 11 |- ( ph -> ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) = ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) )
169	168	fveq1d 5851	. . . . . . . . . 10 |- ( ph -> ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) = ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) )
170	169	adantr 463	. . . . . . . . 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 2492	. . . . . . . 8 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) )
172	134	feq2d 5701	. . . . . . . . . 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 463	. . . . . . . 8 |- ( ( ph /\ y e. ( A (,) B ) ) -> G : U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) --> CC )
175		eqid 2402	. . . . . . . . 9 |- U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) )
176	175, 104	cnprest 20083	. . . . . . . 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 1231	. . . . . . 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 3992	. . . . . . 7 |- ( y e. { A , B } -> ( y = A \/ y = B ) )
180		lbicc2 11690	. . . . . . . . . . . . . 14 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
181	19, 22, 25, 180	syl3anc 1230	. . . . . . . . . . . . 13 |- ( ph -> A e. ( A [,] B ) )
182		iftrue 3891	. . . . . . . . . . . . . 14 |- ( x = A -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = R )
183	182, 41	fvmptg 5930	. . . . . . . . . . . . 13 |- ( ( A e. ( A [,] B ) /\ R e. ( F lim CC A ) ) -> ( G ` A ) = R )
184	181, 3, 183	syl2anc 659	. . . . . . . . . . . 12 |- ( ph -> ( G ` A ) = R )
185	97	eqcomd 2410	. . . . . . . . . . . . . . . 16 |- ( ph -> ( x e. ( A (,) B ) |-> ( F ` x ) ) = F )
186	96, 185	eqtr2d 2444	. . . . . . . . . . . . . . 15 |- ( ph -> F = ( G |` ( A (,) B ) ) )
187	186	oveq1d 6293	. . . . . . . . . . . . . 14 |- ( ph -> ( F lim CC A ) = ( ( G |` ( A (,) B ) ) lim CC A ) )
188	3, 187	eleqtrd 2492	. . . . . . . . . . . . 13 |- ( ph -> R e. ( ( G |` ( A (,) B ) ) lim CC A ) )
189	18, 21, 24, 42	limciccioolb 36995	. . . . . . . . . . . . 13 |- ( ph -> ( ( G |` ( A (,) B ) ) lim CC A ) = ( G lim CC A ) )
190	188, 189	eleqtrd 2492	. . . . . . . . . . . 12 |- ( ph -> R e. ( G lim CC A ) )
191	184, 190	eqeltrd 2490	. . . . . . . . . . 11 |- ( ph -> ( G ` A ) e. ( G lim CC A ) )
192		eqid 2402	. . . . . . . . . . . . 13 |- ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) )
193	101, 192	cnplimc 22583	. . . . . . . . . . . 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 659	. . . . . . . . . . 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 923	. . . . . . . . . 10 |- ( ph -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) )
196	195	adantr 463	. . . . . . . . 9 |- ( ( ph /\ y = A ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) )
197		fveq2 5849	. . . . . . . . . . 11 |- ( y = A -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) )
198	197	eqcomd 2410	. . . . . . . . . 10 |- ( y = A -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
199	198	adantl 464	. . . . . . . . 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 2492	. . . . . . . 8 |- ( ( ph /\ y = A ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
201	21	leidd 10159	. . . . . . . . . . . . . . 15 |- ( ph -> B <_ B )
202	18, 21, 21, 25, 201	eliccd 36906	. . . . . . . . . . . . . 14 |- ( ph -> B e. ( A [,] B ) )
203		eqid 2402	. . . . . . . . . . . . . . . . . 18 |- B = B
204	203	iftruei 3892	. . . . . . . . . . . . . . . . 17 |- if ( B = B , L , ( F ` B ) ) = L
205	204, 8	syl5eqel 2494	. . . . . . . . . . . . . . . 16 |- ( ph -> if ( B = B , L , ( F ` B ) ) e. CC )
206	4, 205	ifcld 3928	. . . . . . . . . . . . . . 15 |- ( ph -> if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) e. CC )
207	202, 206	jca 530	. . . . . . . . . . . . . 14 |- ( ph -> ( B e. ( A [,] B ) /\ if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) e. CC ) )
208		nfv 1728	. . . . . . . . . . . . . . . 16 |- F/ x ( B e. ( A [,] B ) /\ if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) e. CC )
209		nfcv 2564	. . . . . . . . . . . . . . . . . 18 |- F/_ x B
210	53, 209	nffv 5856	. . . . . . . . . . . . . . . . 17 |- F/_ x ( G ` B )
211	210	nfeq1 2579	. . . . . . . . . . . . . . . 16 |- F/ x ( G ` B ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) )
212	208, 211	nfim 1948	. . . . . . . . . . . . . . 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 2474	. . . . . . . . . . . . . . . . 17 |- ( x = B -> ( x e. ( A [,] B ) <-> B e. ( A [,] B ) ) )
214	182	adantl 464	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = B /\ x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = R )
215		eqtr2 2429	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x = B /\ x = A ) -> B = A )
216		iftrue 3891	. . . . . . . . . . . . . . . . . . . . . 22 |- ( B = A -> if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) = R )
217	216	eqcomd 2410	. . . . . . . . . . . . . . . . . . . . 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 2443	. . . . . . . . . . . . . . . . . . 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 3894	. . . . . . . . . . . . . . . . . . . . 21 |- ( -. x = A -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
221	220	adantl 464	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = B /\ -. x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
222		iftrue 3891	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = B -> if ( x = B , L , ( F ` x ) ) = L )
223	222	adantr 463	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = B /\ -. x = A ) -> if ( x = B , L , ( F ` x ) ) = L )
224		df-ne 2600	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x =/= A <-> -. x = A )
225		pm13.18 2714	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( x = B /\ x =/= A ) -> B =/= A )
226	224, 225	sylan2br 474	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( x = B /\ -. x = A ) -> B =/= A )
227	226	neneqd 2605	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( x = B /\ -. x = A ) -> -. B = A )
228	227	iffalsed 3896	. . . . . . . . . . . . . . . . . . . . 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 2460	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x = B /\ -. x = A ) -> L = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
230	221, 223, 229	3eqtrd 2447	. . . . . . . . . . . . . . . . . . 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 792	. . . . . . . . . . . . . . . . . 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 2471	. . . . . . . . . . . . . . . . 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 709	. . . . . . . . . . . . . . . 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 5849	. . . . . . . . . . . . . . . . 17 |- ( x = B -> ( G ` x ) = ( G ` B ) )
235	234, 231	eqeq12d 2424	. . . . . . . . . . . . . . . 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 318	. . . . . . . . . . . . . . 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 3116	. . . . . . . . . . . . . 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 59	. . . . . . . . . . . . 13 |- ( ph -> ( G ` B ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
239	18, 24	gtned 9752	. . . . . . . . . . . . . . 15 |- ( ph -> B =/= A )
240	239	neneqd 2605	. . . . . . . . . . . . . 14 |- ( ph -> -. B = A )
241	240	iffalsed 3896	. . . . . . . . . . . . 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 2447	. . . . . . . . . . . 12 |- ( ph -> ( G ` B ) = L )
244	186	oveq1d 6293	. . . . . . . . . . . . . 14 |- ( ph -> ( F lim CC B ) = ( ( G |` ( A (,) B ) ) lim CC B ) )
245	7, 244	eleqtrd 2492	. . . . . . . . . . . . 13 |- ( ph -> L e. ( ( G |` ( A (,) B ) ) lim CC B ) )
246	18, 21, 24, 42	limcicciooub 37011	. . . . . . . . . . . . 13 |- ( ph -> ( ( G |` ( A (,) B ) ) lim CC B ) = ( G lim CC B ) )
247	245, 246	eleqtrd 2492	. . . . . . . . . . . 12 |- ( ph -> L e. ( G lim CC B ) )
248	243, 247	eqeltrd 2490	. . . . . . . . . . 11 |- ( ph -> ( G ` B ) e. ( G lim CC B ) )
249	101, 192	cnplimc 22583	. . . . . . . . . . . 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 659	. . . . . . . . . . 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 923	. . . . . . . . . 10 |- ( ph -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` B ) )
252	251	adantr 463	. . . . . . . . 9 |- ( ( ph /\ y = B ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` B ) )
253		fveq2 5849	. . . . . . . . . . 11 |- ( y = B -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` B ) )
254	253	eqcomd 2410	. . . . . . . . . 10 |- ( y = B -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` B ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
255	254	adantl 464	. . . . . . . . 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 2492	. . . . . . . 8 |- ( ( ph /\ y = B ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
257	200, 256	jaodan 786	. . . . . . 7 |- ( ( ph /\ ( y = A \/ y = B ) ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
258	179, 257	sylan2 472	. . . . . 6 |- ( ( ph /\ y e. { A , B } ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
259	178, 258	jaodan 786	. . . . 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 468	. . . 4 |- ( ( ph /\ y e. ( A [,] B ) ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
261	260	ralrimiva 2818	. . 3 |- ( ph -> A. y e. ( A [,] B ) G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
262	101	cnfldtopon 21582	. . . . 5 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
263		resttopon 19955	. . . . 5 |- ( ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) /\ ( A [,] B ) C_ CC ) -> ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) e. (TopOn ` ( A [,] B ) ) )
264	262, 132, 263	sylancr 661	. . . 4 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) e. (TopOn ` ( A [,] B ) ) )
265		cncnp 20074	. . . 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 660	. . 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 923	. 2 |- ( ph -> G e. ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) Cn ( TopOpen ` ℂfld ) ) )
268	101, 192, 107	cncfcn 21705	. . 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 660	. 2 |- ( ph -> ( ( A [,] B ) -cn-> CC ) = ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) Cn ( TopOpen ` ℂfld ) ) )
270	267, 269	eleqtrrd 2493	1 |- ( ph -> G e. ( ( A [,] B ) -cn-> CC ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 366   /\ wa 367   /\ w3a 974   = wceq 1405   F/wnf 1637   e. wcel 1842   =/= wne 2598   A.wral 2754   _Vcvv 3059   \ cdif 3411   u. cun 3412   i^i cin 3413   C_ wss 3414   ifcif 3885   {cpr 3974   U.cuni 4191   class class class wbr 4395   |-> cmpt 4453   ran crn 4824   |` cres 4825   -->wf 5565   ` cfv 5569  (class class class)co 6278   CCcc 9520   RRcr 9521   RR*cxr 9657   < clt 9658   <_ cle 9659   (,)cioo 11582   [,]cicc 11585   ↾_t crest 15035   TopOpenctopn 15036   topGenctg 15052  ℂ_fldccnfld 18740   Topctop 19686  TopOnctopon 19687   intcnt 19810   Cn ccn 20018   CnP ccnp 20019   -cn->ccncf 21672   lim CC climc 22558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4507  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574  ax-cnex 9578  ax-resscn 9579  ax-1cn 9580  ax-icn 9581  ax-addcl 9582  ax-addrcl 9583  ax-mulcl 9584  ax-mulrcl 9585  ax-mulcom 9586  ax-addass 9587  ax-mulass 9588  ax-distr 9589  ax-i2m1 9590  ax-1ne0 9591  ax-1rid 9592  ax-rnegex 9593  ax-rrecex 9594  ax-cnre 9595  ax-pre-lttri 9596  ax-pre-lttrn 9597  ax-pre-ltadd 9598  ax-pre-mulgt0 9599  ax-pre-sup 9600

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2759  df-rex 2760  df-reu 2761  df-rmo 2762  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-pss 3430  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-tp 3977  df-op 3979  df-uni 4192  df-int 4228  df-iun 4273  df-iin 4274  df-br 4396  df-opab 4454  df-mpt 4455  df-tr 4490  df-eprel 4734  df-id 4738  df-po 4744  df-so 4745  df-fr 4782  df-we 4784  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-pred 5367  df-ord 5413  df-on 5414  df-lim 5415  df-suc 5416  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-fv 5577  df-riota 6240  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-om 6684  df-1st 6784  df-2nd 6785  df-wrecs 7013  df-recs 7075  df-rdg 7113  df-1o 7167  df-oadd 7171  df-er 7348  df-map 7459  df-pm 7460  df-en 7555  df-dom 7556  df-sdom 7557  df-fin 7558  df-fi 7905  df-sup 7935  df-pnf 9660  df-mnf 9661  df-xr 9662  df-ltxr 9663  df-le 9664  df-sub 9843  df-neg 9844  df-div 10248  df-nn 10577  df-2 10635  df-3 10636  df-4 10637  df-5 10638  df-6 10639  df-7 10640  df-8 10641  df-9 10642  df-10 10643  df-n0 10837  df-z 10906  df-dec 11020  df-uz 11128  df-q 11228  df-rp 11266  df-xneg 11371  df-xadd 11372  df-xmul 11373  df-ioo 11586  df-ioc 11587  df-ico 11588  df-icc 11589  df-fz 11727  df-seq 12152  df-exp 12211  df-cj 13081  df-re 13082  df-im 13083  df-sqrt 13217  df-abs 13218  df-struct 14843  df-ndx 14844  df-slot 14845  df-base 14846  df-plusg 14922  df-mulr 14923  df-starv 14924  df-tset 14928  df-ple 14929  df-ds 14931  df-unif 14932  df-rest 15037  df-topn 15038  df-topgen 15058  df-psmet 18731  df-xmet 18732  df-met 18733  df-bl 18734  df-mopn 18735  df-cnfld 18741  df-top 19691  df-bases 19693  df-topon 19694  df-topsp 19695  df-cld 19812  df-ntr 19813  df-cls 19814  df-cn 20021  df-cnp 20022  df-xms 21115  df-ms 21116  df-cncf 21674  df-limc 22562

This theorem is referenced by:  cncfiooicc  37065