Step | Hyp | Ref
| Expression |
1 | | limccnp2.j |
. . . . 5
  
↾t     |
2 | | limccnp2cntop.k |
. . . . . . . 8
      |
3 | 2 | cntoptopon 14002 |
. . . . . . 7
TopOn   |
4 | | txtopon 13732 |
. . . . . . 7
  TopOn 
TopOn  
  TopOn      |
5 | 3, 3, 4 | mp2an 426 |
. . . . . 6
  TopOn     |
6 | | limccnp2.x |
. . . . . . 7

  |
7 | | limccnp2.y |
. . . . . . 7

  |
8 | | xpss12 4733 |
. . . . . . 7
 
   
   |
9 | 6, 7, 8 | syl2anc 411 |
. . . . . 6
  
    |
10 | | resttopon 13641 |
. . . . . 6
    TopOn 
    
     ↾t    TopOn      |
11 | 5, 9, 10 | sylancr 414 |
. . . . 5
   
↾t    TopOn      |
12 | 1, 11 | eqeltrid 2264 |
. . . 4
 TopOn 
    |
13 | 3 | a1i 9 |
. . . 4
 TopOn    |
14 | | limccnp2.h |
. . . 4
            |
15 | | cnpf2 13677 |
. . . 4
  TopOn 
  TopOn 
                  |
16 | 12, 13, 14, 15 | syl3anc 1238 |
. . 3
         |
17 | 2 | cntoptop 14003 |
. . . . . . . . . . 11
 |
18 | 17 | a1i 9 |
. . . . . . . . . . 11
   |
19 | | txtop 13730 |
. . . . . . . . . . 11
 
     |
20 | 17, 18, 19 | sylancr 414 |
. . . . . . . . . 10
     |
21 | | cnex 7934 |
. . . . . . . . . . . . 13
 |
22 | 21 | a1i 9 |
. . . . . . . . . . . 12
   |
23 | 22, 6 | ssexd 4143 |
. . . . . . . . . . 11
   |
24 | 22, 7 | ssexd 4143 |
. . . . . . . . . . 11
   |
25 | | xpexg 4740 |
. . . . . . . . . . 11
 
     |
26 | 23, 24, 25 | syl2anc 411 |
. . . . . . . . . 10
     |
27 | | resttop 13640 |
. . . . . . . . . 10
    
    
↾t      |
28 | 20, 26, 27 | syl2anc 411 |
. . . . . . . . 9
   
↾t      |
29 | 1, 28 | eqeltrid 2264 |
. . . . . . . 8
   |
30 | | toptopon2 13489 |
. . . . . . . 8

TopOn     |
31 | 29, 30 | sylib 122 |
. . . . . . 7
 TopOn     |
32 | | cnprcl2k 13676 |
. . . . . . 7
  TopOn                   |
33 | 31, 18, 14, 32 | syl3anc 1238 |
. . . . . 6
       |
34 | | toponuni 13485 |
. . . . . . 7
 TopOn         |
35 | 12, 34 | syl 14 |
. . . . . 6
      |
36 | 33, 35 | eleqtrrd 2257 |
. . . . 5
        |
37 | | opelxp 4656 |
. . . . 5
  
       |
38 | 36, 37 | sylib 122 |
. . . 4
 
   |
39 | 38 | simpld 112 |
. . 3
   |
40 | 38 | simprd 114 |
. . 3
   |
41 | 16, 39, 40 | fovcdmd 6018 |
. 2
       |
42 | | txrest 13746 |
. . . . . . . . . . . . 13
      
   ↾t      ↾t   ↾t     |
43 | 18, 18, 23, 24, 42 | syl22anc 1239 |
. . . . . . . . . . . 12
   
↾t      ↾t   ↾t     |
44 | 1, 43 | eqtrid 2222 |
. . . . . . . . . . 11
   ↾t   ↾t     |
45 | | cnxmet 14001 |
. . . . . . . . . . . . 13

      |
46 | | eqid 2177 |
. . . . . . . . . . . . . 14
           |
47 | | eqid 2177 |
. . . . . . . . . . . . . 14
    
        
     |
48 | 46, 2, 47 | metrest 13976 |
. . . . . . . . . . . . 13
  
      
↾t      
      |
49 | 45, 6, 48 | sylancr 414 |
. . . . . . . . . . . 12
 
↾t      
      |
50 | | eqid 2177 |
. . . . . . . . . . . . . 14
           |
51 | | eqid 2177 |
. . . . . . . . . . . . . 14
    
        
     |
52 | 50, 2, 51 | metrest 13976 |
. . . . . . . . . . . . 13
  
      
↾t      
      |
53 | 45, 7, 52 | sylancr 414 |
. . . . . . . . . . . 12
 
↾t      
      |
54 | 49, 53 | oveq12d 5892 |
. . . . . . . . . . 11
   ↾t   ↾t        
        
       |
55 | 44, 54 | eqtrd 2210 |
. . . . . . . . . 10
      
        
       |
56 | 55 | oveq1d 5889 |
. . . . . . . . 9
          
        
       |
57 | 56 | fveq1d 5517 |
. . . . . . . 8
                 
        
              |
58 | 14, 57 | eleqtrd 2256 |
. . . . . . 7
        
         
             |
59 | | xmetres2 13849 |
. . . . . . . . 9
  
       
          |
60 | 45, 6, 59 | sylancr 414 |
. . . . . . . 8
  
          |
61 | | xmetres2 13849 |
. . . . . . . . 9
  
       
          |
62 | 45, 7, 61 | sylancr 414 |
. . . . . . . 8
  
          |
63 | 45 | a1i 9 |
. . . . . . . 8
 
       |
64 | 47, 51, 2 | txmetcnp 13988 |
. . . . . . . 8
    
         
       
       
 
        
        
           
                
                     
           |
65 | 60, 62, 63, 38, 64 | syl31anc 1241 |
. . . . . . 7
         
        
           
                
                     
           |
66 | 58, 65 | mpbid 147 |
. . . . . 6
           
     
                     
          |
67 | 66 | simprd 114 |
. . . . 5
   

              
     
                |
68 | 67 | r19.21bi 2565 |
. . . 4
 

        
                     
         |
69 | | simpll 527 |
. . . . . 6
     

              
     
                  |
70 | | simprl 529 |
. . . . . 6
     

              
     
                  |
71 | | limccnp2.c |
. . . . . . . . 9
    lim    |
72 | | eqid 2177 |
. . . . . . . . . . . 12
     |
73 | | limccnp2.r |
. . . . . . . . . . . 12
 
   |
74 | 72, 73 | dmmptd 5346 |
. . . . . . . . . . 11
     |
75 | | limcrcl 14097 |
. . . . . . . . . . . . 13
    lim          


   |
76 | 71, 75 | syl 14 |
. . . . . . . . . . . 12
         


   |
77 | 76 | simp2d 1010 |
. . . . . . . . . . 11
     |
78 | 74, 77 | eqsstrrd 3192 |
. . . . . . . . . 10

  |
79 | 76 | simp3d 1011 |
. . . . . . . . . 10
   |
80 | 6 | adantr 276 |
. . . . . . . . . . 11
 
   |
81 | 80, 73 | sseldd 3156 |
. . . . . . . . . 10
 
   |
82 | 78, 79, 81 | limcmpted 14102 |
. . . . . . . . 9
     lim        #           
 
     |
83 | 71, 82 | mpbid 147 |
. . . . . . . 8
    
  #                  |
84 | 83 | simprd 114 |
. . . . . . 7
   
  #                 |
85 | 84 | r19.21bi 2565 |
. . . . . 6
 

    #       
         |
86 | 69, 70, 85 | syl2anc 411 |
. . . . 5
     

              
     
                

  #                 |
87 | 69 | adantr 276 |
. . . . . . 7
   
   
     
                     
          
  #           
 
     |
88 | | simplrl 535 |
. . . . . . 7
   
   
     
                     
          
  #           
 
     |
89 | | limccnp2.d |
. . . . . . . . . 10
    lim    |
90 | 7 | adantr 276 |
. . . . . . . . . . . 12
 
   |
91 | | limccnp2.s |
. . . . . . . . . . . 12
 
   |
92 | 90, 91 | sseldd 3156 |
. . . . . . . . . . 11
 
   |
93 | 78, 79, 92 | limcmpted 14102 |
. . . . . . . . . 10
     lim        #           
 
     |
94 | 89, 93 | mpbid 147 |
. . . . . . . . 9
    
  #                  |
95 | 94 | simprd 114 |
. . . . . . . 8
   
  #                 |
96 | 95 | r19.21bi 2565 |
. . . . . . 7
 

    #       
         |
97 | 87, 88, 96 | syl2anc 411 |
. . . . . 6
   
   
     
                     
          
  #           
 
       #       
         |
98 | | simp-5l 543 |
. . . . . . . 8
     
 


              
     
                    #           
 
    
  #           
 
      |
99 | 98, 73 | sylancom 420 |
. . . . . . 7
     
 


              
     
                    #           
 
    
  #           
 
      |
100 | 98, 91 | sylancom 420 |
. . . . . . 7
     
 


              
     
                    #           
 
    
  #           
 
      |
101 | 6 | ad4antr 494 |
. . . . . . 7
        
     
                     
          
  #           
 
    
  #           
 
     |
102 | 7 | ad4antr 494 |
. . . . . . 7
        
     
                     
          
  #           
 
    
  #           
 
     |
103 | 71 | ad4antr 494 |
. . . . . . 7
        
     
                     
          
  #           
 
    
  #           
 
      lim    |
104 | 89 | ad4antr 494 |
. . . . . . 7
        
     
                     
          
  #           
 
    
  #           
 
      lim    |
105 | 14 | ad4antr 494 |
. . . . . . 7
        
     
                     
          
  #           
 
    
  #           
 
              |
106 | | nfv 1528 |
. . . . . . . . 9
   
   
     
                     
          |
107 | | nfv 1528 |
. . . . . . . . . 10

 |
108 | | nfra1 2508 |
. . . . . . . . . 10
  
  #           
 
  |
109 | 107, 108 | nfan 1565 |
. . . . . . . . 9
      #           
 
   |
110 | 106, 109 | nfan 1565 |
. . . . . . . 8
        
     
                     
          
  #           
 
    |
111 | | nfv 1528 |
. . . . . . . . 9

 |
112 | | nfra1 2508 |
. . . . . . . . 9
  
  #           
 
  |
113 | 111, 112 | nfan 1565 |
. . . . . . . 8
      #           
 
   |
114 | 110, 113 | nfan 1565 |
. . . . . . 7
     
 


              
     
                    #           
 
    
  #           
 
    |
115 | | simp-4r 542 |
. . . . . . 7
        
     
                     
          
  #           
 
    
  #           
 
     |
116 | 70 | ad2antrr 488 |
. . . . . . 7
        
     
                     
          
  #           
 
    
  #           
 
     |
117 | | simprr 531 |
. . . . . . . 8
     

              
     
                

     
                     
         |
118 | 117 | ad2antrr 488 |
. . . . . . 7
        
     
                     
          
  #           
 
    
  #           
 
   

              
     
                |
119 | | simplrl 535 |
. . . . . . 7
        
     
                     
          
  #           
 
    
  #           
 
     |
120 | | simplrr 536 |
. . . . . . 7
        
     
                     
          
  #           
 
    
  #           
 
   
  #                 |
121 | | simprl 529 |
. . . . . . 7
        
     
                     
          
  #           
 
    
  #           
 
     |
122 | | simprr 531 |
. . . . . . 7
        
     
                     
          
  #           
 
    
  #           
 
   
  #                 |
123 | 99, 100, 101, 102, 2, 1, 103, 104, 105, 114, 115, 116, 118, 119, 120, 121, 122 | limccnp2lem 14115 |
. . . . . 6
        
     
                     
          
  #           
 
    
  #           
 
       #       
                 |
124 | 97, 123 | rexlimddv 2599 |
. . . . 5
   
   
     
                     
          
  #           
 
       #       
                 |
125 | 86, 124 | rexlimddv 2599 |
. . . 4
     

              
     
                

  #                         |
126 | 68, 125 | rexlimddv 2599 |
. . 3
 

    #       
                 |
127 | 126 | ralrimiva 2550 |
. 2
   
  #                         |
128 | 16 | adantr 276 |
. . . 4
 
         |
129 | 128, 73, 91 | fovcdmd 6018 |
. . 3
 
       |
130 | 78, 79, 129 | limcmpted 14102 |
. 2
             lim            #                           |
131 | 41, 127, 130 | mpbir2and 944 |
1
            lim    |