Metamath Proof Explorer

Theorem cncfiooicclem1

Description: A continuous function F on an open interval ( A (,) B ) can be extended to a continuous function G on the corresponding closed interval, if it has a finite right limit R in A and a finite left limit L in B . F can be complex-valued. This lemma assumes A < B , the invoking theorem drops this assumption. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses 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 limCC B ) )
cncfiooicclem1.r 
|- ( ph -> R e. ( F limCC A ) )
Assertion cncfiooicclem1 
|- ( ph -> G e. ( ( A [,] B ) -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 cncfiooicclem1.x 
 |-  F/ x ph
2 cncfiooicclem1.g 
 |-  G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
3 cncfiooicclem1.a 
 |-  ( ph -> A e. RR )
4 cncfiooicclem1.b 
 |-  ( ph -> B e. RR )
5 cncfiooicclem1.altb 
 |-  ( ph -> A < B )
6 cncfiooicclem1.f 
 |-  ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
7 cncfiooicclem1.l 
 |-  ( ph -> L e. ( F limCC B ) )
8 cncfiooicclem1.r 
 |-  ( ph -> R e. ( F limCC A ) )
9 limccl 
 |-  ( F limCC A ) C_ CC
10 9 8 sselid 
 |-  ( ph -> R e. CC )
11 10 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ x = A ) -> R e. CC )
12 limccl 
 |-  ( F limCC B ) C_ CC
13 12 7 sselid 
 |-  ( ph -> L e. CC )
14 13 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ x = B ) -> L e. CC )
15 simplll 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ph )
16 orel1 
 |-  ( -. x = A -> ( ( x = A \/ x = B ) -> x = B ) )
17 16 con3dimp 
 |-  ( ( -. x = A /\ -. x = B ) -> -. ( x = A \/ x = B ) )
18 vex 
 |-  x e. _V
19 18 elpr 
 |-  ( x e. { A , B } <-> ( x = A \/ x = B ) )
20 17 19 sylnibr 
 |-  ( ( -. x = A /\ -. x = B ) -> -. x e. { A , B } )
21 20 adantll 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> -. x e. { A , B } )
22 simpllr 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> x e. ( A [,] B ) )
23 3 rexrd 
 |-  ( ph -> A e. RR* )
24 15 23 syl 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> A e. RR* )
25 4 rexrd 
 |-  ( ph -> B e. RR* )
26 15 25 syl 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> B e. RR* )
27 3 4 5 ltled 
 |-  ( ph -> A <_ B )
28 15 27 syl 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> A <_ B )
29 prunioo 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
30 24 26 28 29 syl3anc 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
31 22 30 eleqtrrd 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> x e. ( ( A (,) B ) u. { A , B } ) )
32 elun 
 |-  ( x e. ( ( A (,) B ) u. { A , B } ) <-> ( x e. ( A (,) B ) \/ x e. { A , B } ) )
33 31 32 sylib 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( x e. ( A (,) B ) \/ x e. { A , B } ) )
34 orel2 
 |-  ( -. x e. { A , B } -> ( ( x e. ( A (,) B ) \/ x e. { A , B } ) -> x e. ( A (,) B ) ) )
35 21 33 34 sylc 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> x e. ( A (,) B ) )
36 cncff 
 |-  ( F e. ( ( A (,) B ) -cn-> CC ) -> F : ( A (,) B ) --> CC )
37 6 36 syl 
 |-  ( ph -> F : ( A (,) B ) --> CC )
38 37 ffvelcdmda 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( F ` x ) e. CC )
39 15 35 38 syl2anc 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( F ` x ) e. CC )
40 14 39 ifclda 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> if ( x = B , L , ( F ` x ) ) e. CC )
41 11 40 ifclda 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC )
42 1 41 2 fmptdf 
 |-  ( ph -> G : ( A [,] B ) --> CC )
43 elun 
 |-  ( y e. ( ( A (,) B ) u. { A , B } ) <-> ( y e. ( A (,) B ) \/ y e. { A , B } ) )
44 23 25 27 29 syl3anc 
 |-  ( ph -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
45 44 eleq2d 
 |-  ( ph -> ( y e. ( ( A (,) B ) u. { A , B } ) <-> y e. ( A [,] B ) ) )
46 43 45 bitr3id 
 |-  ( ph -> ( ( y e. ( A (,) B ) \/ y e. { A , B } ) <-> y e. ( A [,] B ) ) )
47 46 biimpar 
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( y e. ( A (,) B ) \/ y e. { A , B } ) )
48 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
49 fssres 
 |-  ( ( G : ( A [,] B ) --> CC /\ ( A (,) B ) C_ ( A [,] B ) ) -> ( G |` ( A (,) B ) ) : ( A (,) B ) --> CC )
50 42 48 49 sylancl 
 |-  ( ph -> ( G |` ( A (,) B ) ) : ( A (,) B ) --> CC )
51 50 feqmptd 
 |-  ( ph -> ( G |` ( A (,) B ) ) = ( y e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` y ) ) )
52 nfmpt1 
 |-  F/_ x ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
53 2 52 nfcxfr 
 |-  F/_ x G
54 nfcv 
 |-  F/_ x ( A (,) B )
55 53 54 nfres 
 |-  F/_ x ( G |` ( A (,) B ) )
56 nfcv 
 |-  F/_ x y
57 55 56 nffv 
 |-  F/_ x ( ( G |` ( A (,) B ) ) ` y )
58 nfcv 
 |-  F/_ y ( G |` ( A (,) B ) )
59 nfcv 
 |-  F/_ y x
60 58 59 nffv 
 |-  F/_ y ( ( G |` ( A (,) B ) ) ` x )
61 fveq2 
 |-  ( y = x -> ( ( G |` ( A (,) B ) ) ` y ) = ( ( G |` ( A (,) B ) ) ` x ) )
62 57 60 61 cbvmpt 
 |-  ( y e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` y ) ) = ( x e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` x ) )
63 62 a1i 
 |-  ( ph -> ( y e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` y ) ) = ( x e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` x ) ) )
64 fvres 
 |-  ( x e. ( A (,) B ) -> ( ( G |` ( A (,) B ) ) ` x ) = ( G ` x ) )
65 64 adantl 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( G |` ( A (,) B ) ) ` x ) = ( G ` x ) )
66 simpr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( A (,) B ) )
67 48 66 sselid 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( A [,] B ) )
68 10 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> R e. CC )
69 13 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ x = B ) -> L e. CC )
70 38 adantr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ -. x = B ) -> ( F ` x ) e. CC )
71 69 70 ifclda 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = B , L , ( F ` x ) ) e. CC )
72 68 71 ifcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) e. CC )
73 2 fvmpt2 
 |-  ( ( 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 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( G ` x ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
75 elioo4g 
 |-  ( x e. ( A (,) B ) <-> ( ( A e. RR* /\ B e. RR* /\ x e. RR ) /\ ( A < x /\ x < B ) ) )
76 75 biimpi 
 |-  ( x e. ( A (,) B ) -> ( ( A e. RR* /\ B e. RR* /\ x e. RR ) /\ ( A < x /\ x < B ) ) )
77 76 simpld 
 |-  ( x e. ( A (,) B ) -> ( A e. RR* /\ B e. RR* /\ x e. RR ) )
78 77 simp1d 
 |-  ( x e. ( A (,) B ) -> A e. RR* )
79 elioore 
 |-  ( x e. ( A (,) B ) -> x e. RR )
80 79 rexrd 
 |-  ( x e. ( A (,) B ) -> x e. RR* )
81 eliooord 
 |-  ( x e. ( A (,) B ) -> ( A < x /\ x < B ) )
82 81 simpld 
 |-  ( x e. ( A (,) B ) -> A < x )
83 xrltne 
 |-  ( ( A e. RR* /\ x e. RR* /\ A < x ) -> x =/= A )
84 78 80 82 83 syl3anc 
 |-  ( x e. ( A (,) B ) -> x =/= A )
85 84 adantl 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x =/= A )
86 85 neneqd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> -. x = A )
87 86 iffalsed 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
88 81 simprd 
 |-  ( x e. ( A (,) B ) -> x < B )
89 79 88 ltned 
 |-  ( x e. ( A (,) B ) -> x =/= B )
90 89 neneqd 
 |-  ( x e. ( A (,) B ) -> -. x = B )
91 90 iffalsed 
 |-  ( x e. ( A (,) B ) -> if ( x = B , L , ( F ` x ) ) = ( F ` x ) )
92 91 adantl 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = B , L , ( F ` x ) ) = ( F ` x ) )
93 87 92 eqtrd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = ( F ` x ) )
94 65 74 93 3eqtrd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( G |` ( A (,) B ) ) ` x ) = ( F ` x ) )
95 1 94 mpteq2da 
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( ( G |` ( A (,) B ) ) ` x ) ) = ( x e. ( A (,) B ) |-> ( F ` x ) ) )
96 51 63 95 3eqtrd 
 |-  ( ph -> ( G |` ( A (,) B ) ) = ( x e. ( A (,) B ) |-> ( F ` x ) ) )
97 37 feqmptd 
 |-  ( ph -> F = ( x e. ( A (,) B ) |-> ( F ` x ) ) )
98 ioosscn 
 |-  ( A (,) B ) C_ CC
99 98 a1i 
 |-  ( ph -> ( A (,) B ) C_ CC )
100 ssid 
 |-  CC C_ CC
101 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
102 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) = ( ( TopOpen ` CCfld ) |`t ( A (,) B ) )
103 101 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
104 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
105 104 restid 
 |-  ( ( TopOpen ` CCfld ) e. Top -> ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld ) )
106 103 105 ax-mp 
 |-  ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld )
107 106 eqcomi 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
108 101 102 107 cncfcn 
 |-  ( ( ( A (,) B ) C_ CC /\ CC C_ CC ) -> ( ( A (,) B ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) )
109 99 100 108 sylancl 
 |-  ( ph -> ( ( A (,) B ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) )
110 6 97 109 3eltr3d 
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( F ` x ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) )
111 96 110 eqeltrd 
 |-  ( ph -> ( G |` ( A (,) B ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) )
112 104 restuni 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( A (,) B ) C_ CC ) -> ( A (,) B ) = U. ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) )
113 103 98 112 mp2an 
 |-  ( A (,) B ) = U. ( ( TopOpen ` CCfld ) |`t ( A (,) B ) )
114 113 cncnpi 
 |-  ( ( ( G |` ( A (,) B ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) /\ y e. ( A (,) B ) ) -> ( G |` ( A (,) B ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
115 111 114 sylan 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( G |` ( A (,) B ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
116 103 a1i 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( TopOpen ` CCfld ) e. Top )
117 48 a1i 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( A (,) B ) C_ ( A [,] B ) )
118 ovex 
 |-  ( A [,] B ) e. _V
119 118 a1i 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( A [,] B ) e. _V )
120 restabs 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( A (,) B ) C_ ( A [,] B ) /\ ( A [,] B ) e. _V ) -> ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) |`t ( A (,) B ) ) = ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) )
121 116 117 119 120 syl3anc 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) |`t ( A (,) B ) ) = ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) )
122 121 eqcomd 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) = ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) |`t ( A (,) B ) ) )
123 122 oveq1d 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) = ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) )
124 123 fveq1d 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) = ( ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
125 115 124 eleqtrd 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( G |` ( A (,) B ) ) e. ( ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
126 resttop 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( A [,] B ) e. _V ) -> ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) e. Top )
127 103 118 126 mp2an 
 |-  ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) e. Top
128 127 a1i 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) e. Top )
129 48 a1i 
 |-  ( ph -> ( A (,) B ) C_ ( A [,] B ) )
130 3 4 iccssred 
 |-  ( ph -> ( A [,] B ) C_ RR )
131 ax-resscn 
 |-  RR C_ CC
132 130 131 sstrdi 
 |-  ( ph -> ( A [,] B ) C_ CC )
133 104 restuni 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( A [,] B ) C_ CC ) -> ( A [,] B ) = U. ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) )
134 103 132 133 sylancr 
 |-  ( ph -> ( A [,] B ) = U. ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) )
135 129 134 sseqtrd 
 |-  ( ph -> ( A (,) B ) C_ U. ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) )
136 135 adantr 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( A (,) B ) C_ U. ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) )
137 retop 
 |-  ( topGen ` ran (,) ) e. Top
138 137 a1i 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( topGen ` ran (,) ) e. Top )
139 ioossre 
 |-  ( A (,) B ) C_ RR
140 difss 
 |-  ( RR \ ( A [,] B ) ) C_ RR
141 139 140 unssi 
 |-  ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) C_ RR
142 141 a1i 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) C_ RR )
143 ssun1 
 |-  ( A (,) B ) C_ ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) )
144 143 a1i 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( A (,) B ) C_ ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) )
145 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
146 145 ntrss 
 |-  ( ( ( 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 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) C_ ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
148 simpr 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( A (,) B ) )
149 ioontr 
 |-  ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) = ( A (,) B )
150 148 149 eleqtrrdi 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( topGen ` ran (,) ) ) ` ( A (,) B ) ) )
151 147 150 sseldd 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) )
152 48 148 sselid 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( A [,] B ) )
153 151 152 elind 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) u. ( RR \ ( A [,] B ) ) ) ) i^i ( A [,] B ) ) )
154 130 adantr 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( A [,] B ) C_ RR )
155 eqid 
 |-  ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) = ( ( topGen ` ran (,) ) |`t ( A [,] B ) )
156 145 155 restntr 
 |-  ( ( ( 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 
 |-  ( ( 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 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) ) ` ( A (,) B ) ) )
159 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
160 159 a1i 
 |-  ( ph -> ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR ) )
161 160 oveq1d 
 |-  ( ph -> ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) = ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( A [,] B ) ) )
162 103 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. Top )
163 reex 
 |-  RR e. _V
164 163 a1i 
 |-  ( ph -> RR e. _V )
165 restabs 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( A [,] B ) C_ RR /\ RR e. _V ) -> ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( A [,] B ) ) = ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) )
166 162 130 164 165 syl3anc 
 |-  ( ph -> ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( A [,] B ) ) = ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) )
167 161 166 eqtrd 
 |-  ( ph -> ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) = ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) )
168 167 fveq2d 
 |-  ( ph -> ( int ` ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) ) = ( int ` ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) ) )
169 168 fveq1d 
 |-  ( ph -> ( ( int ` ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) ) ` ( A (,) B ) ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) ) ` ( A (,) B ) ) )
170 169 adantr 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( int ` ( ( topGen ` ran (,) ) |`t ( A [,] B ) ) ) ` ( A (,) B ) ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) ) ` ( A (,) B ) ) )
171 158 170 eleqtrd 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) ) ` ( A (,) B ) ) )
172 134 feq2d 
 |-  ( ph -> ( G : ( A [,] B ) --> CC <-> G : U. ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) --> CC ) )
173 42 172 mpbid 
 |-  ( ph -> G : U. ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) --> CC )
174 173 adantr 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> G : U. ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) --> CC )
175 eqid 
 |-  U. ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) = U. ( ( TopOpen ` CCfld ) |`t ( A [,] B ) )
176 175 104 cnprest 
 |-  ( ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) e. Top /\ ( A (,) B ) C_ U. ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) ) /\ ( y e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) ) ` ( A (,) B ) ) /\ G : U. ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) --> CC ) ) -> ( G e. ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) <-> ( G |` ( A (,) B ) ) e. ( ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) ) )
177 128 136 171 174 176 syl22anc 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( G e. ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) <-> ( G |` ( A (,) B ) ) e. ( ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) ) )
178 125 177 mpbird 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> G e. ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
179 elpri 
 |-  ( y e. { A , B } -> ( y = A \/ y = B ) )
180 iftrue 
 |-  ( x = A -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = R )
181 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
182 23 25 27 181 syl3anc 
 |-  ( ph -> A e. ( A [,] B ) )
183 2 180 182 8 fvmptd3 
 |-  ( ph -> ( G ` A ) = R )
184 97 eqcomd 
 |-  ( ph -> ( x e. ( A (,) B ) |-> ( F ` x ) ) = F )
185 96 184 eqtr2d 
 |-  ( ph -> F = ( G |` ( A (,) B ) ) )
186 185 oveq1d 
 |-  ( ph -> ( F limCC A ) = ( ( G |` ( A (,) B ) ) limCC A ) )
187 8 186 eleqtrd 
 |-  ( ph -> R e. ( ( G |` ( A (,) B ) ) limCC A ) )
188 3 4 5 42 limciccioolb 
 |-  ( ph -> ( ( G |` ( A (,) B ) ) limCC A ) = ( G limCC A ) )
189 187 188 eleqtrd 
 |-  ( ph -> R e. ( G limCC A ) )
190 183 189 eqeltrd 
 |-  ( ph -> ( G ` A ) e. ( G limCC A ) )
191 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) = ( ( TopOpen ` CCfld ) |`t ( A [,] B ) )
192 101 191 cnplimc 
 |-  ( ( ( A [,] B ) C_ CC /\ A e. ( A [,] B ) ) -> ( G e. ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` A ) <-> ( G : ( A [,] B ) --> CC /\ ( G ` A ) e. ( G limCC A ) ) ) )
193 132 182 192 syl2anc 
 |-  ( ph -> ( G e. ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` A ) <-> ( G : ( A [,] B ) --> CC /\ ( G ` A ) e. ( G limCC A ) ) ) )
194 42 190 193 mpbir2and 
 |-  ( ph -> G e. ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` A ) )
195 194 adantr 
 |-  ( ( ph /\ y = A ) -> G e. ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` A ) )
196 fveq2 
 |-  ( y = A -> ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) = ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` A ) )
197 196 eqcomd 
 |-  ( y = A -> ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` A ) = ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
198 197 adantl 
 |-  ( ( ph /\ y = A ) -> ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` A ) = ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
199 195 198 eleqtrd 
 |-  ( ( ph /\ y = A ) -> G e. ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
200 180 adantl 
 |-  ( ( x = B /\ x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = R )
201 eqtr2 
 |-  ( ( x = B /\ x = A ) -> B = A )
202 iftrue 
 |-  ( B = A -> if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) = R )
203 202 eqcomd 
 |-  ( B = A -> R = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
204 201 203 syl 
 |-  ( ( x = B /\ x = A ) -> R = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
205 200 204 eqtrd 
 |-  ( ( x = B /\ x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
206 iffalse 
 |-  ( -. x = A -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
207 206 adantl 
 |-  ( ( x = B /\ -. x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
208 iftrue 
 |-  ( x = B -> if ( x = B , L , ( F ` x ) ) = L )
209 208 adantr 
 |-  ( ( x = B /\ -. x = A ) -> if ( x = B , L , ( F ` x ) ) = L )
210 df-ne 
 |-  ( x =/= A <-> -. x = A )
211 pm13.18 
 |-  ( ( x = B /\ x =/= A ) -> B =/= A )
212 210 211 sylan2br 
 |-  ( ( x = B /\ -. x = A ) -> B =/= A )
213 212 neneqd 
 |-  ( ( x = B /\ -. x = A ) -> -. B = A )
214 213 iffalsed 
 |-  ( ( x = B /\ -. x = A ) -> if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) = if ( B = B , L , ( F ` B ) ) )
215 eqid 
 |-  B = B
216 215 iftruei 
 |-  if ( B = B , L , ( F ` B ) ) = L
217 214 216 eqtr2di 
 |-  ( ( x = B /\ -. x = A ) -> L = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
218 207 209 217 3eqtrd 
 |-  ( ( x = B /\ -. x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
219 205 218 pm2.61dan 
 |-  ( x = B -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
220 4 leidd 
 |-  ( ph -> B <_ B )
221 3 4 4 27 220 eliccd 
 |-  ( ph -> B e. ( A [,] B ) )
222 216 13 eqeltrid 
 |-  ( ph -> if ( B = B , L , ( F ` B ) ) e. CC )
223 10 222 ifcld 
 |-  ( ph -> if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) e. CC )
224 2 219 221 223 fvmptd3 
 |-  ( ph -> ( G ` B ) = if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) )
225 3 5 gtned 
 |-  ( ph -> B =/= A )
226 225 neneqd 
 |-  ( ph -> -. B = A )
227 226 iffalsed 
 |-  ( ph -> if ( B = A , R , if ( B = B , L , ( F ` B ) ) ) = if ( B = B , L , ( F ` B ) ) )
228 216 a1i 
 |-  ( ph -> if ( B = B , L , ( F ` B ) ) = L )
229 224 227 228 3eqtrd 
 |-  ( ph -> ( G ` B ) = L )
230 185 oveq1d 
 |-  ( ph -> ( F limCC B ) = ( ( G |` ( A (,) B ) ) limCC B ) )
231 7 230 eleqtrd 
 |-  ( ph -> L e. ( ( G |` ( A (,) B ) ) limCC B ) )
232 3 4 5 42 limcicciooub 
 |-  ( ph -> ( ( G |` ( A (,) B ) ) limCC B ) = ( G limCC B ) )
233 231 232 eleqtrd 
 |-  ( ph -> L e. ( G limCC B ) )
234 229 233 eqeltrd 
 |-  ( ph -> ( G ` B ) e. ( G limCC B ) )
235 101 191 cnplimc 
 |-  ( ( ( A [,] B ) C_ CC /\ B e. ( A [,] B ) ) -> ( G e. ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` B ) <-> ( G : ( A [,] B ) --> CC /\ ( G ` B ) e. ( G limCC B ) ) ) )
236 132 221 235 syl2anc 
 |-  ( ph -> ( G e. ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` B ) <-> ( G : ( A [,] B ) --> CC /\ ( G ` B ) e. ( G limCC B ) ) ) )
237 42 234 236 mpbir2and 
 |-  ( ph -> G e. ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` B ) )
238 237 adantr 
 |-  ( ( ph /\ y = B ) -> G e. ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` B ) )
239 fveq2 
 |-  ( y = B -> ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) = ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` B ) )
240 239 eqcomd 
 |-  ( y = B -> ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` B ) = ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
241 240 adantl 
 |-  ( ( ph /\ y = B ) -> ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` B ) = ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
242 238 241 eleqtrd 
 |-  ( ( ph /\ y = B ) -> G e. ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
243 199 242 jaodan 
 |-  ( ( ph /\ ( y = A \/ y = B ) ) -> G e. ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
244 179 243 sylan2 
 |-  ( ( ph /\ y e. { A , B } ) -> G e. ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
245 178 244 jaodan 
 |-  ( ( ph /\ ( y e. ( A (,) B ) \/ y e. { A , B } ) ) -> G e. ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
246 47 245 syldan 
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> G e. ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
247 246 ralrimiva 
 |-  ( ph -> A. y e. ( A [,] B ) G e. ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
248 101 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
249 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( A [,] B ) C_ CC ) -> ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) e. ( TopOn ` ( A [,] B ) ) )
250 248 132 249 sylancr 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) e. ( TopOn ` ( A [,] B ) ) )
251 cncnp 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) e. ( TopOn ` ( A [,] B ) ) /\ ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) -> ( G e. ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) Cn ( TopOpen ` CCfld ) ) <-> ( G : ( A [,] B ) --> CC /\ A. y e. ( A [,] B ) G e. ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) ) ) )
252 250 248 251 sylancl 
 |-  ( ph -> ( G e. ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) Cn ( TopOpen ` CCfld ) ) <-> ( G : ( A [,] B ) --> CC /\ A. y e. ( A [,] B ) G e. ( ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) ) ) )
253 42 247 252 mpbir2and 
 |-  ( ph -> G e. ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) Cn ( TopOpen ` CCfld ) ) )
254 101 191 107 cncfcn 
 |-  ( ( ( A [,] B ) C_ CC /\ CC C_ CC ) -> ( ( A [,] B ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) Cn ( TopOpen ` CCfld ) ) )
255 132 100 254 sylancl 
 |-  ( ph -> ( ( A [,] B ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( A [,] B ) ) Cn ( TopOpen ` CCfld ) ) )
256 253 255 eleqtrrd 
 |-  ( ph -> G e. ( ( A [,] B ) -cn-> CC ) )