Step | Hyp | Ref
| Expression |
1 | | limccl 22830 |
. . . 4
 lim   |
2 | 1 | sseli 3428 |
. . 3
  lim    |
3 | 2 | pm4.71ri 639 |
. 2
  lim 
  lim     |
4 | | eqid 2451 |
. . . . . 6
 ↾t      
↾t       |
5 | | ellimc2.k |
. . . . . 6
  ℂfld |
6 | | eqid 2451 |
. . . . . 6
                               |
7 | | limccl.f |
. . . . . 6
       |
8 | | limccl.a |
. . . . . 6

  |
9 | | limccl.b |
. . . . . 6
   |
10 | 4, 5, 6, 7, 8, 9 | ellimc 22828 |
. . . . 5
   lim          
         ↾t             |
11 | 10 | adantr 467 |
. . . 4
 

  lim 
        
         ↾t             |
12 | 5 | cnfldtopon 21803 |
. . . . . . 7
TopOn   |
13 | 9 | snssd 4117 |
. . . . . . . 8
     |
14 | 8, 13 | unssd 3610 |
. . . . . . 7
       |
15 | | resttopon 20177 |
. . . . . . 7
  TopOn 

     ↾t      TopOn        |
16 | 12, 14, 15 | sylancr 669 |
. . . . . 6
 
↾t      TopOn 
      |
17 | 16 | adantr 467 |
. . . . 5
 

 ↾t      TopOn        |
18 | 12 | a1i 11 |
. . . . 5
 

TopOn    |
19 | | ssun2 3598 |
. . . . . . 7
       |
20 | | snssg 4105 |
. . . . . . . 8
 
      
      |
21 | 9, 20 | syl 17 |
. . . . . . 7
     
         |
22 | 19, 21 | mpbiri 237 |
. . . . . 6
       |
23 | 22 | adantr 467 |
. . . . 5
 

      |
24 | | elun 3574 |
. . . . . . . 8
    

     |
25 | | elsn 3982 |
. . . . . . . . 9
     |
26 | 25 | orbi2i 522 |
. . . . . . . 8
 
  

   |
27 | 24, 26 | bitri 253 |
. . . . . . 7
    

   |
28 | | simpllr 769 |
. . . . . . . 8
   
 
     |
29 | | pm5.61 719 |
. . . . . . . . . 10
  



   |
30 | 7 | ffvelrnda 6022 |
. . . . . . . . . . 11
 
       |
31 | 30 | ad2ant2r 753 |
. . . . . . . . . 10
    
        |
32 | 29, 31 | sylan2b 478 |
. . . . . . . . 9
     

        |
33 | 32 | anassrs 654 |
. . . . . . . 8
   
 
 
       |
34 | 28, 33 | ifclda 3913 |
. . . . . . 7
    
 
   
       |
35 | 27, 34 | sylan2b 478 |
. . . . . 6
                    |
36 | 35, 6 | fmptd 6046 |
. . . . 5
 

                         |
37 | | iscnp 20253 |
. . . . . 6
  
↾t      TopOn 
   
TopOn                
         ↾t                                             
        
 
↾t                          
      |
38 | 37 | baibd 920 |
. . . . 5
    ↾t      TopOn     
TopOn               
              
                   ↾t                               
 ↾t 
               
              |
39 | 17, 18, 23, 36, 38 | syl31anc 1271 |
. . . 4
 

                   ↾t                               
 ↾t 
               
              |
40 | | iftrue 3887 |
. . . . . . . . . . 11
            |
41 | 40, 6 | fvmptg 5946 |
. . . . . . . . . 10
     

                     |
42 | 22, 41 | sylan 474 |
. . . . . . . . 9
 

                     |
43 | 42 | eleq1d 2513 |
. . . . . . . 8
 

          
        
   |
44 | 43 | imbi1d 319 |
. . . . . . 7
 

           
        
 
↾t                          
  
 
↾t                          
     |
45 | 44 | adantr 467 |
. . . . . 6
                          
 ↾t 
               
          

 
↾t                          
     |
46 | 5 | cnfldtop 21804 |
. . . . . . . . . . 11
 |
47 | | cnex 9620 |
. . . . . . . . . . . . . 14
 |
48 | 47 | ssex 4547 |
. . . . . . . . . . . . 13
           |
49 | 14, 48 | syl 17 |
. . . . . . . . . . . 12
       |
50 | 49 | ad2antrr 732 |
. . . . . . . . . . 11
    
 
      |
51 | | restval 15325 |
. . . . . . . . . . 11
  
     ↾t      
 
       |
52 | 46, 50, 51 | sylancr 669 |
. . . . . . . . . 10
    
 
 ↾t 
              |
53 | 52 | rexeqdv 2994 |
. . . . . . . . 9
    
 
 
 ↾t 
               
         
                             
    |
54 | | vex 3048 |
. . . . . . . . . . . 12
 |
55 | 54 | inex1 4544 |
. . . . . . . . . . 11
       |
56 | 55 | rgenw 2749 |
. . . . . . . . . 10

       |
57 | | eqid 2451 |
. . . . . . . . . . 11
                 |
58 | | eleq2 2518 |
. . . . . . . . . . . 12
                 |
59 | | imaeq2 5164 |
. . . . . . . . . . . . 13
                
                  
                 |
60 | 59 | sseq1d 3459 |
. . . . . . . . . . . 12
                          
                            |
61 | 58, 60 | anbi12d 717 |
. . . . . . . . . . 11
                            
  
             
                   |
62 | 57, 61 | rexrnmpt 6032 |
. . . . . . . . . 10
 

       
 
                         
                           
          |
63 | 56, 62 | mp1i 13 |
. . . . . . . . 9
    
 
 
                             

  
             
                   |
64 | 22 | ad3antrrr 736 |
. . . . . . . . . . . 12
   
 
         |
65 | | elin 3617 |
. . . . . . . . . . . . 13
      

       |
66 | 65 | rbaib 917 |
. . . . . . . . . . . 12
           
   |
67 | 64, 66 | syl 17 |
. . . . . . . . . . 11
   
 
   
     
   |
68 | | simpllr 769 |
. . . . . . . . . . . . . . . . 17
   
 
     |
69 | | fvex 5875 |
. . . . . . . . . . . . . . . . 17
     |
70 | | ifexg 3950 |
. . . . . . . . . . . . . . . . 17
                  |
71 | 68, 69, 70 | sylancl 668 |
. . . . . . . . . . . . . . . 16
   
 
              |
72 | 71 | ralrimivw 2803 |
. . . . . . . . . . . . . . 15
   
 
     
                |
73 | | eqid 2451 |
. . . . . . . . . . . . . . . 16
                                   |
74 | 73 | fnmpt 5704 |
. . . . . . . . . . . . . . 15
 
                                  
      |
75 | 73 | fmpt 6043 |
. . . . . . . . . . . . . . . . 17
 
               
  
                          |
76 | | df-f 5586 |
. . . . . . . . . . . . . . . . 17
                     
         
              
                         |
77 | 75, 76 | bitri 253 |
. . . . . . . . . . . . . . . 16
 
               
                   
              
         |
78 | 77 | baib 914 |
. . . . . . . . . . . . . . 15
                   
       
             
                    |
79 | 72, 74, 78 | 3syl 18 |
. . . . . . . . . . . . . 14
   
 
    

                 
                 |
80 | | simplrr 771 |
. . . . . . . . . . . . . . . . 17
   
 
     |
81 | | inss2 3653 |
. . . . . . . . . . . . . . . . . . 19
   
   |
82 | 81 | sseli 3428 |
. . . . . . . . . . . . . . . . . 18
         |
83 | 25, 40 | sylbi 199 |
. . . . . . . . . . . . . . . . . . 19
              |
84 | 83 | eleq1d 2513 |
. . . . . . . . . . . . . . . . . 18
            
   |
85 | 82, 84 | syl 17 |
. . . . . . . . . . . . . . . . 17
         
    
   |
86 | 80, 85 | syl5ibrcom 226 |
. . . . . . . . . . . . . . . 16
   
 
       
   
        |
87 | 86 | ralrimiv 2800 |
. . . . . . . . . . . . . . 15
   
 
            
       |
88 | | undif1 3842 |
. . . . . . . . . . . . . . . . . . . 20
             |
89 | 88 | ineq2i 3631 |
. . . . . . . . . . . . . . . . . . 19
           
     |
90 | | indi 3689 |
. . . . . . . . . . . . . . . . . . 19
                       |
91 | 89, 90 | eqtr3i 2475 |
. . . . . . . . . . . . . . . . . 18
                   |
92 | 91 | raleqi 2991 |
. . . . . . . . . . . . . . . . 17
 
               
                         |
93 | | ralunb 3615 |
. . . . . . . . . . . . . . . . 17
 
 
              
                 
              
        |
94 | 92, 93 | bitri 253 |
. . . . . . . . . . . . . . . 16
 
               
 
                                  |
95 | 94 | rbaib 917 |
. . . . . . . . . . . . . . 15
 
                 
             
           
        |
96 | 87, 95 | syl 17 |
. . . . . . . . . . . . . 14
   
 
    

                          
        |
97 | 79, 96 | bitr3d 259 |
. . . . . . . . . . . . 13
   
 
              
     
           
        |
98 | | inss2 3653 |
. . . . . . . . . . . . . . . 16
           |
99 | 98 | sseli 3428 |
. . . . . . . . . . . . . . 15
             |
100 | | eldifsni 4098 |
. . . . . . . . . . . . . . . . 17
       |
101 | | ifnefalse 3893 |
. . . . . . . . . . . . . . . . 17
                |
102 | 100, 101 | syl 17 |
. . . . . . . . . . . . . . . 16
                    |
103 | 102 | eleq1d 2513 |
. . . . . . . . . . . . . . 15
                      |
104 | 99, 103 | syl 17 |
. . . . . . . . . . . . . 14
                        |
105 | 104 | ralbiia 2818 |
. . . . . . . . . . . . 13
 
               
              |
106 | 97, 105 | syl6bb 265 |
. . . . . . . . . . . 12
   
 
              
     
               |
107 | | df-ima 4847 |
. . . . . . . . . . . . . 14
                                          
      |
108 | | inss2 3653 |
. . . . . . . . . . . . . . . 16
           |
109 | | resmpt 5154 |
. . . . . . . . . . . . . . . 16
       
            
       
       
                |
110 | 108, 109 | mp1i 13 |
. . . . . . . . . . . . . . 15
   
 
            
       
       
                |
111 | 110 | rneqd 5062 |
. . . . . . . . . . . . . 14
   
 
            
       
                        |
112 | 107, 111 | syl5eq 2497 |
. . . . . . . . . . . . 13
   
 
            
                                  |
113 | 112 | sseq1d 3459 |
. . . . . . . . . . . 12
   
 
             
              
                    |
114 | 7 | ad3antrrr 736 |
. . . . . . . . . . . . . 14
   
 
         |
115 | | ffun 5731 |
. . . . . . . . . . . . . 14
       |
116 | 114, 115 | syl 17 |
. . . . . . . . . . . . 13
   
 
     |
117 | | difss 3560 |
. . . . . . . . . . . . . . 15
   
 |
118 | 98, 117 | sstri 3441 |
. . . . . . . . . . . . . 14
       |
119 | | fdm 5733 |
. . . . . . . . . . . . . . 15
       |
120 | 114, 119 | syl 17 |
. . . . . . . . . . . . . 14
   
 
     |
121 | 118, 120 | syl5sseqr 3481 |
. . . . . . . . . . . . 13
   
 
   
    
  |
122 | | funimass4 5916 |
. . . . . . . . . . . . 13
  
    
           
               |
123 | 116, 121,
122 | syl2anc 667 |
. . . . . . . . . . . 12
   
 
       
                     |
124 | 106, 113,
123 | 3bitr4d 289 |
. . . . . . . . . . 11
   
 
             
              
             |
125 | 67, 124 | anbi12d 717 |
. . . . . . . . . 10
   
 
                    
               

              |
126 | 125 | rexbidva 2898 |
. . . . . . . . 9
    
 
 

               
               


              |
127 | 53, 63, 126 | 3bitrd 283 |
. . . . . . . 8
    
 
 
 ↾t 
               
         


              |
128 | 127 | anassrs 654 |
. . . . . . 7
   


  
 ↾t 
               
         


              |
129 | 128 | pm5.74da 693 |
. . . . . 6
         ↾t                 
          



               |
130 | 45, 129 | bitrd 257 |
. . . . 5
                          
 ↾t 
               
          



               |
131 | 130 | ralbidva 2824 |
. . . 4
 

 
          
        
 
↾t                          
   
 
   
           |
132 | 11, 39, 131 | 3bitrd 283 |
. . 3
 

  lim 




               |
133 | 132 | pm5.32da 647 |
. 2
    lim  
 



                |
134 | 3, 133 | syl5bb 261 |
1
   lim    
 
   
            |