Metamath Proof Explorer

Theorem fourierdlem32

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

Ref Expression
Hypotheses fourierdlem32.a 
|- ( ph -> A e. RR )
fourierdlem32.b 
|- ( ph -> B e. RR )
fourierdlem32.altb 
|- ( ph -> A < B )
fourierdlem32.f 
|- ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
fourierdlem32.l 
|- ( ph -> R e. ( F limCC A ) )
fourierdlem32.c 
|- ( ph -> C e. RR )
fourierdlem32.d 
|- ( ph -> D e. RR )
fourierdlem32.cltd 
|- ( ph -> C < D )
fourierdlem32.ss 
|- ( ph -> ( C (,) D ) C_ ( A (,) B ) )
fourierdlem32.y 
|- Y = if ( C = A , R , ( F ` C ) )
fourierdlem32.j 
|- J = ( ( TopOpen ` CCfld ) |`t ( A [,) B ) )
Assertion fourierdlem32 
|- ( ph -> Y e. ( ( F |` ( C (,) D ) ) limCC C ) )

Proof

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