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