Step | Hyp | Ref
| Expression |
1 | | limccnp2.h |
. . . . . . . . . . 11
|
2 | | eqid 2622 |
. . . . . . . . . . . 12
|
3 | 2 | cnprcl 21049 |
. . . . . . . . . . 11
|
4 | 1, 3 | syl 17 |
. . . . . . . . . 10
|
5 | | limccnp2.j |
. . . . . . . . . . . 12
↾t |
6 | | limccnp2.k |
. . . . . . . . . . . . . . 15
ℂfld |
7 | 6 | cnfldtopon 22586 |
. . . . . . . . . . . . . 14
TopOn |
8 | | txtopon 21394 |
. . . . . . . . . . . . . 14
TopOn
TopOn
TopOn |
9 | 7, 7, 8 | mp2an 708 |
. . . . . . . . . . . . 13
TopOn |
10 | | limccnp2.x |
. . . . . . . . . . . . . 14
|
11 | | limccnp2.y |
. . . . . . . . . . . . . 14
|
12 | | xpss12 5225 |
. . . . . . . . . . . . . 14
|
13 | 10, 11, 12 | syl2anc 693 |
. . . . . . . . . . . . 13
|
14 | | resttopon 20965 |
. . . . . . . . . . . . 13
TopOn
↾t TopOn |
15 | 9, 13, 14 | sylancr 695 |
. . . . . . . . . . . 12
↾t TopOn |
16 | 5, 15 | syl5eqel 2705 |
. . . . . . . . . . 11
TopOn
|
17 | | toponuni 20719 |
. . . . . . . . . . 11
TopOn |
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
|
19 | 4, 18 | eleqtrrd 2704 |
. . . . . . . . 9
|
20 | | opelxp 5146 |
. . . . . . . . 9
|
21 | 19, 20 | sylib 208 |
. . . . . . . 8
|
22 | 21 | simpld 475 |
. . . . . . 7
|
23 | 22 | ad2antrr 762 |
. . . . . 6
|
24 | | simpll 790 |
. . . . . . 7
|
25 | | simpr 477 |
. . . . . . . . . . . 12
|
26 | | elun 3753 |
. . . . . . . . . . . 12
|
27 | 25, 26 | sylib 208 |
. . . . . . . . . . 11
|
28 | 27 | ord 392 |
. . . . . . . . . 10
|
29 | | elsni 4194 |
. . . . . . . . . 10
|
30 | 28, 29 | syl6 35 |
. . . . . . . . 9
|
31 | 30 | con1d 139 |
. . . . . . . 8
|
32 | 31 | imp 445 |
. . . . . . 7
|
33 | | limccnp2.r |
. . . . . . 7
|
34 | 24, 32, 33 | syl2anc 693 |
. . . . . 6
|
35 | 23, 34 | ifclda 4120 |
. . . . 5
|
36 | 21 | simprd 479 |
. . . . . . 7
|
37 | 36 | ad2antrr 762 |
. . . . . 6
|
38 | | limccnp2.s |
. . . . . . 7
|
39 | 24, 32, 38 | syl2anc 693 |
. . . . . 6
|
40 | 37, 39 | ifclda 4120 |
. . . . 5
|
41 | | opelxpi 5148 |
. . . . 5
|
42 | 35, 40, 41 | syl2anc 693 |
. . . 4
|
43 | | eqidd 2623 |
. . . 4
|
44 | 7 | a1i 11 |
. . . . . 6
TopOn |
45 | | cnpf2 21054 |
. . . . . 6
TopOn
TopOn
|
46 | 16, 44, 1, 45 | syl3anc 1326 |
. . . . 5
|
47 | 46 | feqmptd 6249 |
. . . 4
|
48 | | fveq2 6191 |
. . . . 5
|
49 | | df-ov 6653 |
. . . . . 6
|
50 | | ovif12 6739 |
. . . . . 6
|
51 | 49, 50 | eqtr3i 2646 |
. . . . 5
|
52 | 48, 51 | syl6eq 2672 |
. . . 4
|
53 | 42, 43, 47, 52 | fmptco 6396 |
. . 3
|
54 | | eqid 2622 |
. . . . . . . . . . 11
|
55 | 54, 33 | dmmptd 6024 |
. . . . . . . . . 10
|
56 | | limccnp2.c |
. . . . . . . . . . . 12
lim |
57 | | limcrcl 23638 |
. . . . . . . . . . . 12
lim
|
58 | 56, 57 | syl 17 |
. . . . . . . . . . 11
|
59 | 58 | simp2d 1074 |
. . . . . . . . . 10
|
60 | 55, 59 | eqsstr3d 3640 |
. . . . . . . . 9
|
61 | 58 | simp3d 1075 |
. . . . . . . . . 10
|
62 | 61 | snssd 4340 |
. . . . . . . . 9
|
63 | 60, 62 | unssd 3789 |
. . . . . . . 8
|
64 | | resttopon 20965 |
. . . . . . . 8
TopOn
↾t TopOn |
65 | 7, 63, 64 | sylancr 695 |
. . . . . . 7
↾t TopOn
|
66 | | ssun2 3777 |
. . . . . . . 8
|
67 | | snssg 4327 |
. . . . . . . . 9
|
68 | 61, 67 | syl 17 |
. . . . . . . 8
|
69 | 66, 68 | mpbiri 248 |
. . . . . . 7
|
70 | 10 | adantr 481 |
. . . . . . . . . 10
|
71 | 70, 33 | sseldd 3604 |
. . . . . . . . 9
|
72 | | eqid 2622 |
. . . . . . . . 9
↾t
↾t |
73 | 60, 61, 71, 72, 6 | limcmpt 23647 |
. . . . . . . 8
lim
↾t |
74 | 56, 73 | mpbid 222 |
. . . . . . 7
↾t |
75 | | limccnp2.d |
. . . . . . . 8
lim |
76 | 11 | adantr 481 |
. . . . . . . . . 10
|
77 | 76, 38 | sseldd 3604 |
. . . . . . . . 9
|
78 | 60, 61, 77, 72, 6 | limcmpt 23647 |
. . . . . . . 8
lim
↾t |
79 | 75, 78 | mpbid 222 |
. . . . . . 7
↾t |
80 | 65, 44, 44, 69, 74, 79 | txcnp 21423 |
. . . . . 6
↾t |
81 | 9 | topontopi 20720 |
. . . . . . . 8
|
82 | 81 | a1i 11 |
. . . . . . 7
|
83 | | eqid 2622 |
. . . . . . . . 9
|
84 | 42, 83 | fmptd 6385 |
. . . . . . . 8
|
85 | | toponuni 20719 |
. . . . . . . . . 10
↾t TopOn
↾t |
86 | 65, 85 | syl 17 |
. . . . . . . . 9
↾t |
87 | 86 | feq2d 6031 |
. . . . . . . 8
↾t |
88 | 84, 87 | mpbid 222 |
. . . . . . 7
↾t |
89 | | eqid 2622 |
. . . . . . . 8
↾t
↾t |
90 | 9 | toponunii 20721 |
. . . . . . . 8
|
91 | 89, 90 | cnprest2 21094 |
. . . . . . 7
↾t
↾t
↾t
↾t |
92 | 82, 88, 13, 91 | syl3anc 1326 |
. . . . . 6
↾t
↾t
↾t |
93 | 80, 92 | mpbid 222 |
. . . . 5
↾t
↾t |
94 | 5 | oveq2i 6661 |
. . . . . 6
↾t
↾t ↾t |
95 | 94 | fveq1i 6192 |
. . . . 5
↾t ↾t ↾t |
96 | 93, 95 | syl6eleqr 2712 |
. . . 4
↾t |
97 | | iftrue 4092 |
. . . . . . . . 9
|
98 | | iftrue 4092 |
. . . . . . . . 9
|
99 | 97, 98 | opeq12d 4410 |
. . . . . . . 8
|
100 | | opex 4932 |
. . . . . . . 8
|
101 | 99, 83, 100 | fvmpt 6282 |
. . . . . . 7
|
102 | 69, 101 | syl 17 |
. . . . . 6
|
103 | 102 | fveq2d 6195 |
. . . . 5
|
104 | 1, 103 | eleqtrrd 2704 |
. . . 4
|
105 | | cnpco 21071 |
. . . 4
↾t
↾t |
106 | 96, 104, 105 | syl2anc 693 |
. . 3
↾t |
107 | 53, 106 | eqeltrrd 2702 |
. 2
↾t |
108 | 46 | adantr 481 |
. . . 4
|
109 | 108, 33, 38 | fovrnd 6806 |
. . 3
|
110 | 60, 61, 109, 72, 6 | limcmpt 23647 |
. 2
lim
↾t |
111 | 107, 110 | mpbird 247 |
1
lim |