Metamath Proof Explorer

Theorem fourierdlem33

Description: Limit of a continuous function on an open subinterval. Upper bound version. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem33.1 
|- ( ph -> A e. RR )
fourierdlem33.2 
|- ( ph -> B e. RR )
fourierdlem33.3 
|- ( ph -> A < B )
fourierdlem33.4 
|- ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
fourierdlem33.5 
|- ( ph -> L e. ( F limCC B ) )
fourierdlem33.6 
|- ( ph -> C e. RR )
fourierdlem33.7 
|- ( ph -> D e. RR )
fourierdlem33.8 
|- ( ph -> C < D )
fourierdlem33.ss 
|- ( ph -> ( C (,) D ) C_ ( A (,) B ) )
fourierdlem33.y 
|- Y = if ( D = B , L , ( F ` D ) )
fourierdlem33.10 
|- J = ( ( TopOpen ` CCfld ) |`t ( ( A (,) B ) u. { B } ) )
Assertion fourierdlem33 
|- ( ph -> Y e. ( ( F |` ( C (,) D ) ) limCC D ) )

Proof

Step Hyp Ref Expression
1 fourierdlem33.1 
 |-  ( ph -> A e. RR )
2 fourierdlem33.2 
 |-  ( ph -> B e. RR )
3 fourierdlem33.3 
 |-  ( ph -> A < B )
4 fourierdlem33.4 
 |-  ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
5 fourierdlem33.5 
 |-  ( ph -> L e. ( F limCC B ) )
6 fourierdlem33.6 
 |-  ( ph -> C e. RR )
7 fourierdlem33.7 
 |-  ( ph -> D e. RR )
8 fourierdlem33.8 
 |-  ( ph -> C < D )
9 fourierdlem33.ss 
 |-  ( ph -> ( C (,) D ) C_ ( A (,) B ) )
10 fourierdlem33.y 
 |-  Y = if ( D = B , L , ( F ` D ) )
11 fourierdlem33.10 
 |-  J = ( ( TopOpen ` CCfld ) |`t ( ( A (,) B ) u. { B } ) )
12 5 adantr 
 |-  ( ( ph /\ D = B ) -> L e. ( F limCC B ) )
13 iftrue 
 |-  ( D = B -> if ( D = B , L , ( F ` D ) ) = L )
14 10 13 eqtr2id 
 |-  ( D = B -> L = Y )
15 14 adantl 
 |-  ( ( ph /\ D = B ) -> L = Y )
16 oveq2 
 |-  ( D = B -> ( ( F |` ( C (,) D ) ) limCC D ) = ( ( F |` ( C (,) D ) ) limCC B ) )
17 16 adantl 
 |-  ( ( ph /\ D = B ) -> ( ( F |` ( C (,) D ) ) limCC D ) = ( ( F |` ( C (,) D ) ) limCC B ) )
18 cncff 
 |-  ( F e. ( ( A (,) B ) -cn-> CC ) -> F : ( A (,) B ) --> CC )
19 4 18 syl 
 |-  ( ph -> F : ( A (,) B ) --> CC )
20 19 adantr 
 |-  ( ( ph /\ D = B ) -> F : ( A (,) B ) --> CC )
21 9 adantr 
 |-  ( ( ph /\ D = B ) -> ( C (,) D ) C_ ( A (,) B ) )
22 ioosscn 
 |-  ( A (,) B ) C_ CC
23 22 a1i 
 |-  ( ( ph /\ D = B ) -> ( A (,) B ) C_ CC )
24 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
25 7 leidd 
 |-  ( ph -> D <_ D )
26 6 rexrd 
 |-  ( ph -> C e. RR* )
27 elioc2 
 |-  ( ( C e. RR* /\ D e. RR ) -> ( D e. ( C (,] D ) <-> ( D e. RR /\ C < D /\ D <_ D ) ) )
28 26 7 27 syl2anc 
 |-  ( ph -> ( D e. ( C (,] D ) <-> ( D e. RR /\ C < D /\ D <_ D ) ) )
29 7 8 25 28 mpbir3and 
 |-  ( ph -> D e. ( C (,] D ) )
30 29 adantr 
 |-  ( ( ph /\ D = B ) -> D e. ( C (,] D ) )
31 eqcom 
 |-  ( D = B <-> B = D )
32 31 bilani 
 |-  ( ( ph /\ D = B ) -> B = D )
33 24 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
34 1 rexrd 
 |-  ( ph -> A e. RR* )
35 2 rexrd 
 |-  ( ph -> B e. RR* )
36 ioounsn 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( A (,) B ) u. { B } ) = ( A (,] B ) )
37 34 35 3 36 syl3anc 
 |-  ( ph -> ( ( A (,) B ) u. { B } ) = ( A (,] B ) )
38 ovex 
 |-  ( A (,] B ) e. _V
39 38 a1i 
 |-  ( ph -> ( A (,] B ) e. _V )
40 37 39 eqeltrd 
 |-  ( ph -> ( ( A (,) B ) u. { B } ) e. _V )
41 resttop 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( ( A (,) B ) u. { B } ) e. _V ) -> ( ( TopOpen ` CCfld ) |`t ( ( A (,) B ) u. { B } ) ) e. Top )
42 33 40 41 sylancr 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t ( ( A (,) B ) u. { B } ) ) e. Top )
43 11 42 eqeltrid 
 |-  ( ph -> J e. Top )
44 43 adantr 
 |-  ( ( ph /\ D = B ) -> J e. Top )
45 oveq2 
 |-  ( D = B -> ( C (,] D ) = ( C (,] B ) )
46 45 adantl 
 |-  ( ( ph /\ D = B ) -> ( C (,] D ) = ( C (,] B ) )
47 26 adantr 
 |-  ( ( ph /\ x e. ( C (,] B ) ) -> C e. RR* )
48 pnfxr 
 |-  +oo e. RR*
49 48 a1i 
 |-  ( ( ph /\ x e. ( C (,] B ) ) -> +oo e. RR* )
50 simpr 
 |-  ( ( ph /\ x e. ( C (,] B ) ) -> x e. ( C (,] B ) )
51 2 adantr 
 |-  ( ( ph /\ x e. ( C (,] B ) ) -> B e. RR )
52 elioc2 
 |-  ( ( C e. RR* /\ B e. RR ) -> ( x e. ( C (,] B ) <-> ( x e. RR /\ C < x /\ x <_ B ) ) )
53 47 51 52 syl2anc 
 |-  ( ( ph /\ x e. ( C (,] B ) ) -> ( x e. ( C (,] B ) <-> ( x e. RR /\ C < x /\ x <_ B ) ) )
54 50 53 mpbid 
 |-  ( ( ph /\ x e. ( C (,] B ) ) -> ( x e. RR /\ C < x /\ x <_ B ) )
55 54 simp1d 
 |-  ( ( ph /\ x e. ( C (,] B ) ) -> x e. RR )
56 54 simp2d 
 |-  ( ( ph /\ x e. ( C (,] B ) ) -> C < x )
57 55 ltpnfd 
 |-  ( ( ph /\ x e. ( C (,] B ) ) -> x < +oo )
58 47 49 55 56 57 eliood 
 |-  ( ( ph /\ x e. ( C (,] B ) ) -> x e. ( C (,) +oo ) )
59 1 adantr 
 |-  ( ( ph /\ x e. ( C (,] B ) ) -> A e. RR )
60 6 adantr 
 |-  ( ( ph /\ x e. ( C (,] B ) ) -> C e. RR )
61 1 2 6 7 8 9 fourierdlem10 
 |-  ( ph -> ( A <_ C /\ D <_ B ) )
62 61 simpld 
 |-  ( ph -> A <_ C )
63 62 adantr 
 |-  ( ( ph /\ x e. ( C (,] B ) ) -> A <_ C )
64 59 60 55 63 56 lelttrd 
 |-  ( ( ph /\ x e. ( C (,] B ) ) -> A < x )
65 54 simp3d 
 |-  ( ( ph /\ x e. ( C (,] B ) ) -> x <_ B )
66 34 adantr 
 |-  ( ( ph /\ x e. ( C (,] B ) ) -> A e. RR* )
67 elioc2 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( x e. ( A (,] B ) <-> ( x e. RR /\ A < x /\ x <_ B ) ) )
68 66 51 67 syl2anc 
 |-  ( ( ph /\ x e. ( C (,] B ) ) -> ( x e. ( A (,] B ) <-> ( x e. RR /\ A < x /\ x <_ B ) ) )
69 55 64 65 68 mpbir3and 
 |-  ( ( ph /\ x e. ( C (,] B ) ) -> x e. ( A (,] B ) )
70 58 69 elind 
 |-  ( ( ph /\ x e. ( C (,] B ) ) -> x e. ( ( C (,) +oo ) i^i ( A (,] B ) ) )
71 elinel1 
 |-  ( x e. ( ( C (,) +oo ) i^i ( A (,] B ) ) -> x e. ( C (,) +oo ) )
72 elioore 
 |-  ( x e. ( C (,) +oo ) -> x e. RR )
73 71 72 syl 
 |-  ( x e. ( ( C (,) +oo ) i^i ( A (,] B ) ) -> x e. RR )
74 73 adantl 
 |-  ( ( ph /\ x e. ( ( C (,) +oo ) i^i ( A (,] B ) ) ) -> x e. RR )
75 26 adantr 
 |-  ( ( ph /\ x e. ( ( C (,) +oo ) i^i ( A (,] B ) ) ) -> C e. RR* )
76 48 a1i 
 |-  ( ( ph /\ x e. ( ( C (,) +oo ) i^i ( A (,] B ) ) ) -> +oo e. RR* )
77 71 adantl 
 |-  ( ( ph /\ x e. ( ( C (,) +oo ) i^i ( A (,] B ) ) ) -> x e. ( C (,) +oo ) )
78 ioogtlb 
 |-  ( ( C e. RR* /\ +oo e. RR* /\ x e. ( C (,) +oo ) ) -> C < x )
79 75 76 77 78 syl3anc 
 |-  ( ( ph /\ x e. ( ( C (,) +oo ) i^i ( A (,] B ) ) ) -> C < x )
80 elinel2 
 |-  ( x e. ( ( C (,) +oo ) i^i ( A (,] B ) ) -> x e. ( A (,] B ) )
81 80 adantl 
 |-  ( ( ph /\ x e. ( ( C (,) +oo ) i^i ( A (,] B ) ) ) -> x e. ( A (,] B ) )
82 34 adantr 
 |-  ( ( ph /\ x e. ( ( C (,) +oo ) i^i ( A (,] B ) ) ) -> A e. RR* )
83 2 adantr 
 |-  ( ( ph /\ x e. ( ( C (,) +oo ) i^i ( A (,] B ) ) ) -> B e. RR )
84 82 83 67 syl2anc 
 |-  ( ( ph /\ x e. ( ( C (,) +oo ) i^i ( A (,] B ) ) ) -> ( x e. ( A (,] B ) <-> ( x e. RR /\ A < x /\ x <_ B ) ) )
85 81 84 mpbid 
 |-  ( ( ph /\ x e. ( ( C (,) +oo ) i^i ( A (,] B ) ) ) -> ( x e. RR /\ A < x /\ x <_ B ) )
86 85 simp3d 
 |-  ( ( ph /\ x e. ( ( C (,) +oo ) i^i ( A (,] B ) ) ) -> x <_ B )
87 75 83 52 syl2anc 
 |-  ( ( ph /\ x e. ( ( C (,) +oo ) i^i ( A (,] B ) ) ) -> ( x e. ( C (,] B ) <-> ( x e. RR /\ C < x /\ x <_ B ) ) )
88 74 79 86 87 mpbir3and 
 |-  ( ( ph /\ x e. ( ( C (,) +oo ) i^i ( A (,] B ) ) ) -> x e. ( C (,] B ) )
89 70 88 impbida 
 |-  ( ph -> ( x e. ( C (,] B ) <-> x e. ( ( C (,) +oo ) i^i ( A (,] B ) ) ) )
90 89 eqrdv 
 |-  ( ph -> ( C (,] B ) = ( ( C (,) +oo ) i^i ( A (,] B ) ) )
91 retop 
 |-  ( topGen ` ran (,) ) e. Top
92 91 a1i 
 |-  ( ph -> ( topGen ` ran (,) ) e. Top )
93 iooretop 
 |-  ( C (,) +oo ) e. ( topGen ` ran (,) )
94 93 a1i 
 |-  ( ph -> ( C (,) +oo ) e. ( topGen ` ran (,) ) )
95 elrestr 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( A (,] B ) e. _V /\ ( C (,) +oo ) e. ( topGen ` ran (,) ) ) -> ( ( C (,) +oo ) i^i ( A (,] B ) ) e. ( ( topGen ` ran (,) ) |`t ( A (,] B ) ) )
96 92 39 94 95 syl3anc 
 |-  ( ph -> ( ( C (,) +oo ) i^i ( A (,] B ) ) e. ( ( topGen ` ran (,) ) |`t ( A (,] B ) ) )
97 90 96 eqeltrd 
 |-  ( ph -> ( C (,] B ) e. ( ( topGen ` ran (,) ) |`t ( A (,] B ) ) )
98 97 adantr 
 |-  ( ( ph /\ D = B ) -> ( C (,] B ) e. ( ( topGen ` ran (,) ) |`t ( A (,] B ) ) )
99 46 98 eqeltrd 
 |-  ( ( ph /\ D = B ) -> ( C (,] D ) e. ( ( topGen ` ran (,) ) |`t ( A (,] B ) ) )
100 11 a1i 
 |-  ( ph -> J = ( ( TopOpen ` CCfld ) |`t ( ( A (,) B ) u. { B } ) ) )
101 37 oveq2d 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t ( ( A (,) B ) u. { B } ) ) = ( ( TopOpen ` CCfld ) |`t ( A (,] B ) ) )
102 33 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. Top )
103 iocssre 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) C_ RR )
104 34 2 103 syl2anc 
 |-  ( ph -> ( A (,] B ) C_ RR )
105 reex 
 |-  RR e. _V
106 105 a1i 
 |-  ( ph -> RR e. _V )
107 restabs 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( A (,] B ) C_ RR /\ RR e. _V ) -> ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( A (,] B ) ) = ( ( TopOpen ` CCfld ) |`t ( A (,] B ) ) )
108 102 104 106 107 syl3anc 
 |-  ( ph -> ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( A (,] B ) ) = ( ( TopOpen ` CCfld ) |`t ( A (,] B ) ) )
109 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
110 109 eqcomi 
 |-  ( ( TopOpen ` CCfld ) |`t RR ) = ( topGen ` ran (,) )
111 110 oveq1i 
 |-  ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( A (,] B ) ) = ( ( topGen ` ran (,) ) |`t ( A (,] B ) )
112 108 111 eqtr3di 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t ( A (,] B ) ) = ( ( topGen ` ran (,) ) |`t ( A (,] B ) ) )
113 100 101 112 3eqtrrd 
 |-  ( ph -> ( ( topGen ` ran (,) ) |`t ( A (,] B ) ) = J )
114 113 adantr 
 |-  ( ( ph /\ D = B ) -> ( ( topGen ` ran (,) ) |`t ( A (,] B ) ) = J )
115 99 114 eleqtrd 
 |-  ( ( ph /\ D = B ) -> ( C (,] D ) e. J )
116 isopn3i 
 |-  ( ( J e. Top /\ ( C (,] D ) e. J ) -> ( ( int ` J ) ` ( C (,] D ) ) = ( C (,] D ) )
117 44 115 116 syl2anc 
 |-  ( ( ph /\ D = B ) -> ( ( int ` J ) ` ( C (,] D ) ) = ( C (,] D ) )
118 30 32 117 3eltr4d 
 |-  ( ( ph /\ D = B ) -> B e. ( ( int ` J ) ` ( C (,] D ) ) )
119 sneq 
 |-  ( D = B -> { D } = { B } )
120 119 eqcomd 
 |-  ( D = B -> { B } = { D } )
121 120 uneq2d 
 |-  ( D = B -> ( ( C (,) D ) u. { B } ) = ( ( C (,) D ) u. { D } ) )
122 121 adantl 
 |-  ( ( ph /\ D = B ) -> ( ( C (,) D ) u. { B } ) = ( ( C (,) D ) u. { D } ) )
123 7 rexrd 
 |-  ( ph -> D e. RR* )
124 ioounsn 
 |-  ( ( C e. RR* /\ D e. RR* /\ C < D ) -> ( ( C (,) D ) u. { D } ) = ( C (,] D ) )
125 26 123 8 124 syl3anc 
 |-  ( ph -> ( ( C (,) D ) u. { D } ) = ( C (,] D ) )
126 125 adantr 
 |-  ( ( ph /\ D = B ) -> ( ( C (,) D ) u. { D } ) = ( C (,] D ) )
127 122 126 eqtr2d 
 |-  ( ( ph /\ D = B ) -> ( C (,] D ) = ( ( C (,) D ) u. { B } ) )
128 127 fveq2d 
 |-  ( ( ph /\ D = B ) -> ( ( int ` J ) ` ( C (,] D ) ) = ( ( int ` J ) ` ( ( C (,) D ) u. { B } ) ) )
129 118 128 eleqtrd 
 |-  ( ( ph /\ D = B ) -> B e. ( ( int ` J ) ` ( ( C (,) D ) u. { B } ) ) )
130 20 21 23 24 11 129 limcres 
 |-  ( ( ph /\ D = B ) -> ( ( F |` ( C (,) D ) ) limCC B ) = ( F limCC B ) )
131 17 130 eqtr2d 
 |-  ( ( ph /\ D = B ) -> ( F limCC B ) = ( ( F |` ( C (,) D ) ) limCC D ) )
132 12 15 131 3eltr3d 
 |-  ( ( ph /\ D = B ) -> Y e. ( ( F |` ( C (,) D ) ) limCC D ) )
133 limcresi 
 |-  ( F limCC D ) C_ ( ( F |` ( C (,) D ) ) limCC D )
134 iffalse 
 |-  ( -. D = B -> if ( D = B , L , ( F ` D ) ) = ( F ` D ) )
135 10 134 eqtrid 
 |-  ( -. D = B -> Y = ( F ` D ) )
136 135 adantl 
 |-  ( ( ph /\ -. D = B ) -> Y = ( F ` D ) )
137 ssid 
 |-  CC C_ CC
138 137 a1i 
 |-  ( ph -> CC C_ CC )
139 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) = ( ( TopOpen ` CCfld ) |`t ( A (,) B ) )
140 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
141 140 restid 
 |-  ( ( TopOpen ` CCfld ) e. Top -> ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld ) )
142 33 141 ax-mp 
 |-  ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld )
143 142 eqcomi 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
144 24 139 143 cncfcn 
 |-  ( ( ( A (,) B ) C_ CC /\ CC C_ CC ) -> ( ( A (,) B ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) )
145 22 138 144 sylancr 
 |-  ( ph -> ( ( A (,) B ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) )
146 4 145 eleqtrd 
 |-  ( ph -> F e. ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) )
147 24 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
148 22 a1i 
 |-  ( ph -> ( A (,) B ) C_ CC )
149 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( A (,) B ) C_ CC ) -> ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) e. ( TopOn ` ( A (,) B ) ) )
150 147 148 149 sylancr 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) e. ( TopOn ` ( A (,) B ) ) )
151 147 a1i 
 |-  ( ph -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
152 cncnp 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) e. ( TopOn ` ( A (,) B ) ) /\ ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) -> ( F e. ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) <-> ( F : ( A (,) B ) --> CC /\ A. x e. ( A (,) B ) F e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` x ) ) ) )
153 150 151 152 syl2anc 
 |-  ( ph -> ( F e. ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) <-> ( F : ( A (,) B ) --> CC /\ A. x e. ( A (,) B ) F e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` x ) ) ) )
154 146 153 mpbid 
 |-  ( ph -> ( F : ( A (,) B ) --> CC /\ A. x e. ( A (,) B ) F e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` x ) ) )
155 154 simprd 
 |-  ( ph -> A. x e. ( A (,) B ) F e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` x ) )
156 155 adantr 
 |-  ( ( ph /\ -. D = B ) -> A. x e. ( A (,) B ) F e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` x ) )
157 34 adantr 
 |-  ( ( ph /\ -. D = B ) -> A e. RR* )
158 35 adantr 
 |-  ( ( ph /\ -. D = B ) -> B e. RR* )
159 7 adantr 
 |-  ( ( ph /\ -. D = B ) -> D e. RR )
160 1 6 7 62 8 lelttrd 
 |-  ( ph -> A < D )
161 160 adantr 
 |-  ( ( ph /\ -. D = B ) -> A < D )
162 2 adantr 
 |-  ( ( ph /\ -. D = B ) -> B e. RR )
163 61 simprd 
 |-  ( ph -> D <_ B )
164 163 adantr 
 |-  ( ( ph /\ -. D = B ) -> D <_ B )
165 neqne 
 |-  ( -. D = B -> D =/= B )
166 165 necomd 
 |-  ( -. D = B -> B =/= D )
167 166 adantl 
 |-  ( ( ph /\ -. D = B ) -> B =/= D )
168 159 162 164 167 leneltd 
 |-  ( ( ph /\ -. D = B ) -> D < B )
169 157 158 159 161 168 eliood 
 |-  ( ( ph /\ -. D = B ) -> D e. ( A (,) B ) )
170 fveq2 
 |-  ( x = D -> ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` x ) = ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` D ) )
171 170 eleq2d 
 |-  ( x = D -> ( F e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` x ) <-> F e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` D ) ) )
172 171 rspccva 
 |-  ( ( A. x e. ( A (,) B ) F e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` x ) /\ D e. ( A (,) B ) ) -> F e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` D ) )
173 156 169 172 syl2anc 
 |-  ( ( ph /\ -. D = B ) -> F e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` D ) )
174 24 139 cnplimc 
 |-  ( ( ( A (,) B ) C_ CC /\ D e. ( A (,) B ) ) -> ( F e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` D ) <-> ( F : ( A (,) B ) --> CC /\ ( F ` D ) e. ( F limCC D ) ) ) )
175 22 169 174 sylancr 
 |-  ( ( ph /\ -. D = B ) -> ( F e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` D ) <-> ( F : ( A (,) B ) --> CC /\ ( F ` D ) e. ( F limCC D ) ) ) )
176 173 175 mpbid 
 |-  ( ( ph /\ -. D = B ) -> ( F : ( A (,) B ) --> CC /\ ( F ` D ) e. ( F limCC D ) ) )
177 176 simprd 
 |-  ( ( ph /\ -. D = B ) -> ( F ` D ) e. ( F limCC D ) )
178 136 177 eqeltrd 
 |-  ( ( ph /\ -. D = B ) -> Y e. ( F limCC D ) )
179 133 178 sselid 
 |-  ( ( ph /\ -. D = B ) -> Y e. ( ( F |` ( C (,) D ) ) limCC D ) )
180 132 179 pm2.61dan 
 |-  ( ph -> Y e. ( ( F |` ( C (,) D ) ) limCC D ) )