Step | Hyp | Ref
| Expression |
1 | | df-dv 22878 |
. . . . . . . . . . . . . . . . . . . 20
  

         ℂfld
↾t    
                          lim     |
2 | 1 | dmmpt2ssx 6890 |
. . . . . . . . . . . . . . . . . . 19
         |
3 | | simpl 463 |
. . . . . . . . . . . . . . . . . . 19
    
 ↾t  Perf   
 |
4 | 2, 3 | sseldi 3442 |
. . . . . . . . . . . . . . . . . 18
    
 ↾t  Perf              |
5 | | oveq2 6328 |
. . . . . . . . . . . . . . . . . . 19
       |
6 | 5 | opeliunxp2 4995 |
. . . . . . . . . . . . . . . . . 18
  
        
       |
7 | 4, 6 | sylib 201 |
. . . . . . . . . . . . . . . . 17
    
 ↾t  Perf   
    |
8 | 7 | simprd 469 |
. . . . . . . . . . . . . . . 16
    
 ↾t  Perf     |
9 | | cnex 9651 |
. . . . . . . . . . . . . . . . 17
 |
10 | 7 | simpld 465 |
. . . . . . . . . . . . . . . . 17
    
 ↾t  Perf    |
11 | | elpm2g 7519 |
. . . . . . . . . . . . . . . . 17
 
              |
12 | 9, 10, 11 | sylancr 674 |
. . . . . . . . . . . . . . . 16
    
 ↾t  Perf  
          |
13 | 8, 12 | mpbid 215 |
. . . . . . . . . . . . . . 15
    
 ↾t  Perf         |
14 | 13 | simpld 465 |
. . . . . . . . . . . . . 14
    
 ↾t  Perf       |
15 | 14 | adantr 471 |
. . . . . . . . . . . . 13
      
↾t  Perf
     ↾t             |
16 | 2 | sseli 3440 |
. . . . . . . . . . . . . . . . . . . 20
  

             |
17 | 16, 6 | sylib 201 |
. . . . . . . . . . . . . . . . . . 19
  

 
     |
18 | 17 | simprd 469 |
. . . . . . . . . . . . . . . . . 18
  

    |
19 | 17 | simpld 465 |
. . . . . . . . . . . . . . . . . . 19
  

   |
20 | 9, 19, 11 | sylancr 674 |
. . . . . . . . . . . . . . . . . 18
  

            |
21 | 18, 20 | mpbid 215 |
. . . . . . . . . . . . . . . . 17
  

    
   |
22 | 21 | simprd 469 |
. . . . . . . . . . . . . . . 16
  

  |
23 | 22 | adantr 471 |
. . . . . . . . . . . . . . 15
    
 ↾t  Perf   |
24 | 10 | elpwid 3973 |
. . . . . . . . . . . . . . 15
    
 ↾t  Perf
  |
25 | 23, 24 | sstrd 3454 |
. . . . . . . . . . . . . 14
    
 ↾t  Perf   |
26 | 25 | adantr 471 |
. . . . . . . . . . . . 13
      
↾t  Perf
     ↾t      
  |
27 | | perfdvf.1 |
. . . . . . . . . . . . . . . . . 18
  ℂfld |
28 | 27 | cnfldtopon 21858 |
. . . . . . . . . . . . . . . . 17
TopOn   |
29 | | resttopon 20232 |
. . . . . . . . . . . . . . . . 17
  TopOn 

 ↾t  TopOn    |
30 | 28, 24, 29 | sylancr 674 |
. . . . . . . . . . . . . . . 16
    
 ↾t  Perf 
↾t  TopOn    |
31 | | topontop 19996 |
. . . . . . . . . . . . . . . 16
  ↾t  TopOn   ↾t    |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . 15
    
 ↾t  Perf 
↾t    |
33 | | toponuni 19997 |
. . . . . . . . . . . . . . . . 17
  ↾t  TopOn    ↾t    |
34 | 30, 33 | syl 17 |
. . . . . . . . . . . . . . . 16
    
 ↾t  Perf   ↾t    |
35 | 23, 34 | sseqtrd 3480 |
. . . . . . . . . . . . . . 15
    
 ↾t  Perf   ↾t    |
36 | | eqid 2462 |
. . . . . . . . . . . . . . . 16
  ↾t   
↾t   |
37 | 36 | ntrss2 20127 |
. . . . . . . . . . . . . . 15
  
↾t 
  ↾t        ↾t        |
38 | 32, 35, 37 | syl2anc 671 |
. . . . . . . . . . . . . 14
    
 ↾t  Perf      ↾t        |
39 | 38 | sselda 3444 |
. . . . . . . . . . . . 13
      
↾t  Perf
     ↾t      
  |
40 | 15, 26, 39 | dvlem 22907 |
. . . . . . . . . . . 12
       
↾t  Perf
     ↾t      
                     |
41 | | eqid 2462 |
. . . . . . . . . . . 12
                                         |
42 | 40, 41 | fmptd 6074 |
. . . . . . . . . . 11
      
↾t  Perf
     ↾t                             
       |
43 | 26 | ssdifssd 3583 |
. . . . . . . . . . 11
      
↾t  Perf
     ↾t       
     |
44 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . 17
    
 ↾t  Perf TopOn    |
45 | 36 | ntrss3 20130 |
. . . . . . . . . . . . . . . . . . 19
  
↾t 
  ↾t        ↾t        ↾t    |
46 | 32, 35, 45 | syl2anc 671 |
. . . . . . . . . . . . . . . . . 18
    
 ↾t  Perf      ↾t        ↾t    |
47 | 46, 34 | sseqtr4d 3481 |
. . . . . . . . . . . . . . . . 17
    
 ↾t  Perf      ↾t        |
48 | | restabs 20236 |
. . . . . . . . . . . . . . . . 17
  TopOn 
     ↾t     
 
  ↾t 
↾t     
↾t       
↾t     
↾t         |
49 | 44, 47, 10, 48 | syl3anc 1276 |
. . . . . . . . . . . . . . . 16
    
 ↾t  Perf   ↾t  ↾t      ↾t       
↾t     
↾t         |
50 | | simpr 467 |
. . . . . . . . . . . . . . . . 17
    
 ↾t  Perf 
↾t  Perf |
51 | 36 | ntropn 20119 |
. . . . . . . . . . . . . . . . . 18
  
↾t 
  ↾t        ↾t       ↾t    |
52 | 32, 35, 51 | syl2anc 671 |
. . . . . . . . . . . . . . . . 17
    
 ↾t  Perf      ↾t       ↾t    |
53 | | eqid 2462 |
. . . . . . . . . . . . . . . . . 18
  ↾t 
↾t     
↾t         ↾t  ↾t      ↾t        |
54 | 36, 53 | perfopn 20256 |
. . . . . . . . . . . . . . . . 17
  
↾t  Perf      ↾t       ↾t     ↾t  ↾t      ↾t       Perf |
55 | 50, 52, 54 | syl2anc 671 |
. . . . . . . . . . . . . . . 16
    
 ↾t  Perf   ↾t  ↾t      ↾t       Perf |
56 | 49, 55 | eqeltrrd 2541 |
. . . . . . . . . . . . . . 15
    
 ↾t  Perf 
↾t     
↾t       Perf |
57 | 27 | cnfldtop 21859 |
. . . . . . . . . . . . . . . 16
 |
58 | 47, 24 | sstrd 3454 |
. . . . . . . . . . . . . . . 16
    
 ↾t  Perf      ↾t        |
59 | 28 | toponunii 20002 |
. . . . . . . . . . . . . . . . 17
  |
60 | | eqid 2462 |
. . . . . . . . . . . . . . . . 17
 ↾t      ↾t       
↾t     
↾t        |
61 | 59, 60 | restperf 20255 |
. . . . . . . . . . . . . . . 16
       ↾t         ↾t      ↾t       Perf      ↾t                  ↾t          |
62 | 57, 58, 61 | sylancr 674 |
. . . . . . . . . . . . . . 15
    
 ↾t  Perf   ↾t      ↾t       Perf
     ↾t     
            ↾t          |
63 | 56, 62 | mpbid 215 |
. . . . . . . . . . . . . 14
    
 ↾t  Perf      ↾t                  ↾t         |
64 | 57 | a1i 11 |
. . . . . . . . . . . . . . 15
    
 ↾t  Perf   |
65 | 59 | lpss3 20215 |
. . . . . . . . . . . . . . 15
 
     ↾t      
            ↾t                 |
66 | 64, 25, 38, 65 | syl3anc 1276 |
. . . . . . . . . . . . . 14
    
 ↾t  Perf             ↾t                 |
67 | 63, 66 | sstrd 3454 |
. . . . . . . . . . . . 13
    
 ↾t  Perf      ↾t                |
68 | 67 | sselda 3444 |
. . . . . . . . . . . 12
      
↾t  Perf
     ↾t      
          |
69 | 59 | lpdifsn 20214 |
. . . . . . . . . . . . 13
 
         
               |
70 | 57, 26, 69 | sylancr 674 |
. . . . . . . . . . . 12
      
↾t  Perf
     ↾t               
               |
71 | 68, 70 | mpbid 215 |
. . . . . . . . . . 11
      
↾t  Perf
     ↾t      
              |
72 | 42, 43, 71, 27 | limcmo 22893 |
. . . . . . . . . 10
      
↾t  Perf
     ↾t       
                     lim    |
73 | 72 | ex 440 |
. . . . . . . . 9
    
 ↾t  Perf       ↾t      
                     lim     |
74 | | moanimv 2371 |
. . . . . . . . 9
         ↾t                           lim         ↾t      
                     lim     |
75 | 73, 74 | sylibr 217 |
. . . . . . . 8
    
 ↾t  Perf        
↾t                           lim     |
76 | | eqid 2462 |
. . . . . . . . . 10
 ↾t   ↾t   |
77 | 76, 27, 41, 24, 14, 23 | eldv 22909 |
. . . . . . . . 9
    
 ↾t  Perf            ↾t                           lim      |
78 | 77 | mobidv 2331 |
. . . . . . . 8
    
 ↾t  Perf      
        ↾t                           lim      |
79 | 75, 78 | mpbird 240 |
. . . . . . 7
    
 ↾t  Perf        |
80 | 79 | alrimiv 1784 |
. . . . . 6
    
 ↾t  Perf          |
81 | | reldv 22881 |
. . . . . . 7
   |
82 | | dffun6 5620 |
. . . . . . 7
                |
83 | 81, 82 | mpbiran 934 |
. . . . . 6
            |
84 | 80, 83 | sylibr 217 |
. . . . 5
    
 ↾t  Perf     |
85 | | funfn 5634 |
. . . . 5
     
   |
86 | 84, 85 | sylib 201 |
. . . 4
    
 ↾t  Perf       |
87 | | vex 3060 |
. . . . . . 7
 |
88 | 87 | elrn 5097 |
. . . . . 6
  
       |
89 | 24, 14, 23 | dvcl 22910 |
. . . . . . . 8
      
↾t  Perf        |
90 | 89 | ex 440 |
. . . . . . 7
    
 ↾t  Perf         |
91 | 90 | exlimdv 1790 |
. . . . . 6
    
 ↾t  Perf          |
92 | 88, 91 | syl5bi 225 |
. . . . 5
    
 ↾t  Perf  

   |
93 | 92 | ssrdv 3450 |
. . . 4
    
 ↾t  Perf     |
94 | | df-f 5609 |
. . . 4
               
   |
95 | 86, 93, 94 | sylanbrc 675 |
. . 3
    
 ↾t  Perf           |
96 | 95 | ex 440 |
. 2
  

  ↾t  Perf            |
97 | | f0 5791 |
. . . 4
     |
98 | | df-ov 6323 |
. . . . . 6
        |
99 | | ndmfv 5916 |
. . . . . 6
   
       |
100 | 98, 99 | syl5eq 2508 |
. . . . 5
   
    |
101 | 100 | dmeqd 5059 |
. . . . . 6
   
    |
102 | | dm0 5070 |
. . . . . 6
 |
103 | 101, 102 | syl6eq 2512 |
. . . . 5
   
    |
104 | 100, 103 | feq12d 5743 |
. . . 4
   
                |
105 | 97, 104 | mpbiri 241 |
. . 3
   
          |
106 | 105 | a1d 26 |
. 2
   
  ↾t  Perf            |
107 | 96, 106 | pm2.61i 169 |
1
  ↾t  Perf           |