Step | Hyp | Ref
| Expression |
1 | | cncfiooicclem1.x |
. . . 4
|
2 | | limccl 23639 |
. . . . . . 7
lim |
3 | | cncfiooicclem1.r |
. . . . . . 7
lim |
4 | 2, 3 | sseldi 3601 |
. . . . . 6
|
5 | 4 | ad2antrr 762 |
. . . . 5
|
6 | | limccl 23639 |
. . . . . . . 8
lim |
7 | | cncfiooicclem1.l |
. . . . . . . 8
lim |
8 | 6, 7 | sseldi 3601 |
. . . . . . 7
|
9 | 8 | ad3antrrr 766 |
. . . . . 6
|
10 | | simplll 798 |
. . . . . . 7
|
11 | | orel1 397 |
. . . . . . . . . . 11
|
12 | 11 | con3dimp 457 |
. . . . . . . . . 10
|
13 | | vex 3203 |
. . . . . . . . . . 11
|
14 | 13 | elpr 4198 |
. . . . . . . . . 10
|
15 | 12, 14 | sylnibr 319 |
. . . . . . . . 9
|
16 | 15 | adantll 750 |
. . . . . . . 8
|
17 | | simpllr 799 |
. . . . . . . . . 10
|
18 | | cncfiooicclem1.a |
. . . . . . . . . . . . 13
|
19 | 18 | rexrd 10089 |
. . . . . . . . . . . 12
|
20 | 10, 19 | syl 17 |
. . . . . . . . . . 11
|
21 | | cncfiooicclem1.b |
. . . . . . . . . . . . 13
|
22 | 21 | rexrd 10089 |
. . . . . . . . . . . 12
|
23 | 10, 22 | syl 17 |
. . . . . . . . . . 11
|
24 | | cncfiooicclem1.altb |
. . . . . . . . . . . . 13
|
25 | 18, 21, 24 | ltled 10185 |
. . . . . . . . . . . 12
|
26 | 10, 25 | syl 17 |
. . . . . . . . . . 11
|
27 | | prunioo 12301 |
. . . . . . . . . . 11
|
28 | 20, 23, 26, 27 | syl3anc 1326 |
. . . . . . . . . 10
|
29 | 17, 28 | eleqtrrd 2704 |
. . . . . . . . 9
|
30 | | elun 3753 |
. . . . . . . . 9
|
31 | 29, 30 | sylib 208 |
. . . . . . . 8
|
32 | | orel2 398 |
. . . . . . . 8
|
33 | 16, 31, 32 | sylc 65 |
. . . . . . 7
|
34 | | cncfiooicclem1.f |
. . . . . . . . 9
|
35 | | cncff 22696 |
. . . . . . . . 9
|
36 | 34, 35 | syl 17 |
. . . . . . . 8
|
37 | 36 | ffvelrnda 6359 |
. . . . . . 7
|
38 | 10, 33, 37 | syl2anc 693 |
. . . . . 6
|
39 | 9, 38 | ifclda 4120 |
. . . . 5
|
40 | 5, 39 | ifclda 4120 |
. . . 4
|
41 | | cncfiooicclem1.g |
. . . 4
|
42 | 1, 40, 41 | fmptdf 6387 |
. . 3
|
43 | | elun 3753 |
. . . . . . 7
|
44 | 19, 22, 25, 27 | syl3anc 1326 |
. . . . . . . 8
|
45 | 44 | eleq2d 2687 |
. . . . . . 7
|
46 | 43, 45 | syl5bbr 274 |
. . . . . 6
|
47 | 46 | biimpar 502 |
. . . . 5
|
48 | | ioossicc 12259 |
. . . . . . . . . . . . 13
|
49 | | fssres 6070 |
. . . . . . . . . . . . 13
|
50 | 42, 48, 49 | sylancl 694 |
. . . . . . . . . . . 12
|
51 | 50 | feqmptd 6249 |
. . . . . . . . . . 11
|
52 | | nfmpt1 4747 |
. . . . . . . . . . . . . . . 16
|
53 | 41, 52 | nfcxfr 2762 |
. . . . . . . . . . . . . . 15
|
54 | | nfcv 2764 |
. . . . . . . . . . . . . . 15
|
55 | 53, 54 | nfres 5398 |
. . . . . . . . . . . . . 14
|
56 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
57 | 55, 56 | nffv 6198 |
. . . . . . . . . . . . 13
|
58 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
59 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
60 | 58, 59 | nffv 6198 |
. . . . . . . . . . . . 13
|
61 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
62 | 57, 60, 61 | cbvmpt 4749 |
. . . . . . . . . . . 12
|
63 | 62 | a1i 11 |
. . . . . . . . . . 11
|
64 | | fvres 6207 |
. . . . . . . . . . . . . 14
|
65 | 64 | adantl 482 |
. . . . . . . . . . . . 13
|
66 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
67 | 48, 66 | sseldi 3601 |
. . . . . . . . . . . . . 14
|
68 | 4 | adantr 481 |
. . . . . . . . . . . . . . 15
|
69 | 8 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
70 | 37 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
71 | 69, 70 | ifclda 4120 |
. . . . . . . . . . . . . . 15
|
72 | 68, 71 | ifcld 4131 |
. . . . . . . . . . . . . 14
|
73 | 41 | fvmpt2 6291 |
. . . . . . . . . . . . . 14
|
74 | 67, 72, 73 | syl2anc 693 |
. . . . . . . . . . . . 13
|
75 | | elioo4g 12234 |
. . . . . . . . . . . . . . . . . . . . 21
|
76 | 75 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . 20
|
77 | 76 | simpld 475 |
. . . . . . . . . . . . . . . . . . 19
|
78 | 77 | simp1d 1073 |
. . . . . . . . . . . . . . . . . 18
|
79 | | elioore 12205 |
. . . . . . . . . . . . . . . . . . 19
|
80 | 79 | rexrd 10089 |
. . . . . . . . . . . . . . . . . 18
|
81 | | eliooord 12233 |
. . . . . . . . . . . . . . . . . . 19
|
82 | 81 | simpld 475 |
. . . . . . . . . . . . . . . . . 18
|
83 | | xrltne 11994 |
. . . . . . . . . . . . . . . . . 18
|
84 | 78, 80, 82, 83 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
85 | 84 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
86 | 85 | neneqd 2799 |
. . . . . . . . . . . . . . 15
|
87 | 86 | iffalsed 4097 |
. . . . . . . . . . . . . 14
|
88 | 81 | simprd 479 |
. . . . . . . . . . . . . . . . . 18
|
89 | 79, 88 | ltned 10173 |
. . . . . . . . . . . . . . . . 17
|
90 | 89 | neneqd 2799 |
. . . . . . . . . . . . . . . 16
|
91 | 90 | iffalsed 4097 |
. . . . . . . . . . . . . . 15
|
92 | 91 | adantl 482 |
. . . . . . . . . . . . . 14
|
93 | 87, 92 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
94 | 65, 74, 93 | 3eqtrd 2660 |
. . . . . . . . . . . 12
|
95 | 1, 94 | mpteq2da 4743 |
. . . . . . . . . . 11
|
96 | 51, 63, 95 | 3eqtrd 2660 |
. . . . . . . . . 10
|
97 | 36 | feqmptd 6249 |
. . . . . . . . . . 11
|
98 | | ioosscn 39716 |
. . . . . . . . . . . . 13
|
99 | 98 | a1i 11 |
. . . . . . . . . . . 12
|
100 | | ssid 3624 |
. . . . . . . . . . . 12
|
101 | | eqid 2622 |
. . . . . . . . . . . . 13
ℂfld ℂfld |
102 | | eqid 2622 |
. . . . . . . . . . . . 13
ℂfld ↾t ℂfld
↾t |
103 | 101 | cnfldtop 22587 |
. . . . . . . . . . . . . . 15
ℂfld |
104 | | unicntop 22589 |
. . . . . . . . . . . . . . . 16
ℂfld |
105 | 104 | restid 16094 |
. . . . . . . . . . . . . . 15
ℂfld ℂfld
↾t ℂfld |
106 | 103, 105 | ax-mp 5 |
. . . . . . . . . . . . . 14
ℂfld ↾t ℂfld |
107 | 106 | eqcomi 2631 |
. . . . . . . . . . . . 13
ℂfld ℂfld ↾t |
108 | 101, 102,
107 | cncfcn 22712 |
. . . . . . . . . . . 12
ℂfld
↾t ℂfld |
109 | 99, 100, 108 | sylancl 694 |
. . . . . . . . . . 11
ℂfld ↾t ℂfld |
110 | 34, 97, 109 | 3eltr3d 2715 |
. . . . . . . . . 10
ℂfld
↾t ℂfld |
111 | 96, 110 | eqeltrd 2701 |
. . . . . . . . 9
ℂfld ↾t ℂfld |
112 | 104 | restuni 20966 |
. . . . . . . . . . 11
ℂfld
ℂfld
↾t |
113 | 103, 98, 112 | mp2an 708 |
. . . . . . . . . 10
ℂfld ↾t |
114 | 113 | cncnpi 21082 |
. . . . . . . . 9
ℂfld ↾t ℂfld ℂfld ↾t ℂfld |
115 | 111, 114 | sylan 488 |
. . . . . . . 8
ℂfld ↾t ℂfld |
116 | 103 | a1i 11 |
. . . . . . . . . . . 12
ℂfld |
117 | 48 | a1i 11 |
. . . . . . . . . . . 12
|
118 | | ovex 6678 |
. . . . . . . . . . . . 13
|
119 | 118 | a1i 11 |
. . . . . . . . . . . 12
|
120 | | restabs 20969 |
. . . . . . . . . . . 12
ℂfld
ℂfld
↾t ↾t ℂfld ↾t |
121 | 116, 117,
119, 120 | syl3anc 1326 |
. . . . . . . . . . 11
ℂfld
↾t ↾t ℂfld ↾t |
122 | 121 | eqcomd 2628 |
. . . . . . . . . 10
ℂfld ↾t ℂfld
↾t ↾t |
123 | 122 | oveq1d 6665 |
. . . . . . . . 9
ℂfld
↾t ℂfld ℂfld ↾t ↾t ℂfld |
124 | 123 | fveq1d 6193 |
. . . . . . . 8
ℂfld
↾t ℂfld ℂfld ↾t ↾t ℂfld |
125 | 115, 124 | eleqtrd 2703 |
. . . . . . 7
ℂfld ↾t
↾t ℂfld |
126 | | resttop 20964 |
. . . . . . . . . 10
ℂfld
ℂfld
↾t |
127 | 103, 118,
126 | mp2an 708 |
. . . . . . . . 9
ℂfld ↾t |
128 | 127 | a1i 11 |
. . . . . . . 8
ℂfld ↾t |
129 | 48 | a1i 11 |
. . . . . . . . . 10
|
130 | 18, 21 | iccssred 39727 |
. . . . . . . . . . . 12
|
131 | | ax-resscn 9993 |
. . . . . . . . . . . 12
|
132 | 130, 131 | syl6ss 3615 |
. . . . . . . . . . 11
|
133 | 104 | restuni 20966 |
. . . . . . . . . . 11
ℂfld
ℂfld
↾t |
134 | 103, 132,
133 | sylancr 695 |
. . . . . . . . . 10
ℂfld
↾t |
135 | 129, 134 | sseqtrd 3641 |
. . . . . . . . 9
ℂfld
↾t |
136 | 135 | adantr 481 |
. . . . . . . 8
ℂfld
↾t |
137 | | retop 22565 |
. . . . . . . . . . . . . 14
|
138 | 137 | a1i 11 |
. . . . . . . . . . . . 13
|
139 | | ioossre 12235 |
. . . . . . . . . . . . . . 15
|
140 | | difss 3737 |
. . . . . . . . . . . . . . 15
|
141 | 139, 140 | unssi 3788 |
. . . . . . . . . . . . . 14
|
142 | 141 | a1i 11 |
. . . . . . . . . . . . 13
|
143 | | ssun1 3776 |
. . . . . . . . . . . . . 14
|
144 | 143 | a1i 11 |
. . . . . . . . . . . . 13
|
145 | | uniretop 22566 |
. . . . . . . . . . . . . 14
|
146 | 145 | ntrss 20859 |
. . . . . . . . . . . . 13
|
147 | 138, 142,
144, 146 | syl3anc 1326 |
. . . . . . . . . . . 12
|
148 | | simpr 477 |
. . . . . . . . . . . . 13
|
149 | | ioontr 39736 |
. . . . . . . . . . . . 13
|
150 | 148, 149 | syl6eleqr 2712 |
. . . . . . . . . . . 12
|
151 | 147, 150 | sseldd 3604 |
. . . . . . . . . . 11
|
152 | 48, 148 | sseldi 3601 |
. . . . . . . . . . 11
|
153 | 151, 152 | elind 3798 |
. . . . . . . . . 10
|
154 | 130 | adantr 481 |
. . . . . . . . . . 11
|
155 | | eqid 2622 |
. . . . . . . . . . . 12
↾t
↾t |
156 | 145, 155 | restntr 20986 |
. . . . . . . . . . 11
↾t
|
157 | 138, 154,
117, 156 | syl3anc 1326 |
. . . . . . . . . 10
↾t |
158 | 153, 157 | eleqtrrd 2704 |
. . . . . . . . 9
↾t |
159 | 101 | tgioo2 22606 |
. . . . . . . . . . . . . . 15
ℂfld
↾t |
160 | 159 | a1i 11 |
. . . . . . . . . . . . . 14
ℂfld ↾t |
161 | 160 | oveq1d 6665 |
. . . . . . . . . . . . 13
↾t ℂfld
↾t
↾t |
162 | 103 | a1i 11 |
. . . . . . . . . . . . . 14
ℂfld
|
163 | | reex 10027 |
. . . . . . . . . . . . . . 15
|
164 | 163 | a1i 11 |
. . . . . . . . . . . . . 14
|
165 | | restabs 20969 |
. . . . . . . . . . . . . 14
ℂfld
ℂfld
↾t
↾t ℂfld
↾t |
166 | 162, 130,
164, 165 | syl3anc 1326 |
. . . . . . . . . . . . 13
ℂfld ↾t ↾t ℂfld ↾t |
167 | 161, 166 | eqtrd 2656 |
. . . . . . . . . . . 12
↾t ℂfld
↾t |
168 | 167 | fveq2d 6195 |
. . . . . . . . . . 11
↾t ℂfld
↾t |
169 | 168 | fveq1d 6193 |
. . . . . . . . . 10
↾t ℂfld
↾t |
170 | 169 | adantr 481 |
. . . . . . . . 9
↾t ℂfld
↾t |
171 | 158, 170 | eleqtrd 2703 |
. . . . . . . 8
ℂfld
↾t |
172 | 134 | feq2d 6031 |
. . . . . . . . . 10
ℂfld
↾t |
173 | 42, 172 | mpbid 222 |
. . . . . . . . 9
ℂfld
↾t |
174 | 173 | adantr 481 |
. . . . . . . 8
ℂfld
↾t |
175 | | eqid 2622 |
. . . . . . . . 9
ℂfld
↾t ℂfld ↾t |
176 | 175, 104 | cnprest 21093 |
. . . . . . . 8
ℂfld ↾t ℂfld
↾t ℂfld
↾t ℂfld ↾t
ℂfld ↾t ℂfld ℂfld ↾t ↾t ℂfld |
177 | 128, 136,
171, 174, 176 | syl22anc 1327 |
. . . . . . 7
ℂfld ↾t ℂfld ℂfld ↾t ↾t ℂfld |
178 | 125, 177 | mpbird 247 |
. . . . . 6
ℂfld ↾t ℂfld |
179 | | elpri 4197 |
. . . . . . 7
|
180 | | lbicc2 12288 |
. . . . . . . . . . . . . 14
|
181 | 19, 22, 25, 180 | syl3anc 1326 |
. . . . . . . . . . . . 13
|
182 | | iftrue 4092 |
. . . . . . . . . . . . . 14
|
183 | 182, 41 | fvmptg 6280 |
. . . . . . . . . . . . 13
lim |
184 | 181, 3, 183 | syl2anc 693 |
. . . . . . . . . . . 12
|
185 | 97 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
|
186 | 96, 185 | eqtr2d 2657 |
. . . . . . . . . . . . . . 15
|
187 | 186 | oveq1d 6665 |
. . . . . . . . . . . . . 14
lim
lim |
188 | 3, 187 | eleqtrd 2703 |
. . . . . . . . . . . . 13
lim |
189 | 18, 21, 24, 42 | limciccioolb 39853 |
. . . . . . . . . . . . 13
lim lim |
190 | 188, 189 | eleqtrd 2703 |
. . . . . . . . . . . 12
lim |
191 | 184, 190 | eqeltrd 2701 |
. . . . . . . . . . 11
lim |
192 | | eqid 2622 |
. . . . . . . . . . . . 13
ℂfld ↾t ℂfld
↾t |
193 | 101, 192 | cnplimc 23651 |
. . . . . . . . . . . 12
ℂfld
↾t ℂfld lim |
194 | 132, 181,
193 | syl2anc 693 |
. . . . . . . . . . 11
ℂfld ↾t ℂfld lim |
195 | 42, 191, 194 | mpbir2and 957 |
. . . . . . . . . 10
ℂfld
↾t ℂfld |
196 | 195 | adantr 481 |
. . . . . . . . 9
ℂfld ↾t ℂfld |
197 | | fveq2 6191 |
. . . . . . . . . . 11
ℂfld ↾t ℂfld ℂfld
↾t ℂfld |
198 | 197 | eqcomd 2628 |
. . . . . . . . . 10
ℂfld ↾t ℂfld ℂfld
↾t ℂfld |
199 | 198 | adantl 482 |
. . . . . . . . 9
ℂfld ↾t ℂfld ℂfld
↾t ℂfld |
200 | 196, 199 | eleqtrd 2703 |
. . . . . . . 8
ℂfld ↾t ℂfld |
201 | 21 | leidd 10594 |
. . . . . . . . . . . . . . 15
|
202 | 18, 21, 21, 25, 201 | eliccd 39726 |
. . . . . . . . . . . . . 14
|
203 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
|
204 | 203 | iftruei 4093 |
. . . . . . . . . . . . . . . . 17
|
205 | 204, 8 | syl5eqel 2705 |
. . . . . . . . . . . . . . . 16
|
206 | 4, 205 | ifcld 4131 |
. . . . . . . . . . . . . . 15
|
207 | 202, 206 | jca 554 |
. . . . . . . . . . . . . 14
|
208 | | nfv 1843 |
. . . . . . . . . . . . . . . 16
|
209 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . 18
|
210 | 53, 209 | nffv 6198 |
. . . . . . . . . . . . . . . . 17
|
211 | 210 | nfeq1 2778 |
. . . . . . . . . . . . . . . 16
|
212 | 208, 211 | nfim 1825 |
. . . . . . . . . . . . . . 15
|
213 | | eleq1 2689 |
. . . . . . . . . . . . . . . . 17
|
214 | 182 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
215 | | eqtr2 2642 |
. . . . . . . . . . . . . . . . . . . . 21
|
216 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . . . 22
|
217 | 216 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . 21
|
218 | 215, 217 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
219 | 214, 218 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
|
220 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . . 21
|
221 | 220 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
222 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . . 21
|
223 | 222 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
224 | | df-ne 2795 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
225 | | pm13.18 2875 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
226 | 224, 225 | sylan2br 493 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
227 | 226 | neneqd 2799 |
. . . . . . . . . . . . . . . . . . . . . 22
|
228 | 227 | iffalsed 4097 |
. . . . . . . . . . . . . . . . . . . . 21
|
229 | 228, 204 | syl6req 2673 |
. . . . . . . . . . . . . . . . . . . 20
|
230 | 221, 223,
229 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . . 19
|
231 | 219, 230 | pm2.61dan 832 |
. . . . . . . . . . . . . . . . . 18
|
232 | 231 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
|
233 | 213, 232 | anbi12d 747 |
. . . . . . . . . . . . . . . 16
|
234 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
235 | 234, 231 | eqeq12d 2637 |
. . . . . . . . . . . . . . . 16
|
236 | 233, 235 | imbi12d 334 |
. . . . . . . . . . . . . . 15
|
237 | 212, 236,
73 | vtoclg1f 3265 |
. . . . . . . . . . . . . 14
|
238 | 202, 207,
237 | sylc 65 |
. . . . . . . . . . . . 13
|
239 | 18, 24 | gtned 10172 |
. . . . . . . . . . . . . . 15
|
240 | 239 | neneqd 2799 |
. . . . . . . . . . . . . 14
|
241 | 240 | iffalsed 4097 |
. . . . . . . . . . . . 13
|
242 | 204 | a1i 11 |
. . . . . . . . . . . . 13
|
243 | 238, 241,
242 | 3eqtrd 2660 |
. . . . . . . . . . . 12
|
244 | 186 | oveq1d 6665 |
. . . . . . . . . . . . . 14
lim
lim |
245 | 7, 244 | eleqtrd 2703 |
. . . . . . . . . . . . 13
lim |
246 | 18, 21, 24, 42 | limcicciooub 39869 |
. . . . . . . . . . . . 13
lim lim |
247 | 245, 246 | eleqtrd 2703 |
. . . . . . . . . . . 12
lim |
248 | 243, 247 | eqeltrd 2701 |
. . . . . . . . . . 11
lim |
249 | 101, 192 | cnplimc 23651 |
. . . . . . . . . . . 12
ℂfld
↾t ℂfld lim |
250 | 132, 202,
249 | syl2anc 693 |
. . . . . . . . . . 11
ℂfld ↾t ℂfld lim |
251 | 42, 248, 250 | mpbir2and 957 |
. . . . . . . . . 10
ℂfld
↾t ℂfld |
252 | 251 | adantr 481 |
. . . . . . . . 9
ℂfld ↾t ℂfld |
253 | | fveq2 6191 |
. . . . . . . . . . 11
ℂfld ↾t ℂfld ℂfld
↾t ℂfld |
254 | 253 | eqcomd 2628 |
. . . . . . . . . 10
ℂfld ↾t ℂfld ℂfld
↾t ℂfld |
255 | 254 | adantl 482 |
. . . . . . . . 9
ℂfld ↾t ℂfld ℂfld
↾t ℂfld |
256 | 252, 255 | eleqtrd 2703 |
. . . . . . . 8
ℂfld ↾t ℂfld |
257 | 200, 256 | jaodan 826 |
. . . . . . 7
ℂfld
↾t ℂfld |
258 | 179, 257 | sylan2 491 |
. . . . . 6
ℂfld ↾t ℂfld |
259 | 178, 258 | jaodan 826 |
. . . . 5
ℂfld
↾t ℂfld |
260 | 47, 259 | syldan 487 |
. . . 4
ℂfld ↾t ℂfld |
261 | 260 | ralrimiva 2966 |
. . 3
ℂfld
↾t ℂfld |
262 | 101 | cnfldtopon 22586 |
. . . . 5
ℂfld TopOn |
263 | | resttopon 20965 |
. . . . 5
ℂfld
TopOn
ℂfld ↾t TopOn |
264 | 262, 132,
263 | sylancr 695 |
. . . 4
ℂfld
↾t TopOn |
265 | | cncnp 21084 |
. . . 4
ℂfld
↾t TopOn ℂfld
TopOn ℂfld
↾t ℂfld
ℂfld
↾t ℂfld |
266 | 264, 262,
265 | sylancl 694 |
. . 3
ℂfld
↾t ℂfld
ℂfld
↾t ℂfld |
267 | 42, 261, 266 | mpbir2and 957 |
. 2
ℂfld
↾t ℂfld |
268 | 101, 192,
107 | cncfcn 22712 |
. . 3
ℂfld
↾t ℂfld |
269 | 132, 100,
268 | sylancl 694 |
. 2
ℂfld ↾t ℂfld |
270 | 267, 269 | eleqtrrd 2704 |
1
|