Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . 3
|
2 | | poimir.i |
. . 3
|
3 | | poimir.r |
. . 3
|
4 | | elmapfn 7880 |
. . . . . . . 8
|
5 | 4, 2 | eleq2s 2719 |
. . . . . . 7
|
6 | 5 | adantl 482 |
. . . . . 6
|
7 | | broucube.1 |
. . . . . . . . 9
↾t ↾t |
8 | | ovex 6678 |
. . . . . . . . . . . . 13
|
9 | | retopon 22567 |
. . . . . . . . . . . . 13
TopOn |
10 | 3 | pttoponconst 21400 |
. . . . . . . . . . . . 13
TopOn
TopOn |
11 | 8, 9, 10 | mp2an 708 |
. . . . . . . . . . . 12
TopOn |
12 | | reex 10027 |
. . . . . . . . . . . . . 14
|
13 | | unitssre 12319 |
. . . . . . . . . . . . . 14
|
14 | | mapss 7900 |
. . . . . . . . . . . . . 14
|
15 | 12, 13, 14 | mp2an 708 |
. . . . . . . . . . . . 13
|
16 | 2, 15 | eqsstri 3635 |
. . . . . . . . . . . 12
|
17 | | resttopon 20965 |
. . . . . . . . . . . 12
TopOn
↾t TopOn |
18 | 11, 16, 17 | mp2an 708 |
. . . . . . . . . . 11
↾t TopOn |
19 | 18 | toponunii 20721 |
. . . . . . . . . 10
↾t |
20 | 19, 19 | cnf 21050 |
. . . . . . . . 9
↾t ↾t |
21 | 7, 20 | syl 17 |
. . . . . . . 8
|
22 | 21 | ffvelrnda 6359 |
. . . . . . 7
|
23 | | elmapfn 7880 |
. . . . . . . 8
|
24 | 23, 2 | eleq2s 2719 |
. . . . . . 7
|
25 | 22, 24 | syl 17 |
. . . . . 6
|
26 | | ovexd 6680 |
. . . . . 6
|
27 | | inidm 3822 |
. . . . . 6
|
28 | | eqidd 2623 |
. . . . . 6
|
29 | | eqidd 2623 |
. . . . . 6
|
30 | 6, 25, 26, 26, 27, 28, 29 | offval 6904 |
. . . . 5
|
31 | 30 | mpteq2dva 4744 |
. . . 4
|
32 | 18 | a1i 11 |
. . . . 5
↾t TopOn |
33 | | ovexd 6680 |
. . . . 5
|
34 | | retop 22565 |
. . . . . . 7
|
35 | 34 | fconst6 6095 |
. . . . . 6
|
36 | 35 | a1i 11 |
. . . . 5
|
37 | 18 | a1i 11 |
. . . . . . . 8
↾t TopOn |
38 | | eqid 2622 |
. . . . . . . . . . . 12
ℂfld ℂfld |
39 | 38 | cnfldtop 22587 |
. . . . . . . . . . 11
ℂfld |
40 | | cnrest2r 21091 |
. . . . . . . . . . 11
ℂfld
↾t ℂfld
↾t ↾t ℂfld |
41 | 39, 40 | ax-mp 5 |
. . . . . . . . . 10
↾t ℂfld
↾t ↾t ℂfld |
42 | | resmpt 5449 |
. . . . . . . . . . . . 13
|
43 | 16, 42 | ax-mp 5 |
. . . . . . . . . . . 12
|
44 | 11 | toponunii 20721 |
. . . . . . . . . . . . . . 15
|
45 | 44, 3 | ptpjcn 21414 |
. . . . . . . . . . . . . 14
|
46 | 8, 35, 45 | mp3an12 1414 |
. . . . . . . . . . . . 13
|
47 | 44 | cnrest 21089 |
. . . . . . . . . . . . 13
↾t |
48 | 46, 16, 47 | sylancl 694 |
. . . . . . . . . . . 12
↾t |
49 | 43, 48 | syl5eqelr 2706 |
. . . . . . . . . . 11
↾t |
50 | | fvex 6201 |
. . . . . . . . . . . . . 14
|
51 | 50 | fvconst2 6469 |
. . . . . . . . . . . . 13
|
52 | 38 | tgioo2 22606 |
. . . . . . . . . . . . 13
ℂfld
↾t |
53 | 51, 52 | syl6eq 2672 |
. . . . . . . . . . . 12
ℂfld ↾t |
54 | 53 | oveq2d 6666 |
. . . . . . . . . . 11
↾t
↾t ℂfld
↾t |
55 | 49, 54 | eleqtrd 2703 |
. . . . . . . . . 10
↾t ℂfld
↾t |
56 | 41, 55 | sseldi 3601 |
. . . . . . . . 9
↾t ℂfld |
57 | 56 | adantl 482 |
. . . . . . . 8
↾t ℂfld |
58 | 21 | feqmptd 6249 |
. . . . . . . . . . 11
|
59 | 58, 7 | eqeltrrd 2702 |
. . . . . . . . . 10
↾t ↾t |
60 | 59 | adantr 481 |
. . . . . . . . 9
↾t ↾t |
61 | | fveq1 6190 |
. . . . . . . . . . 11
|
62 | 61 | cbvmptv 4750 |
. . . . . . . . . 10
|
63 | 62, 57 | syl5eqelr 2706 |
. . . . . . . . 9
↾t ℂfld |
64 | | fveq1 6190 |
. . . . . . . . 9
|
65 | 37, 60, 37, 63, 64 | cnmpt11 21466 |
. . . . . . . 8
↾t ℂfld |
66 | 38 | subcn 22669 |
. . . . . . . . 9
ℂfld ℂfld ℂfld |
67 | 66 | a1i 11 |
. . . . . . . 8
ℂfld ℂfld ℂfld |
68 | 37, 57, 65, 67 | cnmpt12f 21469 |
. . . . . . 7
↾t ℂfld |
69 | | elmapi 7879 |
. . . . . . . . . . . . . . 15
|
70 | 69, 2 | eleq2s 2719 |
. . . . . . . . . . . . . 14
|
71 | 70 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
|
72 | 13, 71 | sseldi 3601 |
. . . . . . . . . . . 12
|
73 | 72 | adantll 750 |
. . . . . . . . . . 11
|
74 | | elmapi 7879 |
. . . . . . . . . . . . . . 15
|
75 | 74, 2 | eleq2s 2719 |
. . . . . . . . . . . . . 14
|
76 | 22, 75 | syl 17 |
. . . . . . . . . . . . 13
|
77 | 76 | ffvelrnda 6359 |
. . . . . . . . . . . 12
|
78 | 13, 77 | sseldi 3601 |
. . . . . . . . . . 11
|
79 | 73, 78 | resubcld 10458 |
. . . . . . . . . 10
|
80 | 79 | an32s 846 |
. . . . . . . . 9
|
81 | | eqid 2622 |
. . . . . . . . 9
|
82 | 80, 81 | fmptd 6385 |
. . . . . . . 8
|
83 | | frn 6053 |
. . . . . . . 8
|
84 | 38 | cnfldtopon 22586 |
. . . . . . . . 9
ℂfld TopOn |
85 | | ax-resscn 9993 |
. . . . . . . . 9
|
86 | | cnrest2 21090 |
. . . . . . . . 9
ℂfld
TopOn
↾t ℂfld
↾t ℂfld ↾t |
87 | 84, 85, 86 | mp3an13 1415 |
. . . . . . . 8
↾t ℂfld
↾t ℂfld ↾t |
88 | 82, 83, 87 | 3syl 18 |
. . . . . . 7
↾t ℂfld
↾t ℂfld ↾t |
89 | 68, 88 | mpbid 222 |
. . . . . 6
↾t ℂfld
↾t |
90 | 54 | adantl 482 |
. . . . . 6
↾t
↾t ℂfld
↾t |
91 | 89, 90 | eleqtrrd 2704 |
. . . . 5
↾t |
92 | 3, 32, 33, 36, 91 | ptcn 21430 |
. . . 4
↾t |
93 | 31, 92 | eqeltrd 2701 |
. . 3
↾t |
94 | | simpr2 1068 |
. . . . . 6
|
95 | | id 22 |
. . . . . . . . 9
|
96 | | fveq2 6191 |
. . . . . . . . 9
|
97 | 95, 96 | oveq12d 6668 |
. . . . . . . 8
|
98 | | eqid 2622 |
. . . . . . . 8
|
99 | | ovex 6678 |
. . . . . . . 8
|
100 | 97, 98, 99 | fvmpt 6282 |
. . . . . . 7
|
101 | 100 | fveq1d 6193 |
. . . . . 6
|
102 | 94, 101 | syl 17 |
. . . . 5
|
103 | | elmapfn 7880 |
. . . . . . . . . . . 12
|
104 | 103, 2 | eleq2s 2719 |
. . . . . . . . . . 11
|
105 | 104 | adantl 482 |
. . . . . . . . . 10
|
106 | 21 | ffvelrnda 6359 |
. . . . . . . . . . . 12
|
107 | | elmapfn 7880 |
. . . . . . . . . . . . 13
|
108 | 107, 2 | eleq2s 2719 |
. . . . . . . . . . . 12
|
109 | 106, 108 | syl 17 |
. . . . . . . . . . 11
|
110 | 109 | adantlr 751 |
. . . . . . . . . 10
|
111 | | ovexd 6680 |
. . . . . . . . . 10
|
112 | | simpllr 799 |
. . . . . . . . . 10
|
113 | | eqidd 2623 |
. . . . . . . . . 10
|
114 | 105, 110,
111, 111, 27, 112, 113 | ofval 6906 |
. . . . . . . . 9
|
115 | | df-neg 10269 |
. . . . . . . . 9
|
116 | 114, 115 | syl6eqr 2674 |
. . . . . . . 8
|
117 | 116 | exp41 638 |
. . . . . . 7
|
118 | 117 | com24 95 |
. . . . . 6
|
119 | 118 | 3imp2 1282 |
. . . . 5
|
120 | 102, 119 | eqtrd 2656 |
. . . 4
|
121 | | elmapi 7879 |
. . . . . . . . . . . 12
|
122 | 121, 2 | eleq2s 2719 |
. . . . . . . . . . 11
|
123 | 106, 122 | syl 17 |
. . . . . . . . . 10
|
124 | 123 | ffvelrnda 6359 |
. . . . . . . . 9
|
125 | | 0xr 10086 |
. . . . . . . . . 10
|
126 | | 1re 10039 |
. . . . . . . . . . 11
|
127 | 126 | rexri 10097 |
. . . . . . . . . 10
|
128 | | iccgelb 12230 |
. . . . . . . . . 10
|
129 | 125, 127,
128 | mp3an12 1414 |
. . . . . . . . 9
|
130 | 124, 129 | syl 17 |
. . . . . . . 8
|
131 | 13, 124 | sseldi 3601 |
. . . . . . . . 9
|
132 | 131 | le0neg2d 10600 |
. . . . . . . 8
|
133 | 130, 132 | mpbid 222 |
. . . . . . 7
|
134 | 133 | an32s 846 |
. . . . . 6
|
135 | 134 | anasss 679 |
. . . . 5
|
136 | 135 | 3adantr3 1222 |
. . . 4
|
137 | 120, 136 | eqbrtrd 4675 |
. . 3
|
138 | | iccleub 12229 |
. . . . . . . . . 10
|
139 | 125, 127,
138 | mp3an12 1414 |
. . . . . . . . 9
|
140 | 124, 139 | syl 17 |
. . . . . . . 8
|
141 | | 1red 10055 |
. . . . . . . . 9
|
142 | 141, 131 | subge0d 10617 |
. . . . . . . 8
|
143 | 140, 142 | mpbird 247 |
. . . . . . 7
|
144 | 143 | an32s 846 |
. . . . . 6
|
145 | 144 | anasss 679 |
. . . . 5
|
146 | 145 | 3adantr3 1222 |
. . . 4
|
147 | | simpr2 1068 |
. . . . . 6
|
148 | 147, 101 | syl 17 |
. . . . 5
|
149 | 104 | adantl 482 |
. . . . . . . . 9
|
150 | 109 | adantlr 751 |
. . . . . . . . 9
|
151 | | ovexd 6680 |
. . . . . . . . 9
|
152 | | simpllr 799 |
. . . . . . . . 9
|
153 | | eqidd 2623 |
. . . . . . . . 9
|
154 | 149, 150,
151, 151, 27, 152, 153 | ofval 6906 |
. . . . . . . 8
|
155 | 154 | exp41 638 |
. . . . . . 7
|
156 | 155 | com24 95 |
. . . . . 6
|
157 | 156 | 3imp2 1282 |
. . . . 5
|
158 | 148, 157 | eqtrd 2656 |
. . . 4
|
159 | 146, 158 | breqtrrd 4681 |
. . 3
|
160 | 1, 2, 3, 93, 137, 159 | poimir 33442 |
. 2
|
161 | | id 22 |
. . . . . . . 8
|
162 | | fveq2 6191 |
. . . . . . . 8
|
163 | 161, 162 | oveq12d 6668 |
. . . . . . 7
|
164 | | ovex 6678 |
. . . . . . 7
|
165 | 163, 98, 164 | fvmpt 6282 |
. . . . . 6
|
166 | 165 | adantl 482 |
. . . . 5
|
167 | 166 | eqeq1d 2624 |
. . . 4
|
168 | | elmapfn 7880 |
. . . . . . . . . . 11
|
169 | 168, 2 | eleq2s 2719 |
. . . . . . . . . 10
|
170 | 169 | adantl 482 |
. . . . . . . . 9
|
171 | 21 | ffvelrnda 6359 |
. . . . . . . . . 10
|
172 | | elmapfn 7880 |
. . . . . . . . . . 11
|
173 | 172, 2 | eleq2s 2719 |
. . . . . . . . . 10
|
174 | 171, 173 | syl 17 |
. . . . . . . . 9
|
175 | | ovexd 6680 |
. . . . . . . . 9
|
176 | | eqidd 2623 |
. . . . . . . . 9
|
177 | | eqidd 2623 |
. . . . . . . . 9
|
178 | 170, 174,
175, 175, 27, 176, 177 | ofval 6906 |
. . . . . . . 8
|
179 | | c0ex 10034 |
. . . . . . . . . 10
|
180 | 179 | fvconst2 6469 |
. . . . . . . . 9
|
181 | 180 | adantl 482 |
. . . . . . . 8
|
182 | 178, 181 | eqeq12d 2637 |
. . . . . . 7
|
183 | 13, 85 | sstri 3612 |
. . . . . . . . . 10
|
184 | | elmapi 7879 |
. . . . . . . . . . . 12
|
185 | 184, 2 | eleq2s 2719 |
. . . . . . . . . . 11
|
186 | 185 | ffvelrnda 6359 |
. . . . . . . . . 10
|
187 | 183, 186 | sseldi 3601 |
. . . . . . . . 9
|
188 | 187 | adantll 750 |
. . . . . . . 8
|
189 | | elmapi 7879 |
. . . . . . . . . . . 12
|
190 | 189, 2 | eleq2s 2719 |
. . . . . . . . . . 11
|
191 | 171, 190 | syl 17 |
. . . . . . . . . 10
|
192 | 191 | ffvelrnda 6359 |
. . . . . . . . 9
|
193 | 183, 192 | sseldi 3601 |
. . . . . . . 8
|
194 | 188, 193 | subeq0ad 10402 |
. . . . . . 7
|
195 | 182, 194 | bitrd 268 |
. . . . . 6
|
196 | 195 | ralbidva 2985 |
. . . . 5
|
197 | 170, 174,
175, 175, 27 | offn 6908 |
. . . . . 6
|
198 | | fnconstg 6093 |
. . . . . . 7
|
199 | 179, 198 | ax-mp 5 |
. . . . . 6
|
200 | | eqfnfv 6311 |
. . . . . 6
|
201 | 197, 199,
200 | sylancl 694 |
. . . . 5
|
202 | | eqfnfv 6311 |
. . . . . 6
|
203 | 170, 174,
202 | syl2anc 693 |
. . . . 5
|
204 | 196, 201,
203 | 3bitr4d 300 |
. . . 4
|
205 | 167, 204 | bitrd 268 |
. . 3
|
206 | 205 | rexbidva 3049 |
. 2
|
207 | 160, 206 | mpbid 222 |
1
|