Step | Hyp | Ref
| Expression |
1 | | dvcnpcntop.k |
. . . . 5
      |
2 | | dvcnp.j |
. . . . 5

↾t   |
3 | | simpl3 1002 |
. . . . . 6
               |
4 | | simpl1 1000 |
. . . . . 6
               |
5 | 3, 4 | sstrd 3165 |
. . . . 5
               |
6 | | simpl2 1001 |
. . . . 5
                   |
7 | 1 | cntoptop 13666 |
. . . . . . . 8
 |
8 | | cnex 7913 |
. . . . . . . . 9
 |
9 | | ssexg 4139 |
. . . . . . . . 9
 
   |
10 | 4, 8, 9 | sylancl 413 |
. . . . . . . 8
               |
11 | | resttop 13303 |
. . . . . . . 8
 
 
↾t    |
12 | 7, 10, 11 | sylancr 414 |
. . . . . . 7
              ↾t    |
13 | 1 | cntoptopon 13665 |
. . . . . . . . . 10
TopOn   |
14 | | resttopon 13304 |
. . . . . . . . . 10
  TopOn 

 ↾t  TopOn    |
15 | 13, 4, 14 | sylancr 414 |
. . . . . . . . 9
              ↾t  TopOn    |
16 | | toponuni 13146 |
. . . . . . . . 9
  ↾t  TopOn    ↾t    |
17 | 15, 16 | syl 14 |
. . . . . . . 8
              
↾t    |
18 | 3, 17 | sseqtrd 3193 |
. . . . . . 7
               ↾t    |
19 | | eqid 2177 |
. . . . . . . 8
  ↾t   
↾t   |
20 | 19 | ntrss2 13254 |
. . . . . . 7
  
↾t 
  ↾t        ↾t        |
21 | 12, 18, 20 | syl2anc 411 |
. . . . . 6
                 
↾t        |
22 | | eqid 2177 |
. . . . . . . 8
 ↾t   ↾t   |
23 | | eqid 2177 |
. . . . . . . 8
  #                   #                  |
24 | | simp1 997 |
. . . . . . . 8
 
       |
25 | | simp2 998 |
. . . . . . . 8
 
           |
26 | | simp3 999 |
. . . . . . . 8
 
       |
27 | 22, 1, 23, 24, 25, 26 | eldvap 13784 |
. . . . . . 7
 
         
      ↾t         #
                lim      |
28 | 27 | simprbda 383 |
. . . . . 6
                  ↾t        |
29 | 21, 28 | sseldd 3156 |
. . . . 5
               |
30 | 6 | ffvelcdmda 5646 |
. . . . . . . 8
        
            |
31 | 6, 29 | ffvelcdmd 5647 |
. . . . . . . . 9
                   |
32 | 31 | adantr 276 |
. . . . . . . 8
        
            |
33 | 30, 32 | subcld 8245 |
. . . . . . 7
        
                  |
34 | | ssid 3175 |
. . . . . . . 8
 |
35 | 34 | a1i 9 |
. . . . . . 7
               |
36 | | txtopon 13395 |
. . . . . . . . 9
  TopOn 
TopOn  
  TopOn      |
37 | 13, 13, 36 | mp2an 426 |
. . . . . . . 8
  TopOn     |
38 | 37 | toponrestid 13152 |
. . . . . . 7
    
↾t     |
39 | 6, 5, 29 | dvlemap 13782 |
. . . . . . . . . 10
        
      #
 
                |
40 | | ssrab2 3240 |
. . . . . . . . . . . . 13

# 
 |
41 | 40, 5 | sstrid 3166 |
. . . . . . . . . . . 12
              #    |
42 | 41 | sselda 3155 |
. . . . . . . . . . 11
        
      #
 
  |
43 | 5, 29 | sseldd 3156 |
. . . . . . . . . . . 12
               |
44 | 43 | adantr 276 |
. . . . . . . . . . 11
        
      #
 
  |
45 | 42, 44 | subcld 8245 |
. . . . . . . . . 10
        
      #
 
    |
46 | 27 | simplbda 384 |
. . . . . . . . . 10
                #                 lim    |
47 | | limcresi 13768 |
. . . . . . . . . . . 12
     lim       

#   lim   |
48 | | resmpt 4950 |
. . . . . . . . . . . . . 14
  #       
#
    #       |
49 | 40, 48 | ax-mp 5 |
. . . . . . . . . . . . 13
    

#    
# 
    |
50 | 49 | oveq1i 5878 |
. . . . . . . . . . . 12
      
#   lim    
# 
   lim   |
51 | 47, 50 | sseqtri 3189 |
. . . . . . . . . . 11
     lim     #     lim   |
52 | 43 | subidd 8233 |
. . . . . . . . . . . 12
                 |
53 | 1 | subcncntop 13686 |
. . . . . . . . . . . . . . 15
     |
54 | 53 | a1i 9 |
. . . . . . . . . . . . . 14
                   |
55 | | cncfmptid 13716 |
. . . . . . . . . . . . . . 15
 
         |
56 | 5, 34, 55 | sylancl 413 |
. . . . . . . . . . . . . 14
                     |
57 | | cncfmptc 13715 |
. . . . . . . . . . . . . . 15
           |
58 | 43, 5, 35, 57 | syl3anc 1238 |
. . . . . . . . . . . . . 14
                     |
59 | 1, 54, 56, 58 | cncfmpt2fcntop 13718 |
. . . . . . . . . . . . 13
                       |
60 | | oveq1 5875 |
. . . . . . . . . . . . 13
       |
61 | 59, 29, 60 | cnmptlimc 13776 |
. . . . . . . . . . . 12
                    lim    |
62 | 52, 61 | eqeltrrd 2255 |
. . . . . . . . . . 11
                  lim    |
63 | 51, 62 | sselid 3153 |
. . . . . . . . . 10
                #     lim    |
64 | 1 | mulcncntop 13687 |
. . . . . . . . . . 11
     |
65 | 24, 25, 26 | dvcl 13785 |
. . . . . . . . . . . 12
               |
66 | | 0cn 7927 |
. . . . . . . . . . . 12
 |
67 | | opelxpi 4654 |
. . . . . . . . . . . 12
 
        |
68 | 65, 66, 67 | sylancl 413 |
. . . . . . . . . . 11
                    |
69 | 37 | toponunii 13148 |
. . . . . . . . . . . 12
      |
70 | 69 | cncnpi 13361 |
. . . . . . . . . . 11
                        |
71 | 64, 68, 70 | sylancr 414 |
. . . . . . . . . 10
                          |
72 | 39, 45, 35, 35, 1, 38, 46, 63, 71 | limccnp2cntop 13779 |
. . . . . . . . 9
                  #                     lim    |
73 | 65 | mul01d 8327 |
. . . . . . . . 9
                 |
74 | 6 | adantr 276 |
. . . . . . . . . . . . . 14
        
      #
 
      |
75 | | simpr 110 |
. . . . . . . . . . . . . . 15
        
      #
 
 #    |
76 | 40, 75 | sselid 3153 |
. . . . . . . . . . . . . 14
        
      #
 
  |
77 | 74, 76 | ffvelcdmd 5647 |
. . . . . . . . . . . . 13
        
      #
 
      |
78 | 31 | adantr 276 |
. . . . . . . . . . . . 13
        
      #
 
      |
79 | 77, 78 | subcld 8245 |
. . . . . . . . . . . 12
        
      #
 
            |
80 | | breq1 4003 |
. . . . . . . . . . . . . . . 16
  #
#    |
81 | 80 | elrab 2893 |
. . . . . . . . . . . . . . 15
  #   #
   |
82 | 81 | simprbi 275 |
. . . . . . . . . . . . . 14
  #  #   |
83 | 82 | adantl 277 |
. . . . . . . . . . . . 13
        
      #
 
#   |
84 | 42, 44, 83 | subap0d 8578 |
. . . . . . . . . . . 12
        
      #
 
  #   |
85 | 79, 45, 84 | divcanap1d 8724 |
. . . . . . . . . . 11
        
      #
 
                              |
86 | 85 | mpteq2dva 4090 |
. . . . . . . . . 10
               #
                     
# 
             |
87 | 86 | oveq1d 5883 |
. . . . . . . . 9
                #                     lim     #             lim    |
88 | 72, 73, 87 | 3eltr3d 2260 |
. . . . . . . 8
                #             lim    |
89 | 33 | fmpttd 5666 |
. . . . . . . . . 10
                               |
90 | 89, 5 | limcdifap 13764 |
. . . . . . . . 9
                          lim                 #
  lim
   |
91 | | resmpt 4950 |
. . . . . . . . . . 11
  #               
#    
# 
             |
92 | 40, 91 | ax-mp 5 |
. . . . . . . . . 10
            

#    
# 
            |
93 | 92 | oveq1i 5878 |
. . . . . . . . 9
              
#   lim    
# 
           lim   |
94 | 90, 93 | eqtrdi 2226 |
. . . . . . . 8
                          lim     #
            lim    |
95 | 88, 94 | eleqtrrd 2257 |
. . . . . . 7
                          lim    |
96 | | cncfmptc 13715 |
. . . . . . . . 9
                   |
97 | 31, 5, 35, 96 | syl3anc 1238 |
. . . . . . . 8
                         |
98 | | eqidd 2178 |
. . . . . . . 8
           |
99 | 97, 29, 98 | cnmptlimc 13776 |
. . . . . . 7
                        lim    |
100 | 1 | addcncntop 13685 |
. . . . . . . 8
     |
101 | | opelxpi 4654 |
. . . . . . . . 9
                  |
102 | 66, 31, 101 | sylancr 414 |
. . . . . . . 8
                        |
103 | 69 | cncnpi 13361 |
. . . . . . . 8
                       
        |
104 | 100, 102,
103 | sylancr 414 |
. . . . . . 7
                              |
105 | 33, 32, 35, 35, 1, 38, 95, 99, 104 | limccnp2cntop 13779 |
. . . . . 6
                                      lim    |
106 | 31 | addid2d 8084 |
. . . . . 6
                         |
107 | 30, 32 | npcand 8249 |
. . . . . . . . 9
        
                            |
108 | 107 | mpteq2dva 4090 |
. . . . . . . 8
                                       |
109 | 6 | feqmptd 5564 |
. . . . . . . 8
                     |
110 | 108, 109 | eqtr4d 2213 |
. . . . . . 7
                                 |
111 | 110 | oveq1d 5883 |
. . . . . 6
                                lim   lim    |
112 | 105, 106,
111 | 3eltr3d 2260 |
. . . . 5
                  lim    |
113 | 1, 2, 5, 6, 29, 112 | cnplimclemr 13771 |
. . . 4
                     |
114 | 113 | ex 115 |
. . 3
 
         
         |
115 | 114 | exlimdv 1819 |
. 2
 
      
             |
116 | | eldmg 4817 |
. . 3
    
         |
117 | 116 | ibi 176 |
. 2
   
      |
118 | 115, 117 | impel 280 |
1
       
           |