Step | Hyp | Ref
| Expression |
1 | | simprr 774 |
. . . . . . 7
 
                |
2 | | ssun2 3589 |
. . . . . . . . 9
       |
3 | | 1stckgen.1 |
. . . . . . . . . . 11
 TopOn    |
4 | | 1stckgen.3 |
. . . . . . . . . . 11
          |
5 | | lmcl 20390 |
. . . . . . . . . . 11
  TopOn         
  |
6 | 3, 4, 5 | syl2anc 673 |
. . . . . . . . . 10
   |
7 | | snssg 4096 |
. . . . . . . . . 10
 
             |
8 | 6, 7 | syl 17 |
. . . . . . . . 9
     
         |
9 | 2, 8 | mpbiri 241 |
. . . . . . . 8
       |
10 | 9 | adantr 472 |
. . . . . . 7
 
               |
11 | 1, 10 | sseldd 3419 |
. . . . . 6
 
            |
12 | | eluni2 4194 |
. . . . . 6
 

  |
13 | 11, 12 | sylib 201 |
. . . . 5
 
         
  |
14 | | nnuz 11218 |
. . . . . . 7
     |
15 | | simprr 774 |
. . . . . . 7
            
    |
16 | | 1zzd 10992 |
. . . . . . 7
            
    |
17 | 4 | ad2antrr 740 |
. . . . . . 7
            
           |
18 | | simplrl 778 |
. . . . . . . . 9
            
     |
19 | 18 | elpwid 3952 |
. . . . . . . 8
            
    |
20 | | simprl 772 |
. . . . . . . 8
            
    |
21 | 19, 20 | sseldd 3419 |
. . . . . . 7
            
    |
22 | 14, 15, 16, 17, 21 | lmcvg 20355 |
. . . . . 6
            
               |
23 | | imassrn 5185 |
. . . . . . . . . . . . 13
         |
24 | | ssun1 3588 |
. . . . . . . . . . . . 13
     |
25 | 23, 24 | sstri 3427 |
. . . . . . . . . . . 12
             |
26 | | id 22 |
. . . . . . . . . . . 12
             |
27 | 25, 26 | syl5ss 3429 |
. . . . . . . . . . 11
                 |
28 | | 1stckgen.2 |
. . . . . . . . . . . . . . . . . . 19
       |
29 | | frn 5747 |
. . . . . . . . . . . . . . . . . . 19
    
  |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . . . . 18
   |
31 | 23, 30 | syl5ss 3429 |
. . . . . . . . . . . . . . . . 17
           |
32 | | resttopon 20254 |
. . . . . . . . . . . . . . . . 17
  TopOn            ↾t          TopOn            |
33 | 3, 31, 32 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
 
↾t          TopOn            |
34 | | topontop 20018 |
. . . . . . . . . . . . . . . 16
  ↾t          TopOn         
 ↾t            |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . 15
 
↾t            |
36 | | fzfid 12224 |
. . . . . . . . . . . . . . . . . 18
       |
37 | | ffun 5742 |
. . . . . . . . . . . . . . . . . . . 20
       |
38 | 28, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
   |
39 | | elfznn 11854 |
. . . . . . . . . . . . . . . . . . . . 21
       |
40 | 39 | ssriv 3422 |
. . . . . . . . . . . . . . . . . . . 20
     |
41 | | fdm 5745 |
. . . . . . . . . . . . . . . . . . . . 21
       |
42 | 28, 41 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
   |
43 | 40, 42 | syl5sseqr 3467 |
. . . . . . . . . . . . . . . . . . 19
    
  |
44 | | fores 5815 |
. . . . . . . . . . . . . . . . . . 19
                               |
45 | 38, 43, 44 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
                         |
46 | | fofi 7878 |
. . . . . . . . . . . . . . . . . 18
      
                                |
47 | 36, 45, 46 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
           |
48 | | pwfi 7887 |
. . . . . . . . . . . . . . . . 17
        
           |
49 | 47, 48 | sylib 201 |
. . . . . . . . . . . . . . . 16
            |
50 | | restsspw 15408 |
. . . . . . . . . . . . . . . 16
 ↾t         
          |
51 | | ssfi 7810 |
. . . . . . . . . . . . . . . 16
           
↾t                   
 ↾t            |
52 | 49, 50, 51 | sylancl 675 |
. . . . . . . . . . . . . . 15
 
↾t            |
53 | 35, 52 | elind 3609 |
. . . . . . . . . . . . . 14
 
↾t              |
54 | | fincmp 20485 |
. . . . . . . . . . . . . 14
  ↾t             ↾t            |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . 13
 
↾t            |
56 | | topontop 20018 |
. . . . . . . . . . . . . . 15
 TopOn 
  |
57 | 3, 56 | syl 17 |
. . . . . . . . . . . . . 14
   |
58 | | toponuni 20019 |
. . . . . . . . . . . . . . . 16
 TopOn 
   |
59 | 3, 58 | syl 17 |
. . . . . . . . . . . . . . 15
    |
60 | 31, 59 | sseqtrd 3454 |
. . . . . . . . . . . . . 14
            |
61 | | eqid 2471 |
. . . . . . . . . . . . . . 15
   |
62 | 61 | cmpsub 20492 |
. . . . . . . . . . . . . 14
              ↾t         
           
                  |
63 | 57, 60, 62 | syl2anc 673 |
. . . . . . . . . . . . 13
   ↾t         
           
                  |
64 | 55, 63 | mpbid 215 |
. . . . . . . . . . . 12
            
                 |
65 | 64 | r19.21bi 2776 |
. . . . . . . . . . 11
 
                             |
66 | 27, 65 | syl5 32 |
. . . . . . . . . 10
 
   
   
                 |
67 | 66 | impr 631 |
. . . . . . . . 9
 
                         |
68 | 67 | adantr 472 |
. . . . . . . 8
                                             |
69 | | inss1 3643 |
. . . . . . . . . . . . . 14
     |
70 | | simprl 772 |
. . . . . . . . . . . . . 14
    
                                             |
71 | 69, 70 | sseldi 3416 |
. . . . . . . . . . . . 13
    
                                           |
72 | 71 | elpwid 3952 |
. . . . . . . . . . . 12
    
                                       
  |
73 | | simprll 780 |
. . . . . . . . . . . . . 14
                               |
74 | 73 | adantr 472 |
. . . . . . . . . . . . 13
    
                                       
  |
75 | 74 | snssd 4108 |
. . . . . . . . . . . 12
    
                                            |
76 | 72, 75 | unssd 3601 |
. . . . . . . . . . 11
    
                                              |
77 | | vex 3034 |
. . . . . . . . . . . 12
 |
78 | 77 | elpw2 4565 |
. . . . . . . . . . 11
            |
79 | 76, 78 | sylibr 217 |
. . . . . . . . . 10
    
                                               |
80 | | inss2 3644 |
. . . . . . . . . . . 12
    |
81 | 80, 70 | sseldi 3416 |
. . . . . . . . . . 11
    
                                          |
82 | | snfi 7668 |
. . . . . . . . . . 11
 
 |
83 | | unfi 7856 |
. . . . . . . . . . 11
           |
84 | 81, 82, 83 | sylancl 675 |
. . . . . . . . . 10
    
                                              |
85 | 79, 84 | elind 3609 |
. . . . . . . . 9
    
                                                 |
86 | | ffn 5739 |
. . . . . . . . . . . . . 14
    
  |
87 | 28, 86 | syl 17 |
. . . . . . . . . . . . 13
   |
88 | 87 | ad3antrrr 744 |
. . . . . . . . . . . 12
    
                                       
  |
89 | | simprrr 783 |
. . . . . . . . . . . . . . . . . 18
                                         |
90 | 89 | adantr 472 |
. . . . . . . . . . . . . . . . 17
    
                                        
           |
91 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . 19
           |
92 | 91 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . 18
     
       |
93 | 92 | rspccva 3135 |
. . . . . . . . . . . . . . . . 17
                
      |
94 | 90, 93 | sylan 479 |
. . . . . . . . . . . . . . . 16
                                             
           |
95 | | elun2 3593 |
. . . . . . . . . . . . . . . 16
              |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . . . . 15
                                             
          
   |
97 | 96 | adantlr 729 |
. . . . . . . . . . . . . 14
     
          

                                            |
98 | | elnnuz 11219 |
. . . . . . . . . . . . . . . . . 18

      |
99 | 98 | anbi1i 709 |
. . . . . . . . . . . . . . . . 17
 
    
    
       |
100 | | elfzuzb 11820 |
. . . . . . . . . . . . . . . . 17
    
    
       |
101 | 99, 100 | bitr4i 260 |
. . . . . . . . . . . . . . . 16
 
    
      |
102 | | simprr 774 |
. . . . . . . . . . . . . . . . . . 19
    
                                                   |
103 | | funimass4 5930 |
. . . . . . . . . . . . . . . . . . . . 21
                
              |
104 | 38, 43, 103 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . 20
                         |
105 | 104 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . . 19
    
                                                                |
106 | 102, 105 | mpbid 215 |
. . . . . . . . . . . . . . . . . 18
    
                                        
            |
107 | 106 | r19.21bi 2776 |
. . . . . . . . . . . . . . . . 17
                                             
            |
108 | | elun1 3592 |
. . . . . . . . . . . . . . . . 17
           
   |
109 | 107, 108 | syl 17 |
. . . . . . . . . . . . . . . 16
                                             
              |
110 | 101, 109 | sylan2b 483 |
. . . . . . . . . . . . . . 15
                                              
               |
111 | 110 | anassrs 660 |
. . . . . . . . . . . . . 14
     
          

                                            |
112 | | simprl 772 |
. . . . . . . . . . . . . . . 16
  

            
  |
113 | 112 | ad2antlr 741 |
. . . . . . . . . . . . . . 15
    
                                          |
114 | | nnz 10983 |
. . . . . . . . . . . . . . . 16
   |
115 | | nnz 10983 |
. . . . . . . . . . . . . . . 16
   |
116 | | uztric 11204 |
. . . . . . . . . . . . . . . 16
 
             |
117 | 114, 115,
116 | syl2an 485 |
. . . . . . . . . . . . . . 15
 
             |
118 | 113, 117 | sylan 479 |
. . . . . . . . . . . . . 14
                                             
             |
119 | 97, 111, 118 | mpjaodan 803 |
. . . . . . . . . . . . 13
                                             
      
   |
120 | 119 | ralrimiva 2809 |
. . . . . . . . . . . 12
    
                                        
         |
121 | | fnfvrnss 6066 |
. . . . . . . . . . . 12
          
 
   |
122 | 88, 120, 121 | syl2anc 673 |
. . . . . . . . . . 11
    
                                       
 
   |
123 | | elun2 3593 |
. . . . . . . . . . . . . 14
      |
124 | 123 | ad2antlr 741 |
. . . . . . . . . . . . 13
  

            
     |
125 | 124 | ad2antlr 741 |
. . . . . . . . . . . 12
    
                                       
 
   |
126 | 125 | snssd 4108 |
. . . . . . . . . . 11
    
                                           
   |
127 | 122, 126 | unssd 3601 |
. . . . . . . . . 10
    
                                        
        |
128 | | uniun 4209 |
. . . . . . . . . . 11
            |
129 | | vex 3034 |
. . . . . . . . . . . . 13
 |
130 | 129 | unisn 4205 |
. . . . . . . . . . . 12
    |
131 | 130 | uneq2i 3576 |
. . . . . . . . . . 11
 
        |
132 | 128, 131 | eqtri 2493 |
. . . . . . . . . 10
         |
133 | 127, 132 | syl6sseqr 3465 |
. . . . . . . . 9
    
                                        
          |
134 | | unieq 4198 |
. . . . . . . . . . 11
             |
135 | 134 | sseq2d 3446 |
. . . . . . . . . 10
                       |
136 | 135 | rspcev 3136 |
. . . . . . . . 9
                   
 
  
      |
137 | 85, 133, 136 | syl2anc 673 |
. . . . . . . 8
    
                                        
 
  
      |
138 | 68, 137 | rexlimddv 2875 |
. . . . . . 7
                                         |
139 | 138 | anassrs 660 |
. . . . . 6
    
                                    |
140 | 22, 139 | rexlimddv 2875 |
. . . . 5
            
              |
141 | 13, 140 | rexlimddv 2875 |
. . . 4
 
                     |
142 | 141 | expr 626 |
. . 3
 
   
   
             |
143 | 142 | ralrimiva 2809 |
. 2
                      |
144 | 6 | snssd 4108 |
. . . . 5
     |
145 | 30, 144 | unssd 3601 |
. . . 4
       |
146 | 145, 59 | sseqtrd 3454 |
. . 3
        |
147 | 61 | cmpsub 20492 |
. . 3
       
  ↾t                            |
148 | 57, 146, 147 | syl2anc 673 |
. 2
   ↾t                            |
149 | 143, 148 | mpbird 240 |
1
 
↾t        |