Step | Hyp | Ref
| Expression |
1 | | limccnp2.h |
. . . . . . . . . . 11
            |
2 | | eqid 2453 |
. . . . . . . . . . . 12
   |
3 | 2 | cnprcl 20273 |
. . . . . . . . . . 11
                |
4 | 1, 3 | syl 17 |
. . . . . . . . . 10
       |
5 | | limccnp2.j |
. . . . . . . . . . . 12
  
↾t     |
6 | | limccnp2.k |
. . . . . . . . . . . . . . 15
  ℂfld |
7 | 6 | cnfldtopon 21815 |
. . . . . . . . . . . . . 14
TopOn   |
8 | | txtopon 20618 |
. . . . . . . . . . . . . 14
  TopOn 
TopOn  
  TopOn      |
9 | 7, 7, 8 | mp2an 679 |
. . . . . . . . . . . . 13
  TopOn     |
10 | | limccnp2.x |
. . . . . . . . . . . . . 14

  |
11 | | limccnp2.y |
. . . . . . . . . . . . . 14

  |
12 | | xpss12 4943 |
. . . . . . . . . . . . . 14
 
   
   |
13 | 10, 11, 12 | syl2anc 667 |
. . . . . . . . . . . . 13
  
    |
14 | | resttopon 20189 |
. . . . . . . . . . . . 13
    TopOn 
    
     ↾t    TopOn      |
15 | 9, 13, 14 | sylancr 670 |
. . . . . . . . . . . 12
   
↾t    TopOn      |
16 | 5, 15 | syl5eqel 2535 |
. . . . . . . . . . 11
 TopOn 
    |
17 | | toponuni 19954 |
. . . . . . . . . . 11
 TopOn         |
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
      |
19 | 4, 18 | eleqtrrd 2534 |
. . . . . . . . 9
        |
20 | | opelxp 4867 |
. . . . . . . . 9
  
       |
21 | 19, 20 | sylib 200 |
. . . . . . . 8
 
   |
22 | 21 | simpld 461 |
. . . . . . 7
   |
23 | 22 | ad2antrr 733 |
. . . . . 6
       
   |
24 | | simpll 761 |
. . . . . . 7
       

  |
25 | | simpr 463 |
. . . . . . . . . . . 12
 

   
      |
26 | | elun 3576 |
. . . . . . . . . . . 12
    

     |
27 | 25, 26 | sylib 200 |
. . . . . . . . . . 11
 

    
     |
28 | 27 | ord 379 |
. . . . . . . . . 10
 

    
     |
29 | | elsni 3995 |
. . . . . . . . . 10
     |
30 | 28, 29 | syl6 34 |
. . . . . . . . 9
 

    
   |
31 | 30 | con1d 128 |
. . . . . . . 8
 

    
   |
32 | 31 | imp 431 |
. . . . . . 7
       

  |
33 | | limccnp2.r |
. . . . . . 7
 
   |
34 | 24, 32, 33 | syl2anc 667 |
. . . . . 6
       

  |
35 | 23, 34 | ifclda 3915 |
. . . . 5
 

           |
36 | 21 | simprd 465 |
. . . . . . 7
   |
37 | 36 | ad2antrr 733 |
. . . . . 6
       
   |
38 | | limccnp2.s |
. . . . . . 7
 
   |
39 | 24, 32, 38 | syl2anc 667 |
. . . . . 6
       

  |
40 | 37, 39 | ifclda 3915 |
. . . . 5
 

           |
41 | | opelxpi 4869 |
. . . . 5
            
    
            |
42 | 35, 40, 41 | syl2anc 667 |
. . . 4
 

            
        |
43 | | eqidd 2454 |
. . . 4
          
                  
           |
44 | 7 | a1i 11 |
. . . . . 6
 TopOn    |
45 | | cnpf2 20278 |
. . . . . 6
  TopOn 
  TopOn 
                  |
46 | 16, 44, 1, 45 | syl3anc 1269 |
. . . . 5
         |
47 | 46 | feqmptd 5923 |
. . . 4
           |
48 | | fveq2 5870 |
. . . . 5
         
               
           |
49 | | df-ov 6298 |
. . . . . 6
           
             
      |
50 | | ovif12 6380 |
. . . . . 6
           
                |
51 | 49, 50 | eqtr3i 2477 |
. . . . 5
           
    
 
            |
52 | 48, 51 | syl6eq 2503 |
. . . 4
         
                       |
53 | 42, 43, 47, 52 | fmptco 6061 |
. . 3
               
                           |
54 | | eqid 2453 |
. . . . . . . . . . 11
     |
55 | 54, 33 | dmmptd 5713 |
. . . . . . . . . 10
     |
56 | | limccnp2.c |
. . . . . . . . . . . 12
    lim    |
57 | | limcrcl 22841 |
. . . . . . . . . . . 12
    lim          


   |
58 | 56, 57 | syl 17 |
. . . . . . . . . . 11
         


   |
59 | 58 | simp2d 1022 |
. . . . . . . . . 10
     |
60 | 55, 59 | eqsstr3d 3469 |
. . . . . . . . 9

  |
61 | 58 | simp3d 1023 |
. . . . . . . . . 10
   |
62 | 61 | snssd 4120 |
. . . . . . . . 9
     |
63 | 60, 62 | unssd 3612 |
. . . . . . . 8
       |
64 | | resttopon 20189 |
. . . . . . . 8
  TopOn 

     ↾t      TopOn        |
65 | 7, 63, 64 | sylancr 670 |
. . . . . . 7
 
↾t      TopOn 
      |
66 | | ssun2 3600 |
. . . . . . . 8
       |
67 | | snssg 4108 |
. . . . . . . . 9
 
      
      |
68 | 61, 67 | syl 17 |
. . . . . . . 8
     
         |
69 | 66, 68 | mpbiri 237 |
. . . . . . 7
       |
70 | 10 | adantr 467 |
. . . . . . . . . 10
 
   |
71 | 70, 33 | sseldd 3435 |
. . . . . . . . 9
 
   |
72 | | eqid 2453 |
. . . . . . . . 9
 ↾t      
↾t       |
73 | 60, 61, 71, 72, 6 | limcmpt 22850 |
. . . . . . . 8
     lim          
    
↾t             |
74 | 56, 73 | mpbid 214 |
. . . . . . 7
         
    
↾t            |
75 | | limccnp2.d |
. . . . . . . 8
    lim    |
76 | 11 | adantr 467 |
. . . . . . . . . 10
 
   |
77 | 76, 38 | sseldd 3435 |
. . . . . . . . 9
 
   |
78 | 60, 61, 77, 72, 6 | limcmpt 22850 |
. . . . . . . 8
     lim          
    
↾t             |
79 | 75, 78 | mpbid 214 |
. . . . . . 7
         
    
↾t            |
80 | 65, 44, 44, 69, 74, 79 | txcnp 20647 |
. . . . . 6
          
            ↾t              |
81 | 9 | topontopi 19958 |
. . . . . . . 8
   |
82 | 81 | a1i 11 |
. . . . . . 7
     |
83 | | eqid 2453 |
. . . . . . . . 9
               
                  
    |
84 | 42, 83 | fmptd 6051 |
. . . . . . . 8
          
                     |
85 | | toponuni 19954 |
. . . . . . . . . 10
  ↾t      TopOn     
      ↾t        |
86 | 65, 85 | syl 17 |
. . . . . . . . 9
      
↾t        |
87 | 86 | feq2d 5720 |
. . . . . . . 8
           
                            
             ↾t             |
88 | 84, 87 | mpbid 214 |
. . . . . . 7
          
             ↾t            |
89 | | eqid 2453 |
. . . . . . . 8
  ↾t 
      ↾t       |
90 | 9 | toponunii 19959 |
. . . . . . . 8
      |
91 | 89, 90 | cnprest2 20318 |
. . . . . . 7
    

       
             ↾t          

             
            ↾t                     
            ↾t        
↾t           |
92 | 82, 88, 13, 91 | syl3anc 1269 |
. . . . . 6
           
            ↾t                     
            ↾t        
↾t           |
93 | 80, 92 | mpbid 214 |
. . . . 5
          
            ↾t        
↾t          |
94 | 5 | oveq2i 6306 |
. . . . . 6
  ↾t        
↾t         ↾t      |
95 | 94 | fveq1i 5871 |
. . . . 5
  
↾t             ↾t         ↾t         |
96 | 93, 95 | syl6eleqr 2542 |
. . . 4
          
            ↾t            |
97 | | iftrue 3889 |
. . . . . . . . 9
  
     |
98 | | iftrue 3889 |
. . . . . . . . 9
  
     |
99 | 97, 98 | opeq12d 4177 |
. . . . . . . 8
     
             |
100 | | opex 4667 |
. . . . . . . 8
    |
101 | 99, 83, 100 | fvmpt 5953 |
. . . . . . 7
               
                 |
102 | 69, 101 | syl 17 |
. . . . . 6
           
                 |
103 | 102 | fveq2d 5874 |
. . . . 5
                    
                    |
104 | 1, 103 | eleqtrrd 2534 |
. . . 4
                      
         |
105 | | cnpco 20295 |
. . . 4
           
            ↾t         
                   
          
         
            
↾t            |
106 | 96, 104, 105 | syl2anc 667 |
. . 3
               
         ↾t            |
107 | 53, 106 | eqeltrrd 2532 |
. 2
                      
↾t            |
108 | 46 | adantr 467 |
. . . 4
 
         |
109 | 108, 33, 38 | fovrnd 6446 |
. . 3
 
       |
110 | 60, 61, 109, 72, 6 | limcmpt 22850 |
. 2
             lim                       
↾t             |
111 | 107, 110 | mpbird 236 |
1
            lim    |