Theorem cncfiooicclem1 31555

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	. . . . . 6 |- F/ x ph
2		limccl 22147	. . . . . . . . . 10 |- ( F lim CC A ) C_ CC
3		cncfiooicclem1.r	. . . . . . . . . 10 |- ( ph -> R e. ( F lim CC A ) )
4	2, 3	sseldi 3507	. . . . . . . . 9 |- ( ph -> R e. CC )
5	4	ad2antrr 725	. . . . . . . 8 |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ x = A ) -> R e. CC )
6		limccl 22147	. . . . . . . . . . 11 |- ( F lim CC B ) C_ CC
7		cncfiooicclem1.l	. . . . . . . . . . 11 |- ( ph -> L e. ( F lim CC B ) )
8	6, 7	sseldi 3507	. . . . . . . . . 10 |- ( ph -> L e. CC )
9	8	ad3antrrr 729	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ x = B ) -> L e. CC )
10		simplll 757	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ph )
11		simplr 754	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> -. x = A )
12		simpr 461	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> -. x = B )
13	11, 12	jca 532	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( -. x = A /\ -. x = B ) )
14		orel1 382	. . . . . . . . . . . . . . 15 |- ( -. x = A -> ( ( x = A \/ x = B ) -> x = B ) )
15	14	con3dimp 441	. . . . . . . . . . . . . 14 |- ( ( -. x = A /\ -. x = B ) -> -. ( x = A \/ x = B ) )
16		vex 3121	. . . . . . . . . . . . . . 15 |- x e. _V
17	16	elpr 4051	. . . . . . . . . . . . . 14 |- ( x e. { A , B } <-> ( x = A \/ x = B ) )
18	15, 17	sylnibr 305	. . . . . . . . . . . . 13 |- ( ( -. x = A /\ -. x = B ) -> -. x e. { A , B } )
19	13, 18	syl 16	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> -. x e. { A , B } )
20		simpllr 758	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> x e. ( A [,] B ) )
21		cncfiooicclem1.a	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A e. RR )
22	21	rexrd 9655	. . . . . . . . . . . . . . . . . 18 |- ( ph -> A e. RR* )
23	10, 22	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> A e. RR* )
24		cncfiooicclem1.b	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> B e. RR )
25	24	rexrd 9655	. . . . . . . . . . . . . . . . . 18 |- ( ph -> B e. RR* )
26	10, 25	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> B e. RR* )
27		cncfiooicclem1.altb	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A < B )
28	22, 25	jca 532	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( A e. RR* /\ B e. RR* ) )
29		xrltle 11367	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A e. RR* /\ B e. RR* ) -> ( A < B -> A <_ B ) )
30	28, 29	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( A < B -> A <_ B ) )
31	27, 30	mpd 15	. . . . . . . . . . . . . . . . . 18 |- ( ph -> A <_ B )
32	10, 31	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> A <_ B )
33	23, 26, 32	3jca 1176	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( A e. RR* /\ B e. RR* /\ A <_ B ) )
34		prunioo 11661	. . . . . . . . . . . . . . . 16 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
35	33, 34	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
36	35	eqcomd 2475	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( A [,] B ) = ( ( A (,) B ) u. { A , B } ) )
37	20, 36	eleqtrd 2557	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> x e. ( ( A (,) B ) u. { A , B } ) )
38		elun 3650	. . . . . . . . . . . . 13 |- ( x e. ( ( A (,) B ) u. { A , B } ) <-> ( x e. ( A (,) B ) \/ x e. { A , B } ) )
39	37, 38	sylib 196	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( x e. ( A (,) B ) \/ x e. { A , B } ) )
40		orel2 383	. . . . . . . . . . . 12 |- ( -. x e. { A , B } -> ( ( x e. ( A (,) B ) \/ x e. { A , B } ) -> x e. ( A (,) B ) ) )
41	19, 39, 40	sylc 60	. . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> x e. ( A (,) B ) )
42	10, 41	jca 532	. . . . . . . . . 10 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( ph /\ x e. ( A (,) B ) ) )
43		cncfiooicclem1.f	. . . . . . . . . . . 12 |- ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
44		cncff 21265	. . . . . . . . . . . 12 |- ( F e. ( ( A (,) B ) -cn-> CC ) -> F : ( A (,) B ) --> CC )
45	43, 44	syl 16	. . . . . . . . . . 11 |- ( ph -> F : ( A (,) B ) --> CC )
46	45	ffvelrnda 6032	. . . . . . . . . 10 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( F ` x ) e. CC )
47	42, 46	syl 16	. . . . . . . . 9 |- ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( F ` x ) e. CC )
48	9, 47	ifclda 3977	. . . . . . . 8 |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> if ( x = B , L , ( F ` x ) ) e. CC )
49	5, 48	ifclda 3977	. . . . . . 7 |- ( ( ph /\ x e. ( A [,] B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC )
50	49	ex 434	. . . . . 6 |- ( ph -> ( x e. ( A [,] B ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC ) )
51	1, 50	ralrimi 2867	. . . . 5 |- ( ph -> A. x e. ( A [,] B ) if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC )
52		cncfiooicclem1.g	. . . . . 6 |- G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
53	52	fmpt 6053	. . . . 5 |- ( A. x e. ( A [,] B ) if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC <-> G : ( A [,] B ) --> CC )
54	51, 53	sylib 196	. . . 4 |- ( ph -> G : ( A [,] B ) --> CC )
55		simpl 457	. . . . . . 7 |- ( ( ph /\ y e. ( A [,] B ) ) -> ph )
56		elun 3650	. . . . . . . . . 10 |- ( y e. ( ( A (,) B ) u. { A , B } ) <-> ( y e. ( A (,) B ) \/ y e. { A , B } ) )
57	22, 25, 31	3jca 1176	. . . . . . . . . . . 12 |- ( ph -> ( A e. RR* /\ B e. RR* /\ A <_ B ) )
58	57, 34	syl 16	. . . . . . . . . . 11 |- ( ph -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
59	58	eleq2d 2537	. . . . . . . . . 10 |- ( ph -> ( y e. ( ( A (,) B ) u. { A , B } ) <-> y e. ( A [,] B ) ) )
60	56, 59	syl5bbr 259	. . . . . . . . 9 |- ( ph -> ( ( y e. ( A (,) B ) \/ y e. { A , B } ) <-> y e. ( A [,] B ) ) )
61	60	biimprd 223	. . . . . . . 8 |- ( ph -> ( y e. ( A [,] B ) -> ( y e. ( A (,) B ) \/ y e. { A , B } ) ) )
62	61	imp 429	. . . . . . 7 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( y e. ( A (,) B ) \/ y e. { A , B } ) )
63	55, 62	jca 532	. . . . . 6 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( ph /\ ( y e. ( A (,) B ) \/ y e. { A , B } ) ) )
64		ioossicc 11622	. . . . . . . . . . . . . . . . . 18 |- ( A (,) B ) C_ ( A [,] B )
65	64	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( A (,) B ) C_ ( A [,] B ) )
66	54, 65	jca 532	. . . . . . . . . . . . . . . 16 |- ( ph -> ( G : ( A [,] B ) --> CC /\ ( A (,) B ) C_ ( A [,] B ) ) )
67		fssres 5757	. . . . . . . . . . . . . . . 16 |- ( ( G : ( A [,] B ) --> CC /\ ( A (,) B ) C_ ( A [,] B ) ) -> ( G |` ( A (,) B ) ) : ( A (,) B ) --> CC )
68	66, 67	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> ( G |` ( A (,) B ) ) : ( A (,) B ) --> CC )
69	68	feqmptd 5927	. . . . . . . . . . . . . 14 |- ( ph -> ( G |` ( A (,) B ) ) = ( y e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` y ) ) )
70		nfmpt1 4542	. . . . . . . . . . . . . . . . . . 19 |- F/_ x ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
71	52, 70	nfcxfr 2627	. . . . . . . . . . . . . . . . . 18 |- F/_ x G
72		nfcv 2629	. . . . . . . . . . . . . . . . . 18 |- F/_ x ( A (,) B )
73	71, 72	nfres 5281	. . . . . . . . . . . . . . . . 17 |- F/_ x ( G |` ( A (,) B ) )
74		nfcv 2629	. . . . . . . . . . . . . . . . 17 |- F/_ x y
75	73, 74	nffv 5879	. . . . . . . . . . . . . . . 16 |- F/_ x ( ( G |` ( A (,) B ) ) ` y )
76		nfcv 2629	. . . . . . . . . . . . . . . . 17 |- F/_ y ( G |` ( A (,) B ) )
77		nfcv 2629	. . . . . . . . . . . . . . . . 17 |- F/_ y x
78	76, 77	nffv 5879	. . . . . . . . . . . . . . . 16 |- F/_ y ( ( G |` ( A (,) B ) ) ` x )
79		fveq2 5872	. . . . . . . . . . . . . . . 16 |- ( y = x -> ( ( G |` ( A (,) B ) ) ` y ) = ( ( G |` ( A (,) B ) ) ` x ) )
80	75, 78, 79	cbvmpt 4543	. . . . . . . . . . . . . . 15 |- ( y e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` y ) ) = ( x e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` x ) )
81	80	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> ( y e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` y ) ) = ( x e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` x ) ) )
82		simpr 461	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( A (,) B ) )
83		fvres 5886	. . . . . . . . . . . . . . . . 17 |- ( x e. ( A (,) B ) -> ( ( G |` ( A (,) B ) ) ` x ) = ( G ` x ) )
84	82, 83	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( G |` ( A (,) B ) ) ` x ) = ( G ` x ) )
85	64, 82	sseldi 3507	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( A [,] B ) )
86	4	idi 2	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> R e. CC )
87	86	adantr 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( A (,) B ) ) -> R e. CC )
88	8	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x = B ) -> L e. CC )
89	88	adantlr 714	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ x e. ( A (,) B ) ) /\ x = B ) -> L e. CC )
90	45	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ x e. ( A (,) B ) ) -> F : ( A (,) B ) --> CC )
91	90, 82	ffvelrnd 6033	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( F ` x ) e. CC )
92	91	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ x e. ( A (,) B ) ) /\ -. x = B ) -> ( F ` x ) e. CC )
93	89, 92	ifclda 3977	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = B , L , ( F ` x ) ) e. CC )
94	87, 93	jca 532	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( R e. CC /\ if ( x = B , L , ( F ` x ) ) e. CC ) )
95		ifcl 3987	. . . . . . . . . . . . . . . . . . 19 |- ( ( R e. CC /\ if ( x = B , L , ( F ` x ) ) e. CC ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC )
96	94, 95	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC )
97	85, 96	jca 532	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( x e. ( A [,] B ) /\ if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC ) )
98	52	fvmpt2 5964	. . . . . . . . . . . . . . . . 17 |- ( ( 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 ) ) ) )
99	97, 98	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( G ` x ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
100		elioo4g 11597	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x e. ( A (,) B ) <-> ( ( A e. RR* /\ B e. RR* /\ x e. RR ) /\ ( A < x /\ x < B ) ) )
101	100	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x e. ( A (,) B ) -> ( ( A e. RR* /\ B e. RR* /\ x e. RR ) /\ ( A < x /\ x < B ) ) )
102	101	simpld 459	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. ( A (,) B ) -> ( A e. RR* /\ B e. RR* /\ x e. RR ) )
103	102	simp1d 1008	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. ( A (,) B ) -> A e. RR* )
104	102	simp3d 1010	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. ( A (,) B ) -> x e. RR )
105	104	rexrd 9655	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. ( A (,) B ) -> x e. RR* )
106	101	simprd 463	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. ( A (,) B ) -> ( A < x /\ x < B ) )
107	106	simpld 459	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. ( A (,) B ) -> A < x )
108	103, 105, 107	3jca 1176	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. ( A (,) B ) -> ( A e. RR* /\ x e. RR* /\ A < x ) )
109		xrltne 11378	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A e. RR* /\ x e. RR* /\ A < x ) -> x =/= A )
110	108, 109	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( A (,) B ) -> x =/= A )
111	110	adantl 466	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( A (,) B ) ) -> x =/= A )
112	111	neneqd 2669	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( A (,) B ) ) -> -. x = A )
113		iffalse 3954	. . . . . . . . . . . . . . . . . 18 |- ( -. x = A -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
114	112, 113	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
115	102	simp2d 1009	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. ( A (,) B ) -> B e. RR* )
116	106	simprd 463	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. ( A (,) B ) -> x < B )
117	105, 115, 116	3jca 1176	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. ( A (,) B ) -> ( x e. RR* /\ B e. RR* /\ x < B ) )
118		xrltne 11378	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( x e. RR* /\ B e. RR* /\ x < B ) -> B =/= x )
119	117, 118	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. ( A (,) B ) -> B =/= x )
120	119	necomd 2738	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( A (,) B ) -> x =/= B )
121	120	neneqd 2669	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( A (,) B ) -> -. x = B )
122		iffalse 3954	. . . . . . . . . . . . . . . . . . 19 |- ( -. x = B -> if ( x = B , L , ( F ` x ) ) = ( F ` x ) )
123	121, 122	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( A (,) B ) -> if ( x = B , L , ( F ` x ) ) = ( F ` x ) )
124	123	adantl 466	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = B , L , ( F ` x ) ) = ( F ` x ) )
125	114, 124	eqtrd 2508	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = ( F ` x ) )
126	84, 99, 125	3eqtrd 2512	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( A (,) B ) ) -> ( ( G |` ( A (,) B ) ) ` x ) = ( F ` x ) )
127	1, 126	mpteq2da 4538	. . . . . . . . . . . . . 14 |- ( ph -> ( x e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` x ) ) = ( x e. ( A (,) B ) |-> ( F ` x ) ) )
128	69, 81, 127	3eqtrd 2512	. . . . . . . . . . . . 13 |- ( ph -> ( G |` ( A (,) B ) ) = ( x e. ( A (,) B ) |-> ( F ` x ) ) )
129		ffn 5737	. . . . . . . . . . . . . . . . . 18 |- ( F : ( A (,) B ) --> CC -> F Fn ( A (,) B ) )
130	45, 129	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> F Fn ( A (,) B ) )
131		dffn5 5919	. . . . . . . . . . . . . . . . 17 |- ( F Fn ( A (,) B ) <-> F = ( x e. ( A (,) B ) |-> ( F ` x ) ) )
132	130, 131	sylib 196	. . . . . . . . . . . . . . . 16 |- ( ph -> F = ( x e. ( A (,) B ) |-> ( F ` x ) ) )
133	132	eqcomd 2475	. . . . . . . . . . . . . . 15 |- ( ph -> ( x e. ( A (,) B ) |-> ( F ` x ) ) = F )
134	133, 43	eqeltrd 2555	. . . . . . . . . . . . . 14 |- ( ph -> ( x e. ( A (,) B ) |-> ( F ` x ) ) e. ( ( A (,) B ) -cn-> CC ) )
135		ioossre 11598	. . . . . . . . . . . . . . . . 17 |- ( A (,) B ) C_ RR
136		ax-resscn 9561	. . . . . . . . . . . . . . . . 17 |- RR C_ CC
137	135, 136	sstri 3518	. . . . . . . . . . . . . . . 16 |- ( A (,) B ) C_ CC
138	137	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> ( A (,) B ) C_ CC )
139		ssid 3528	. . . . . . . . . . . . . . . 16 |- CC C_ CC
140	139	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> CC C_ CC )
141		eqid 2467	. . . . . . . . . . . . . . . 16 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
142		eqid 2467	. . . . . . . . . . . . . . . 16 |- ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) )
143	141	cnfldtop 21159	. . . . . . . . . . . . . . . . . 18 |- ( TopOpen ` ℂfld ) e. Top
144		unicntop 31336	. . . . . . . . . . . . . . . . . . 19 |- CC = U. ( TopOpen ` ℂfld )
145	144	restid 14706	. . . . . . . . . . . . . . . . . 18 |- ( ( TopOpen ` ℂfld ) e. Top -> ( ( TopOpen ` ℂfld ) ↾t CC ) = ( TopOpen ` ℂfld ) )
146	143, 145	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( ( TopOpen ` ℂfld ) ↾t CC ) = ( TopOpen ` ℂfld )
147	146	eqcomi 2480	. . . . . . . . . . . . . . . 16 |- ( TopOpen ` ℂfld ) = ( ( TopOpen ` ℂfld ) ↾t CC )
148	141, 142, 147	cncfcn 21281	. . . . . . . . . . . . . . 15 |- ( ( ( A (,) B ) C_ CC /\ CC C_ CC ) -> ( ( A (,) B ) -cn-> CC ) = ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
149	138, 140, 148	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ph -> ( ( A (,) B ) -cn-> CC ) = ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
150	134, 149	eleqtrd 2557	. . . . . . . . . . . . 13 |- ( ph -> ( x e. ( A (,) B ) |-> ( F ` x ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
151	128, 150	eqeltrd 2555	. . . . . . . . . . . 12 |- ( ph -> ( G |` ( A (,) B ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
152	151	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( G |` ( A (,) B ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
153		simpr 461	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( A (,) B ) )
154	152, 153	jca 532	. . . . . . . . . 10 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( G |` ( A (,) B ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) /\ y e. ( A (,) B ) ) )
155	143, 137	pm3.2i 455	. . . . . . . . . . . 12 |- ( ( TopOpen ` ℂfld ) e. Top /\ ( A (,) B ) C_ CC )
156	141	cnfldtopon 21158	. . . . . . . . . . . . . 14 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
157	156	toponunii 19302	. . . . . . . . . . . . 13 |- CC = U. ( TopOpen ` ℂfld )
158	157	restuni 19531	. . . . . . . . . . . 12 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ ( A (,) B ) C_ CC ) -> ( A (,) B ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) )
159	155, 158	ax-mp 5	. . . . . . . . . . 11 |- ( A (,) B ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) )
160	159	cncnpi 19647	. . . . . . . . . 10 |- ( ( ( 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 ) )
161	154, 160	syl 16	. . . . . . . . 9 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( G |` ( A (,) B ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
162	143	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( TopOpen ` ℂfld ) e. Top )
163	64	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( A (,) B ) C_ ( A [,] B ) )
164		ovex 6320	. . . . . . . . . . . . . . 15 |- ( A [,] B ) e. _V
165	164	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( A [,] B ) e. _V )
166	162, 163, 165	3jca 1176	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( TopOpen ` ℂfld ) e. Top /\ ( A (,) B ) C_ ( A [,] B ) /\ ( A [,] B ) e. _V ) )
167		restabs 19534	. . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
168	166, 167	syl 16	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) )
169	168	eqcomd 2475	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) = ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) )
170	169	oveq1d 6310	. . . . . . . . . 10 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) )
171	170	fveq1d 5874	. . . . . . . . 9 |- ( ( 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 ) )
172	161, 171	eleqtrd 2557	. . . . . . . 8 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( G |` ( A (,) B ) ) e. ( ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
173	143, 164	pm3.2i 455	. . . . . . . . . . . 12 |- ( ( TopOpen ` ℂfld ) e. Top /\ ( A [,] B ) e. _V )
174		resttop 19529	. . . . . . . . . . . 12 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ ( A [,] B ) e. _V ) -> ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) e. Top )
175	173, 174	ax-mp 5	. . . . . . . . . . 11 |- ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) e. Top
176	175	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) e. Top )
177	143	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> ( TopOpen ` ℂfld ) e. Top )
178	21, 24	jca 532	. . . . . . . . . . . . . . . 16 |- ( ph -> ( A e. RR /\ B e. RR ) )
179		iccssre 11618	. . . . . . . . . . . . . . . 16 |- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
180	178, 179	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> ( A [,] B ) C_ RR )
181	136	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> RR C_ CC )
182	180, 181	sstrd 3519	. . . . . . . . . . . . . 14 |- ( ph -> ( A [,] B ) C_ CC )
183	177, 182	jca 532	. . . . . . . . . . . . 13 |- ( ph -> ( ( TopOpen ` ℂfld ) e. Top /\ ( A [,] B ) C_ CC ) )
184	157	restuni 19531	. . . . . . . . . . . . 13 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ ( A [,] B ) C_ CC ) -> ( A [,] B ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
185	183, 184	syl 16	. . . . . . . . . . . 12 |- ( ph -> ( A [,] B ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
186	65, 185	sseqtrd 3545	. . . . . . . . . . 11 |- ( ph -> ( A (,) B ) C_ U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
187	186	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( A (,) B ) C_ U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
188		retop 21136	. . . . . . . . . . . . . . . . . . 19 |- ( topGen ` ran (,) ) e. Top
189	188	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( topGen ` ran (,) ) e. Top )
190		difss 3636	. . . . . . . . . . . . . . . . . . . . 21 |- ( RR \ ( A [,] B ) ) C_ RR
191	135, 190	pm3.2i 455	. . . . . . . . . . . . . . . . . . . 20 |- ( ( A (,) B ) C_ RR /\ ( RR \ ( A [,] B ) ) C_ RR )
192		unss 3683	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( A (,) B ) C_ RR /\ ( RR \ ( A [,] B ) ) C_ RR ) <-> ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) C_ RR )
193	191, 192	mpbi 208	. . . . . . . . . . . . . . . . . . 19 |- ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) C_ RR
194	193	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) C_ RR )
195		ssun1 3672	. . . . . . . . . . . . . . . . . . 19 |- ( A (,) B ) C_ ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) )
196	195	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( A (,) B ) C_ ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) )
197	189, 194, 196	3jca 1176	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( topGen ` ran (,) ) e. Top /\ ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) C_ RR /\ ( A (,) B ) C_ ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
198		uniretop 21137	. . . . . . . . . . . . . . . . . 18 |- RR = U. ( topGen ` ran (,) )
199	198	ntrss 19424	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) ) ) ) )
200	197, 199	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) C_ ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
201		isopn3i 19451	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( topGen ` ran (,) ) e. Top /\ ( A (,) B ) e. ( topGen ` ran (,) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B ) )
202		iooretop 21141	. . . . . . . . . . . . . . . . . . . . 21 |- ( A (,) B ) e. ( topGen ` ran (,) )
203	188	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( topGen ` ran (,) ) e. Top /\ ( A (,) B ) e. ( topGen ` ran (,) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B ) ) /\ ( A (,) B ) e. ( topGen ` ran (,) ) ) -> ( topGen ` ran (,) ) e. Top )
204	202	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( topGen ` ran (,) ) e. Top /\ ( A (,) B ) e. ( topGen ` ran (,) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B ) ) /\ ( A (,) B ) e. ( topGen ` ran (,) ) ) -> ( A (,) B ) e. ( topGen ` ran (,) ) )
205	203, 204	jca 532	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( topGen ` ran (,) ) e. Top /\ ( A (,) B ) e. ( topGen ` ran (,) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B ) ) /\ ( A (,) B ) e. ( topGen ` ran (,) ) ) -> ( ( topGen ` ran (,) ) e. Top /\ ( A (,) B ) e. ( topGen ` ran (,) ) ) )
206	205, 201	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( topGen ` ran (,) ) e. Top /\ ( A (,) B ) e. ( topGen ` ran (,) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B ) ) /\ ( A (,) B ) e. ( topGen ` ran (,) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B ) )
207	201, 202, 206	mp2an 672	. . . . . . . . . . . . . . . . . . . 20 |- ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B )
208	207	eqcomi 2480	. . . . . . . . . . . . . . . . . . 19 |- ( A (,) B ) = ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) )
209	208	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( A (,) B ) = ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) )
210	209	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( A (,) B ) = ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) )
211	153, 210	eleqtrd 2557	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) )
212	200, 211	sseldd 3510	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
213	64, 153	sseldi 3507	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( A [,] B ) )
214	212, 213	jca 532	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( y e. ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) /\ y e. ( A [,] B ) ) )
215		elin 3692	. . . . . . . . . . . . . 14 |- ( y e. ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) i^i ( A [,] B ) ) <-> ( y e. ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) /\ y e. ( A [,] B ) ) )
216	214, 215	sylibr 212	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) i^i ( A [,] B ) ) )
217	180	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( A [,] B ) C_ RR )
218	189, 217, 163	3jca 1176	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( topGen ` ran (,) ) e. Top /\ ( A [,] B ) C_ RR /\ ( A (,) B ) C_ ( A [,] B ) ) )
219		eqid 2467	. . . . . . . . . . . . . . . 16 |- ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) = ( ( topGen ` ran (,) ) ↾t ( A [,] B ) )
220	198, 219	restntr 19551	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) ) )
221	218, 220	syl 16	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) )
222	221	eqcomd 2475	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) i^i ( A [,] B ) ) = ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) )
223	216, 222	eleqtrd 2557	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) )
224	141	tgioo2 21176	. . . . . . . . . . . . . . . . . 18 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
225	224	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR ) )
226	225	oveq1d 6310	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) = ( ( ( TopOpen ` ℂfld ) ↾t RR ) ↾t ( A [,] B ) ) )
227		reex 9595	. . . . . . . . . . . . . . . . . . 19 |- RR e. _V
228	227	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ph -> RR e. _V )
229	177, 180, 228	3jca 1176	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( TopOpen ` ℂfld ) e. Top /\ ( A [,] B ) C_ RR /\ RR e. _V ) )
230		restabs 19534	. . . . . . . . . . . . . . . . 17 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ ( A [,] B ) C_ RR /\ RR e. _V ) -> ( ( ( TopOpen ` ℂfld ) ↾t RR ) ↾t ( A [,] B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
231	229, 230	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( TopOpen ` ℂfld ) ↾t RR ) ↾t ( A [,] B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
232	226, 231	eqtrd 2508	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) )
233	232	fveq2d 5876	. . . . . . . . . . . . . 14 |- ( ph -> ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) = ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) )
234	233	fveq1d 5874	. . . . . . . . . . . . 13 |- ( ph -> ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) = ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) )
235	234	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) = ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) )
236	223, 235	eleqtrd 2557	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) )
237	185	feq2d 5724	. . . . . . . . . . . . 13 |- ( ph -> ( G : ( A [,] B ) --> CC <-> G : U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) --> CC ) )
238	54, 237	mpbid 210	. . . . . . . . . . . 12 |- ( ph -> G : U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) --> CC )
239	238	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( A (,) B ) ) -> G : U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) --> CC )
240	236, 239	jca 532	. . . . . . . . . 10 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( y e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) ` ( A (,) B ) ) /\ G : U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) --> CC ) )
241	176, 187, 240	jca31 534	. . . . . . . . 9 |- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( ( ( 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 ) ) )
242		eqid 2467	. . . . . . . . . 10 |- U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) = U. ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) )
243	242, 157	cnprest 19658	. . . . . . . . 9 |- ( ( ( ( ( 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 ) ) )
244	241, 243	syl 16	. . . . . . . 8 |- ( ( 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 ) ) )
245	172, 244	mpbird 232	. . . . . . 7 |- ( ( ph /\ y e. ( A (,) B ) ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
246		elpri 4053	. . . . . . . . . 10 |- ( y e. { A , B } -> ( y = A \/ y = B ) )
247	246	a1i 11	. . . . . . . . 9 |- ( ph -> ( y e. { A , B } -> ( y = A \/ y = B ) ) )
248	247	imdistani 690	. . . . . . . 8 |- ( ( ph /\ y e. { A , B } ) -> ( ph /\ ( y = A \/ y = B ) ) )
249		lbicc2 11648	. . . . . . . . . . . . . . . . . 18 |- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
250	57, 249	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> A e. ( A [,] B ) )
251	250, 3	jca 532	. . . . . . . . . . . . . . . 16 |- ( ph -> ( A e. ( A [,] B ) /\ R e. ( F lim CC A ) ) )
252		iftrue 3951	. . . . . . . . . . . . . . . . 17 |- ( x = A -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = R )
253	52	idi 2	. . . . . . . . . . . . . . . . 17 |- G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
254	252, 253	fvmptg 5955	. . . . . . . . . . . . . . . 16 |- ( ( A e. ( A [,] B ) /\ R e. ( F lim CC A ) ) -> ( G ` A ) = R )
255	251, 254	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> ( G ` A ) = R )
256	128, 133	eqtr2d 2509	. . . . . . . . . . . . . . . . . 18 |- ( ph -> F = ( G |` ( A (,) B ) ) )
257	256	oveq1d 6310	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( F lim CC A ) = ( ( G |` ( A (,) B ) ) lim CC A ) )
258	3, 257	eleqtrd 2557	. . . . . . . . . . . . . . . 16 |- ( ph -> R e. ( ( G |` ( A (,) B ) ) lim CC A ) )
259		eqid 2467	. . . . . . . . . . . . . . . . 17 |- ( ( TopOpen ` ℂfld ) ↾t ( ( A [,] B ) u. { A } ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( A [,] B ) u. { A } ) )
260		mnfxr 11335	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- -oo e. RR*
261	260	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> -oo e. RR* )
262	261, 25, 22	3jca 1176	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( -oo e. RR* /\ B e. RR* /\ A e. RR* ) )
263		mnflt 11345	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( A e. RR -> -oo < A )
264	21, 263	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> -oo < A )
265	264, 27	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( -oo < A /\ A < B ) )
266	262, 265	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( -oo e. RR* /\ B e. RR* /\ A e. RR* ) /\ ( -oo < A /\ A < B ) ) )
267		elioo3g 11570	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A e. ( -oo (,) B ) <-> ( ( -oo e. RR* /\ B e. RR* /\ A e. RR* ) /\ ( -oo < A /\ A < B ) ) )
268	266, 267	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> A e. ( -oo (,) B ) )
269	188	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> ( topGen ` ran (,) ) e. Top )
270		iooretop 21141	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( -oo (,) B ) e. ( topGen ` ran (,) )
271	270	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> ( -oo (,) B ) e. ( topGen ` ran (,) ) )
272	269, 271	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( ( topGen ` ran (,) ) e. Top /\ ( -oo (,) B ) e. ( topGen ` ran (,) ) ) )
273		isopn3i 19451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( topGen ` ran (,) ) e. Top /\ ( -oo (,) B ) e. ( topGen ` ran (,) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( -oo (,) B ) ) = ( -oo (,) B ) )
274	272, 273	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( -oo (,) B ) ) = ( -oo (,) B ) )
275	274	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( -oo (,) B ) = ( ( int ` ( topGen ` ran (,) ) ) ` ( -oo (,) B ) ) )
276	268, 275	eleqtrd 2557	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> A e. ( ( int ` ( topGen ` ran (,) ) ) ` ( -oo (,) B ) ) )
277	21, 25	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ph -> ( A e. RR /\ B e. RR* ) )
278		icossre 11617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( A e. RR /\ B e. RR* ) -> ( A [,) B ) C_ RR )
279	277, 278	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( A [,) B ) C_ RR )
280	190	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( RR \ ( A [,] B ) ) C_ RR )
281	279, 280	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> ( ( A [,) B ) C_ RR /\ ( RR \ ( A [,] B ) ) C_ RR ) )
282		unss 3683	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( A [,) B ) C_ RR /\ ( RR \ ( A [,] B ) ) C_ RR ) <-> ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) C_ RR )
283	281, 282	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) C_ RR )
284		elioore 11571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( x e. ( -oo (,) B ) -> x e. RR )
285	284	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ x < A ) -> x e. RR )
286	21, 284	anim12ci 567	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ph /\ x e. ( -oo (,) B ) ) -> ( x e. RR /\ A e. RR ) )
287	286	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ x < A ) -> ( x e. RR /\ A e. RR ) )
288	287	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ x < A ) -> A e. RR )
289	28	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ x < A ) -> ( A e. RR* /\ B e. RR* ) )
290	289	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ x < A ) -> B e. RR* )
291	285	rexrd 9655	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ x < A ) -> x e. RR* )
292		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ x < A ) -> x < A )
293	288, 290, 291, 292	ltnelicc 31417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ x < A ) -> -. x e. ( A [,] B ) )
294	285, 293	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ x < A ) -> ( x e. RR /\ -. x e. ( A [,] B ) ) )
295		eldif 3491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( x e. ( RR \ ( A [,] B ) ) <-> ( x e. RR /\ -. x e. ( A [,] B ) ) )
296	294, 295	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ x < A ) -> x e. ( RR \ ( A [,] B ) ) )
297	296	olcd 393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ x < A ) -> ( x e. ( A [,) B ) \/ x e. ( RR \ ( A [,] B ) ) ) )
298	284	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. x < A ) -> x e. RR )
299		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. x < A ) -> -. x < A )
300	286	ancomd 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ph /\ x e. ( -oo (,) B ) ) -> ( A e. RR /\ x e. RR ) )
301	300	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. x < A ) -> ( A e. RR /\ x e. RR ) )
302		lenlt 9675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( A e. RR /\ x e. RR ) -> ( A <_ x <-> -. x < A ) )
303	301, 302	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. x < A ) -> ( A <_ x <-> -. x < A ) )
304	299, 303	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. x < A ) -> A <_ x )
305		elioo3g 11570	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( x e. ( -oo (,) B ) <-> ( ( -oo e. RR* /\ B e. RR* /\ x e. RR* ) /\ ( -oo < x /\ x < B ) ) )
306	305	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( x e. ( -oo (,) B ) -> ( ( -oo e. RR* /\ B e. RR* /\ x e. RR* ) /\ ( -oo < x /\ x < B ) ) )
307	306	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( x e. ( -oo (,) B ) -> ( -oo < x /\ x < B ) )
308	307	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( x e. ( -oo (,) B ) -> x < B )
309	308	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. x < A ) -> x < B )
310	298, 304, 309	3jca 1176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. x < A ) -> ( x e. RR /\ A <_ x /\ x < B ) )
311	277	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. x < A ) -> ( A e. RR /\ B e. RR* ) )
312		elico2 11600	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( A e. RR /\ B e. RR* ) -> ( x e. ( A [,) B ) <-> ( x e. RR /\ A <_ x /\ x < B ) ) )
313	311, 312	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. x < A ) -> ( x e. ( A [,) B ) <-> ( x e. RR /\ A <_ x /\ x < B ) ) )
314	310, 313	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. x < A ) -> x e. ( A [,) B ) )
315	314	orcd 392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ph /\ x e. ( -oo (,) B ) ) /\ -. x < A ) -> ( x e. ( A [,) B ) \/ x e. ( RR \ ( A [,] B ) ) ) )
316	297, 315	pm2.61dan 789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ x e. ( -oo (,) B ) ) -> ( x e. ( A [,) B ) \/ x e. ( RR \ ( A [,] B ) ) ) )
317		elun 3650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( x e. ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) <-> ( x e. ( A [,) B ) \/ x e. ( RR \ ( A [,] B ) ) ) )
318	316, 317	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ x e. ( -oo (,) B ) ) -> x e. ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) )
319	318	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( x e. ( -oo (,) B ) -> x e. ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
320	1, 319	ralrimi 2867	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> A. x e. ( -oo (,) B ) x e. ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) )
321		dfss3 3499	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( -oo (,) B ) C_ ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) <-> A. x e. ( -oo (,) B ) x e. ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) )
322	320, 321	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( -oo (,) B ) C_ ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) )
323	269, 283, 322	3jca 1176	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( topGen ` ran (,) ) e. Top /\ ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) C_ RR /\ ( -oo (,) B ) C_ ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
324	198	ntrss 19424	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( topGen ` ran (,) ) e. Top /\ ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) C_ RR /\ ( -oo (,) B ) C_ ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( -oo (,) B ) ) C_ ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
325	323, 324	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( -oo (,) B ) ) C_ ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
326	325	sseld 3508	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( A e. ( ( int ` ( topGen ` ran (,) ) ) ` ( -oo (,) B ) ) -> A e. ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) ) )
327	276, 326	mpd 15	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> A e. ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
328	327, 250	jca 532	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( A e. ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) /\ A e. ( A [,] B ) ) )
329		elin 3692	. . . . . . . . . . . . . . . . . . . . 21 |- ( A e. ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) i^i ( A [,] B ) ) <-> ( A e. ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) /\ A e. ( A [,] B ) ) )
330	328, 329	sylibr 212	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> A e. ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) i^i ( A [,] B ) ) )
331		icossicc 11623	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A [,) B ) C_ ( A [,] B )
332	331	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( A e. RR* /\ B e. RR* ) -> ( A [,) B ) C_ ( A [,] B ) )
333	28, 332	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( A [,) B ) C_ ( A [,] B ) )
334	269, 180, 333	3jca 1176	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( ( topGen ` ran (,) ) e. Top /\ ( A [,] B ) C_ RR /\ ( A [,) B ) C_ ( A [,] B ) ) )
335	198, 219	restntr 19551	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( 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 ) ) )
336	334, 335	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A [,) B ) ) = ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) i^i ( A [,] B ) ) )
337	336	eqcomd 2475	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A [,) B ) u. ( RR \ ( A [,] B ) ) ) ) i^i ( A [,] B ) ) = ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A [,) B ) ) )
338	330, 337	eleqtrd 2557	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A e. ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A [,) B ) ) )
339	233	fveq1d 5874	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( int ` ( ( topGen ` ran (,) ) ↾t ( A [,] B ) ) ) ` ( A [,) B ) ) = ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) ` ( A [,) B ) ) )
340	338, 339	eleqtrd 2557	. . . . . . . . . . . . . . . . . 18 |- ( ph -> A e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) ` ( A [,) B ) ) )
341	250	snssd 4178	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> { A } C_ ( A [,] B ) )
342		ssequn2 3682	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( { A } C_ ( A [,] B ) <-> ( ( A [,] B ) u. { A } ) = ( A [,] B ) )
343	341, 342	sylib 196	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( ( A [,] B ) u. { A } ) = ( A [,] B ) )
344	343	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( A [,] B ) = ( ( A [,] B ) u. { A } ) )
345	344	oveq2d 6311	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( A [,] B ) u. { A } ) ) )
346	345	fveq2d 5876	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) = ( int ` ( ( TopOpen ` ℂfld ) ↾t ( ( A [,] B ) u. { A } ) ) ) )
347		uncom 3653	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( A (,) B ) u. { A } ) = ( { A } u. ( A (,) B ) )
348	22, 25, 27	3jca 1176	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( A e. RR* /\ B e. RR* /\ A < B ) )
349		snunioo 11658	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( { A } u. ( A (,) B ) ) = ( A [,) B ) )
350	348, 349	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( { A } u. ( A (,) B ) ) = ( A [,) B ) )
351	347, 350	syl5eq 2520	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( A (,) B ) u. { A } ) = ( A [,) B ) )
352	351	eqcomd 2475	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( A [,) B ) = ( ( A (,) B ) u. { A } ) )
353	346, 352	fveq12d 5878	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) ) ` ( A [,) B ) ) = ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( ( A [,] B ) u. { A } ) ) ) ` ( ( A (,) B ) u. { A } ) ) )
354	340, 353	eleqtrd 2557	. . . . . . . . . . . . . . . . 17 |- ( ph -> A e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t ( ( A [,] B ) u. { A } ) ) ) ` ( ( A (,) B ) u. { A } ) ) )
355	54, 65, 182, 141, 259, 354	limcres 22158	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( G |` ( A (,) B ) ) lim CC A ) = ( G lim CC A ) )
356	258, 355	eleqtrd 2557	. . . . . . . . . . . . . . 15 |- ( ph -> R e. ( G lim CC A ) )
357	255, 356	eqeltrd 2555	. . . . . . . . . . . . . 14 |- ( ph -> ( G ` A ) e. ( G lim CC A ) )
358	54, 357	jca 532	. . . . . . . . . . . . 13 |- ( ph -> ( G : ( A [,] B ) --> CC /\ ( G ` A ) e. ( G lim CC A ) ) )
359	182, 250	jca 532	. . . . . . . . . . . . . 14 |- ( ph -> ( ( A [,] B ) C_ CC /\ A e. ( A [,] B ) ) )
360		eqid 2467	. . . . . . . . . . . . . . 15 |- ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) )
361	141, 360	cnplimc 22159	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) ) )
362	359, 361	syl 16	. . . . . . . . . . . . 13 |- ( ph -> ( G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) <-> ( G : ( A [,] B ) --> CC /\ ( G ` A ) e. ( G lim CC A ) ) ) )
363	358, 362	mpbird 232	. . . . . . . . . . . 12 |- ( ph -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) )
364	363	idi 2	. . . . . . . . . . 11 |- ( ph -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) )
365	364	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ y = A ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) )
366		fveq2 5872	. . . . . . . . . . . 12 |- ( y = A -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) )
367	366	eqcomd 2475	. . . . . . . . . . 11 |- ( y = A -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
368	367	adantl 466	. . . . . . . . . 10 |- ( ( ph /\ y = A ) -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` A ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
369	365, 368	eleqtrd 2557	. . . . . . . . 9 |- ( ( ph /\ y = A ) -> G e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A [,] B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
370	24	leidd 10131	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> B <_ B )
371	24, 31, 370	3jca 1176	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( B e. RR /\ A <_ B /\ B <_ B ) )
372		elicc2 11601	. . . . . . . . . . . . . . . . . . 19 |- ( ( A e. RR /\ B e. RR ) -> ( B e. ( A [,] B ) <-> ( B e. RR /\ A <_ B /\ B <_ B ) ) )
373	178, 372	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( B e. ( A [,] B ) <-> ( B e. RR /\ A <_ B /\ B <_ B ) ) )
374	371, 373	mpbird 232	. . . . . . . . . . . . . . . . 17 |- ( ph -> B e. ( A [,] B ) )
375		eqid 2467	. . . . . . . . . . . . . . . . . . . . . 22 |- B = B
376		iftrue 3951	. . . . . . . . . . . . . . . . . . . . . 22 |- ( B = B -> if ( B = B , L , ( F ` B ) ) = L )
377	375, 376	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 |- if ( B = B , L , ( F ` B ) ) = L
378	377, 8	syl5eqel 2559	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> if ( B = B , L , ( F ` B ) ) e. CC )
379	4, 378	jca 532	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( R e. CC /\ if ( B = B , L , ( F ` B ) ) e. CC ) )
380		ifcl 3987	. . . . . . . . . . . . . . . . . . 19 |- ( ( R e. CC /\ if ( B = B , L , ( F ` B ) ) e. CC ) -> if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) e. CC )
381	379, 380	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) e. CC )
382	374, 381	jca 532	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( B e. ( A [,] B ) /\ if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) e. CC ) )
383		nfcv 2629	. . . . . . . . . . . . . . . . . 18 |- F/_ x B
384		nfv 1683	. . . . . . . . . . . . . . . . . . 19 |- F/ x ( B e. ( A [,] B ) /\ if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) e. CC )
385	71, 383	nffv 5879	. . . . . . . . . . . . . . . . . . . 20 |- F/_ x ( G ` B )
386		nfcv 2629	. . . . . . . . . . . . . . . . . . . 20 |- F/_ x if ( B = A , R , if ( B = B , L , ( F ` B ) ) )
387	385, 386	nfeq 2640	. . . . . . . . . . . . . . . . . . 19 |- F/ x ( G ` B ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) )
388	384, 387	nfim 1867	. . . . . . . . . . . . . . . . . 18 |- 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 ) ) ) )
389		eleq1 2539	. . . . . . . . . . . . . . . . . . . 20 |- ( x = B -> ( x e. ( A [,] B ) <-> B e. ( A [,] B ) ) )
390	252	adantl 466	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( x = B /\ x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = R )
391		eqtr2 2494	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( x = B /\ x = A ) -> B = A )
392		iftrue 3951	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( B = A -> if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) = R )
393	392	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( B = A -> R = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
394	391, 393	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( x = B /\ x = A ) -> R = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
395	390, 394	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( x = B /\ x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
396	113	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( x = B /\ -. x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
397		iftrue 3951	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x = B -> if ( x = B , L , ( F ` x ) ) = L )
398	397	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( x = B /\ -. x = A ) -> if ( x = B , L , ( F ` x ) ) = L )
399	396, 398	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( x = B /\ -. x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = L )
400		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( x = B /\ -. x = A ) -> x = B )
401		df-ne 2664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( x =/= A <-> -. x = A )
402	401	biimpri 206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( -. x = A -> x =/= A )
403	402	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( x = B /\ -. x = A ) -> x =/= A )
404	400, 403	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( x = B /\ -. x = A ) -> ( x = B /\ x =/= A ) )
405		pm13.18 2778	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( x = B /\ x =/= A ) -> B =/= A )
406	404, 405	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( x = B /\ -. x = A ) -> B =/= A )
407	406	neneqd 2669	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( x = B /\ -. x = A ) -> -. B = A )
408		iffalse 3954	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( -. B = A -> if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) = if ( B = B , L , ( F ` B ) ) )
409	407, 408	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( x = B /\ -. x = A ) -> if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) = if ( B = B , L , ( F ` B ) ) )
410	377	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( x = B /\ -. x = A ) -> if ( B = B , L , ( F ` B ) ) = L )
411	409, 410	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( x = B /\ -. x = A ) -> if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) = L )
412	411	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( x = B /\ -. x = A ) -> L = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
413	399, 412	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( x = B /\ -. x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
414	395, 413	pm2.61dan 789	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = B -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
415	414	eleq1d 2536	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 ) )
416	389, 415	anbi12d 710	. . . . . . . . . . . . . . . . . . 19 |- ( 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 ) ) )
417		fveq2 5872	. . . . . . . . . . . . . . . . . . . 20 |- ( x = B -> ( G ` x ) = ( G ` B ) )
418	417, 414	eqeq12d 2489	. . . . . . . . . . . . . . . . . . 19 |- ( 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 ) ) ) ) )
419	416, 418	imbi12d 320	. . . . . . . . . . . . . . . . . 18 |- ( 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 ) ) ) ) ) )
420	98	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( A [,] 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 ) ) ) ) )
421	383, 388, 419, 420	vtoclgaf 3181	. . . . . . . . . . . . . . . . 17 |- ( 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 ) ) ) ) )
422	374, 382, 421	sylc 60	. . . . . . . . . . . . . . . 16 |- ( ph -> ( G ` B ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
423	21, 27	ltned 9732	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A =/= B )
424	423	necomd 2738	. . . . . . . . . . . . . . . . . 18 |- ( ph -> B =/= A )
425	424	neneqd 2669	. . . . . . . . . . . . . . . . 17 |- ( ph -> -. B = A )
426	425, 408	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) = if ( B = B , L , ( F ` B ) ) )
427	377	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> if ( B = B , L , ( F ` B ) ) = L )
428	422, 426, 427	3eqtrd 2512	. . . . . . . . . . . . . . 15 |- ( ph -> ( G ` B ) = L )
429	256	oveq1d 6310	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( F lim CC B ) = ( ( G |` ( A (,) B ) ) lim CC B ) )
430	7, 429	eleqtrd 2557	. . . . . . . . . . . . . . . 16 |- ( ph -> L e. ( ( G |` ( A (,) B ) ) lim CC B ) )
431		eqid 2467	. . . . . . . . . . . . . . . . 17 |- ( ( TopOpen ` ℂfld ) ↾t ( ( A [,] B ) u. { B } ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( A [,] B ) u. { B } ) )
432		pnfxr 11333	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- +oo e. RR*
433	432	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> +oo e. RR* )
434	22, 433, 25	3jca 1176	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( A e. RR* /\ +oo e. RR* /\ B e. RR* ) )
435		ltpnf 11343	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( B e. RR -> B < +oo )
436	24, 435	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> B < +oo )
437	27, 436	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( A < B /\ B < +oo ) )
438	434, 437	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( A e. RR* /\ +oo e. RR* /\ B e. RR* ) /\ ( A < B /\ B < +oo ) ) )
439		elioo3g 11570	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( B e. ( A (,) +oo ) <-> ( ( A e. RR* /\ +oo e. RR* /\ B e. RR* ) /\ ( A < B /\ B < +oo ) ) )
440	438, 439	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> B e. ( A (,) +oo ) )
441		iooretop 21141	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( A (,) +oo ) e. ( topGen ` ran (,) )
442	441	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> ( A (,) +oo ) e. ( topGen ` ran (,) ) )
443	269, 442	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( ( topGen ` ran (,) ) e. Top /\ ( A (,) +oo ) e. ( topGen ` ran (,) ) ) )
444		isopn3i 19451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( topGen ` ran (,) ) e. Top /\ ( A (,) +oo ) e. ( topGen ` ran (,) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) +oo ) ) = ( A (,) +oo ) )
445	443, 444	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) +oo ) ) = ( A (,) +oo ) )
446	445	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( A (,) +oo ) = ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) +oo ) ) )
447	440, 446	eleqtrd 2557	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> B e. ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) +oo ) ) )
448	22, 24	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ph -> ( A e. RR* /\ B e. RR ) )
449		iocssre 11616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
450	448, 449	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( A (,] B ) C_ RR )
451	450, 280	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> ( ( A (,] B ) C_ RR /\ ( RR \ ( A [,] B ) ) C_ RR ) )
452		unss 3683	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( A (,] B ) C_ RR /\ ( RR \ ( A [,] B ) ) C_ RR ) <-> ( ( A (,] B ) u. ( RR \ ( A [,] B ) ) ) C_ RR )
453	451, 452	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( ( A (,] B ) u. ( RR \ ( A [,] B ) ) ) C_ RR )
454		elioore 11571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( x e. ( A (,) +oo ) -> x e. RR )
455	454	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ x <_ B ) -> x e. RR )
456		elioo3g 11570	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( x e. ( A (,) +oo ) <-> ( ( A e. RR* /\ +oo e. RR* /\ x e. RR* ) /\ ( A < x /\ x < +oo ) ) )
457	456	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( x e. ( A (,) +oo ) -> ( ( A e. RR* /\ +oo e. RR* /\ x e. RR* ) /\ ( A < x /\ x < +oo ) ) )
458	457	simprd 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( x e. ( A (,) +oo ) -> ( A < x /\ x < +oo ) )
459	458	simpld 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( x e. ( A (,) +oo ) -> A < x )
460	459	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ x <_ B ) -> A < x )
461		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ x <_ B ) -> x <_ B )
462	455, 460, 461	3jca 1176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ x <_ B ) -> ( x e. RR /\ A < x /\ x <_ B ) )
463	448	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ x <_ B ) -> ( A e. RR* /\ B e. RR ) )
464		elioc2 11599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( A e. RR* /\ B e. RR ) -> ( x e. ( A (,] B ) <-> ( x e. RR /\ A < x /\ x <_ B ) ) )
465	463, 464	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ x <_ B ) -> ( x e. ( A (,] B ) <-> ( x e. RR /\ A < x /\ x <_ B ) ) )
466	462, 465	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ x <_ B ) -> x e. ( A (,] B ) )
467		ssun1 3672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( A (,] B ) C_ ( ( A (,] B ) u. ( RR \ ( A [,] B ) ) )
468	467	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ x <_ B ) -> ( A (,] B ) C_ ( ( A (,] B ) u. ( RR \ ( A [,] B ) ) ) )
469	468	sseld 3508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ x <_ B ) -> ( x e. ( A (,] B ) -> x e. ( ( A (,] B ) u. ( RR \ ( A [,] B ) ) ) ) )
470	466, 469	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ x <_ B ) -> x e. ( ( A (,] B ) u. ( RR \ ( A [,] B ) ) ) )
471	454	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ -. x <_ B ) -> x e. RR )
472		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ -. x <_ B ) -> -. x <_ B )
473		simp3 998	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( x e. RR /\ A <_ x /\ x <_ B ) -> x <_ B )
474	472, 473	nsyl 121	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ -. x <_ B ) -> -. ( x e. RR /\ A <_ x /\ x <_ B ) )
475	178	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ -. x <_ B ) -> ( A e. RR /\ B e. RR ) )
476		elicc2 11601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( A e. RR /\ B e. RR ) -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
477	475, 476	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ -. x <_ B ) -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
478	474, 477	mtbird 301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ -. x <_ B ) -> -. x e. ( A [,] B ) )
479	471, 478	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ -. x <_ B ) -> ( x e. RR /\ -. x e. ( A [,] B ) ) )
480	479, 295	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ph /\ x e. ( A (,) +oo ) ) /\ -. x <_ B ) -> x e. ( RR \ ( A [,] B