Step | Hyp | Ref
| Expression |
1 | | df-dv 23631 |
. . . . . . . . . . . . . . . . . . . 20
ℂfld
↾t
lim |
2 | 1 | dmmpt2ssx 7235 |
. . . . . . . . . . . . . . . . . . 19
|
3 | | simpl 473 |
. . . . . . . . . . . . . . . . . . 19
↾t Perf
|
4 | 2, 3 | sseldi 3601 |
. . . . . . . . . . . . . . . . . 18
↾t Perf |
5 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
|
6 | 5 | opeliunxp2 5260 |
. . . . . . . . . . . . . . . . . 18
|
7 | 4, 6 | sylib 208 |
. . . . . . . . . . . . . . . . 17
↾t Perf
|
8 | 7 | simprd 479 |
. . . . . . . . . . . . . . . 16
↾t Perf |
9 | | cnex 10017 |
. . . . . . . . . . . . . . . . 17
|
10 | 7 | simpld 475 |
. . . . . . . . . . . . . . . . 17
↾t Perf |
11 | | elpm2g 7874 |
. . . . . . . . . . . . . . . . 17
|
12 | 9, 10, 11 | sylancr 695 |
. . . . . . . . . . . . . . . 16
↾t Perf
|
13 | 8, 12 | mpbid 222 |
. . . . . . . . . . . . . . 15
↾t Perf |
14 | 13 | simpld 475 |
. . . . . . . . . . . . . 14
↾t Perf |
15 | 14 | adantr 481 |
. . . . . . . . . . . . 13
↾t Perf
↾t |
16 | 2 | sseli 3599 |
. . . . . . . . . . . . . . . . . . . 20
|
17 | 16, 6 | sylib 208 |
. . . . . . . . . . . . . . . . . . 19
|
18 | 17 | simprd 479 |
. . . . . . . . . . . . . . . . . 18
|
19 | 17 | simpld 475 |
. . . . . . . . . . . . . . . . . . 19
|
20 | 9, 19, 11 | sylancr 695 |
. . . . . . . . . . . . . . . . . 18
|
21 | 18, 20 | mpbid 222 |
. . . . . . . . . . . . . . . . 17
|
22 | 21 | simprd 479 |
. . . . . . . . . . . . . . . 16
|
23 | 22 | adantr 481 |
. . . . . . . . . . . . . . 15
↾t Perf |
24 | 10 | elpwid 4170 |
. . . . . . . . . . . . . . 15
↾t Perf
|
25 | 23, 24 | sstrd 3613 |
. . . . . . . . . . . . . 14
↾t Perf |
26 | 25 | adantr 481 |
. . . . . . . . . . . . 13
↾t Perf
↾t
|
27 | | perfdvf.1 |
. . . . . . . . . . . . . . . . . 18
ℂfld |
28 | 27 | cnfldtopon 22586 |
. . . . . . . . . . . . . . . . 17
TopOn |
29 | | resttopon 20965 |
. . . . . . . . . . . . . . . . 17
TopOn
↾t TopOn |
30 | 28, 24, 29 | sylancr 695 |
. . . . . . . . . . . . . . . 16
↾t Perf
↾t TopOn |
31 | | topontop 20718 |
. . . . . . . . . . . . . . . 16
↾t TopOn ↾t |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . 15
↾t Perf
↾t |
33 | | toponuni 20719 |
. . . . . . . . . . . . . . . . 17
↾t TopOn ↾t |
34 | 30, 33 | syl 17 |
. . . . . . . . . . . . . . . 16
↾t Perf ↾t |
35 | 23, 34 | sseqtrd 3641 |
. . . . . . . . . . . . . . 15
↾t Perf ↾t |
36 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
↾t
↾t |
37 | 36 | ntrss2 20861 |
. . . . . . . . . . . . . . 15
↾t
↾t ↾t |
38 | 32, 35, 37 | syl2anc 693 |
. . . . . . . . . . . . . 14
↾t Perf ↾t |
39 | 38 | sselda 3603 |
. . . . . . . . . . . . 13
↾t Perf
↾t
|
40 | 15, 26, 39 | dvlem 23660 |
. . . . . . . . . . . 12
↾t Perf
↾t
|
41 | | eqid 2622 |
. . . . . . . . . . . 12
|
42 | 40, 41 | fmptd 6385 |
. . . . . . . . . . 11
↾t Perf
↾t
|
43 | 26 | ssdifssd 3748 |
. . . . . . . . . . 11
↾t Perf
↾t
|
44 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . 17
↾t Perf TopOn |
45 | 36 | ntrss3 20864 |
. . . . . . . . . . . . . . . . . . 19
↾t
↾t ↾t ↾t |
46 | 32, 35, 45 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
↾t Perf ↾t ↾t |
47 | 46, 34 | sseqtr4d 3642 |
. . . . . . . . . . . . . . . . 17
↾t Perf ↾t |
48 | | restabs 20969 |
. . . . . . . . . . . . . . . . 17
TopOn
↾t
↾t
↾t
↾t
↾t
↾t |
49 | 44, 47, 10, 48 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
↾t Perf ↾t ↾t ↾t
↾t
↾t |
50 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
↾t Perf
↾t Perf |
51 | 36 | ntropn 20853 |
. . . . . . . . . . . . . . . . . 18
↾t
↾t ↾t ↾t |
52 | 32, 35, 51 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
↾t Perf ↾t ↾t |
53 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
↾t
↾t
↾t ↾t ↾t ↾t |
54 | 36, 53 | perfopn 20989 |
. . . . . . . . . . . . . . . . 17
↾t Perf ↾t ↾t ↾t ↾t ↾t Perf |
55 | 50, 52, 54 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
↾t Perf ↾t ↾t ↾t Perf |
56 | 49, 55 | eqeltrrd 2702 |
. . . . . . . . . . . . . . 15
↾t Perf
↾t
↾t Perf |
57 | 27 | cnfldtop 22587 |
. . . . . . . . . . . . . . . 16
|
58 | 47, 24 | sstrd 3613 |
. . . . . . . . . . . . . . . 16
↾t Perf ↾t |
59 | 28 | toponunii 20721 |
. . . . . . . . . . . . . . . . 17
|
60 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
↾t ↾t
↾t
↾t |
61 | 59, 60 | restperf 20988 |
. . . . . . . . . . . . . . . 16
↾t ↾t ↾t Perf ↾t ↾t |
62 | 57, 58, 61 | sylancr 695 |
. . . . . . . . . . . . . . 15
↾t Perf ↾t ↾t Perf
↾t
↾t |
63 | 56, 62 | mpbid 222 |
. . . . . . . . . . . . . 14
↾t Perf ↾t ↾t |
64 | 57 | a1i 11 |
. . . . . . . . . . . . . . 15
↾t Perf |
65 | 59 | lpss3 20948 |
. . . . . . . . . . . . . . 15
↾t
↾t |
66 | 64, 25, 38, 65 | syl3anc 1326 |
. . . . . . . . . . . . . 14
↾t Perf ↾t |
67 | 63, 66 | sstrd 3613 |
. . . . . . . . . . . . 13
↾t Perf ↾t |
68 | 67 | sselda 3603 |
. . . . . . . . . . . 12
↾t Perf
↾t
|
69 | 59 | lpdifsn 20947 |
. . . . . . . . . . . . 13
|
70 | 57, 26, 69 | sylancr 695 |
. . . . . . . . . . . 12
↾t Perf
↾t
|
71 | 68, 70 | mpbid 222 |
. . . . . . . . . . 11
↾t Perf
↾t
|
72 | 42, 43, 71, 27 | limcmo 23646 |
. . . . . . . . . 10
↾t Perf
↾t
lim |
73 | 72 | ex 450 |
. . . . . . . . 9
↾t Perf ↾t
lim |
74 | | moanimv 2531 |
. . . . . . . . 9
↾t lim ↾t
lim |
75 | 73, 74 | sylibr 224 |
. . . . . . . 8
↾t Perf
↾t lim |
76 | | eqid 2622 |
. . . . . . . . . 10
↾t ↾t |
77 | 76, 27, 41, 24, 14, 23 | eldv 23662 |
. . . . . . . . 9
↾t Perf ↾t lim |
78 | 77 | mobidv 2491 |
. . . . . . . 8
↾t Perf
↾t lim |
79 | 75, 78 | mpbird 247 |
. . . . . . 7
↾t Perf |
80 | 79 | alrimiv 1855 |
. . . . . 6
↾t Perf |
81 | | reldv 23634 |
. . . . . . 7
|
82 | | dffun6 5903 |
. . . . . . 7
|
83 | 81, 82 | mpbiran 953 |
. . . . . 6
|
84 | 80, 83 | sylibr 224 |
. . . . 5
↾t Perf |
85 | | funfn 5918 |
. . . . 5
|
86 | 84, 85 | sylib 208 |
. . . 4
↾t Perf |
87 | | vex 3203 |
. . . . . . 7
|
88 | 87 | elrn 5366 |
. . . . . 6
|
89 | 24, 14, 23 | dvcl 23663 |
. . . . . . . 8
↾t Perf |
90 | 89 | ex 450 |
. . . . . . 7
↾t Perf |
91 | 90 | exlimdv 1861 |
. . . . . 6
↾t Perf |
92 | 88, 91 | syl5bi 232 |
. . . . 5
↾t Perf
|
93 | 92 | ssrdv 3609 |
. . . 4
↾t Perf |
94 | | df-f 5892 |
. . . 4
|
95 | 86, 93, 94 | sylanbrc 698 |
. . 3
↾t Perf |
96 | 95 | ex 450 |
. 2
↾t Perf |
97 | | f0 6086 |
. . . 4
|
98 | | df-ov 6653 |
. . . . . 6
|
99 | | ndmfv 6218 |
. . . . . 6
|
100 | 98, 99 | syl5eq 2668 |
. . . . 5
|
101 | 100 | dmeqd 5326 |
. . . . . 6
|
102 | | dm0 5339 |
. . . . . 6
|
103 | 101, 102 | syl6eq 2672 |
. . . . 5
|
104 | 100, 103 | feq12d 6033 |
. . . 4
|
105 | 97, 104 | mpbiri 248 |
. . 3
|
106 | 105 | a1d 25 |
. 2
↾t Perf |
107 | 96, 106 | pm2.61i 176 |
1
↾t Perf |