Step | Hyp | Ref
| Expression |
1 | | eqid 2454 |
. . . 4
  ↾t   
↾t   |
2 | 1 | iscmp 19124 |
. . 3
  ↾t   
↾t   
↾t     
↾t          ↾t       |
3 | | id 22 |
. . . . . 6
   |
4 | | cmpsub.1 |
. . . . . . 7
  |
5 | 4 | topopn 18652 |
. . . . . 6
   |
6 | | ssexg 4547 |
. . . . . 6
 
   |
7 | 3, 5, 6 | syl2anr 478 |
. . . . 5
  
  |
8 | | resttop 18897 |
. . . . 5
 
 
↾t    |
9 | 7, 8 | syldan 470 |
. . . 4
   
↾t    |
10 | | ibar 504 |
. . . . 5
  ↾t     ↾t      ↾t          ↾t      ↾t  
 ↾t     
↾t          ↾t        |
11 | 10 | bicomd 201 |
. . . 4
  ↾t     ↾t    ↾t     
↾t          ↾t      
↾t     
↾t          ↾t       |
12 | 9, 11 | syl 16 |
. . 3
      ↾t    ↾t     
↾t          ↾t      
↾t     
↾t          ↾t       |
13 | 2, 12 | syl5bb 257 |
. 2
     ↾t 
 
↾t     
↾t          ↾t       |
14 | | vex 3081 |
. . . . . . . . . . 11
 |
15 | | eqeq1 2458 |
. . . . . . . . . . . 12
   
     |
16 | 15 | rexbidv 2868 |
. . . . . . . . . . 11
  
 

     |
17 | 14, 16 | elab 3213 |
. . . . . . . . . 10
      
    |
18 | | selpw 3976 |
. . . . . . . . . . . . . 14
 
  |
19 | | ssel2 3460 |
. . . . . . . . . . . . . . . 16
 
   |
20 | | ineq1 3654 |
. . . . . . . . . . . . . . . . . . 19
 
     |
21 | 20 | eqeq2d 2468 |
. . . . . . . . . . . . . . . . . 18
   
     |
22 | 21 | rspcev 3179 |
. . . . . . . . . . . . . . . . 17
 
   
    |
23 | 22 | ex 434 |
. . . . . . . . . . . . . . . 16
    
     |
24 | 19, 23 | syl 16 |
. . . . . . . . . . . . . . 15
 
    
     |
25 | 24 | ex 434 |
. . . . . . . . . . . . . 14
     
      |
26 | 18, 25 | sylbi 195 |
. . . . . . . . . . . . 13
     

      |
27 | 26 | adantl 466 |
. . . . . . . . . . . 12
  

      
      |
28 | 27 | rexlimdv 2946 |
. . . . . . . . . . 11
  

   
  
     |
29 | | simpll 753 |
. . . . . . . . . . . 12
  

    |
30 | 4 | sseq2i 3490 |
. . . . . . . . . . . . . 14

   |
31 | | uniexg 6488 |
. . . . . . . . . . . . . . . 16
    |
32 | | ssexg 4547 |
. . . . . . . . . . . . . . . 16
 
     |
33 | 31, 32 | sylan2 474 |
. . . . . . . . . . . . . . 15
 

   |
34 | 33 | ancoms 453 |
. . . . . . . . . . . . . 14
      |
35 | 30, 34 | sylan2b 475 |
. . . . . . . . . . . . 13
  
  |
36 | 35 | adantr 465 |
. . . . . . . . . . . 12
  

    |
37 | | elrest 14486 |
. . . . . . . . . . . 12
 
   ↾t 

     |
38 | 29, 36, 37 | syl2anc 661 |
. . . . . . . . . . 11
  

    ↾t  
     |
39 | 28, 38 | sylibrd 234 |
. . . . . . . . . 10
  

   
   ↾t     |
40 | 17, 39 | syl5bi 217 |
. . . . . . . . 9
  

         ↾t     |
41 | 40 | ssrdv 3471 |
. . . . . . . 8
  

        ↾t    |
42 | | vex 3081 |
. . . . . . . . . 10
 |
43 | 42 | abrexex 6662 |
. . . . . . . . 9
      |
44 | 43 | elpw 3975 |
. . . . . . . 8
  
    
↾t 
      ↾t    |
45 | 41, 44 | sylibr 212 |
. . . . . . 7
  

         ↾t    |
46 | | unieq 4208 |
. . . . . . . . . 10
        

     |
47 | 46 | eqeq2d 2468 |
. . . . . . . . 9
         ↾t     ↾t           |
48 | | pweq 3972 |
. . . . . . . . . . 11
               |
49 | 48 | ineq1d 3660 |
. . . . . . . . . 10
                   |
50 | 49 | rexeqdv 3030 |
. . . . . . . . 9
              ↾t              
↾t      |
51 | 47, 50 | imbi12d 320 |
. . . . . . . 8
         
↾t          ↾t       ↾t    
              
↾t       |
52 | 51 | rspcva 3177 |
. . . . . . 7
   
    
↾t  
 ↾t     
↾t          ↾t    
  
↾t   

       
       ↾t      |
53 | 45, 52 | sylan 471 |
. . . . . 6
   

  
 ↾t     
↾t          ↾t    
  
↾t   

       
       ↾t      |
54 | 53 | ex 434 |
. . . . 5
  

   

↾t     
↾t          ↾t       ↾t   

       
       ↾t       |
55 | 4 | restuni 18899 |
. . . . . . . . . . 11
  
  ↾t    |
56 | 55 | ad2antrr 725 |
. . . . . . . . . 10
   

   
  ↾t    |
57 | | vex 3081 |
. . . . . . . . . . . . . 14
 |
58 | 57 | inex1 4542 |
. . . . . . . . . . . . 13
   |
59 | 58 | dfiun2 4313 |
. . . . . . . . . . . 12

   

    |
60 | | incom 3652 |
. . . . . . . . . . . . . 14
     |
61 | 60 | a1i 11 |
. . . . . . . . . . . . 13
          
      |
62 | 61 | iuneq2dv 4301 |
. . . . . . . . . . . 12
   

    
  
    |
63 | 59, 62 | syl5eqr 2509 |
. . . . . . . . . . 11
   

      
        |
64 | | iunin2 4343 |
. . . . . . . . . . . 12

   
  |
65 | | uniiun 4332 |
. . . . . . . . . . . . . . . 16
   |
66 | 65 | eqcomi 2467 |
. . . . . . . . . . . . . . 15

  |
67 | 66 | a1i 11 |
. . . . . . . . . . . . . 14
   

    
   |
68 | 67 | ineq2d 3661 |
. . . . . . . . . . . . 13
   

     
      |
69 | | incom 3652 |
. . . . . . . . . . . . . . 15
       |
70 | | sseqin2 3678 |
. . . . . . . . . . . . . . . 16
 
     |
71 | 70 | biimpi 194 |
. . . . . . . . . . . . . . 15
   
   |
72 | 69, 71 | syl5eq 2507 |
. . . . . . . . . . . . . 14
       |
73 | 72 | adantl 466 |
. . . . . . . . . . . . 13
   

         |
74 | 68, 73 | eqtrd 2495 |
. . . . . . . . . . . 12
   

     
   |
75 | 64, 74 | syl5eq 2507 |
. . . . . . . . . . 11
   

    
    |
76 | 63, 75 | eqtr2d 2496 |
. . . . . . . . . 10
   

   
        |
77 | 56, 76 | eqeq12d 2476 |
. . . . . . . . 9
   

      
↾t   

      |
78 | 56 | eqeq1d 2456 |
. . . . . . . . . 10
   

        ↾t      |
79 | 78 | rexbidv 2868 |
. . . . . . . . 9
   

               
           
↾t      |
80 | 77, 79 | imbi12d 320 |
. . . . . . . 8
   

     
               ↾t    
              
↾t       |
81 | | eqid 2454 |
. . . . . . . . . 10
 |
82 | 81 | a1bi 337 |
. . . . . . . . 9
     
                     |
83 | | elin 3648 |
. . . . . . . . . . . 12
    
      

  
   |
84 | | selpw 3976 |
. . . . . . . . . . . . . 14
      
       |
85 | | dfss3 3455 |
. . . . . . . . . . . . . 14
      
       |
86 | | vex 3081 |
. . . . . . . . . . . . . . . 16
 |
87 | | eqeq1 2458 |
. . . . . . . . . . . . . . . . 17
   
     |
88 | 87 | rexbidv 2868 |
. . . . . . . . . . . . . . . 16
  
 

     |
89 | 86, 88 | elab 3213 |
. . . . . . . . . . . . . . 15
      
    |
90 | 89 | ralbii 2839 |
. . . . . . . . . . . . . 14
 
 
  


    |
91 | 84, 85, 90 | 3bitri 271 |
. . . . . . . . . . . . 13
       

    |
92 | 91 | anbi1i 695 |
. . . . . . . . . . . 12
    
   
 

     |
93 | 83, 92 | bitri 249 |
. . . . . . . . . . 11
    
            |
94 | | ineq1 3654 |
. . . . . . . . . . . . . . . 16
     
         |
95 | 94 | eqeq2d 2468 |
. . . . . . . . . . . . . . 15
       
         |
96 | 95 | ac6sfi 7668 |
. . . . . . . . . . . . . 14
   
          
         |
97 | 96 | ancoms 453 |
. . . . . . . . . . . . 13
     
                  |
98 | 97 | adantl 466 |
. . . . . . . . . . . 12
           

 
         
         |
99 | | frn 5674 |
. . . . . . . . . . . . . . . . . . . . 21
    
  |
100 | 99 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . 20
      

        
 
            
     |
101 | | vex 3081 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
102 | 101 | rnex 6623 |
. . . . . . . . . . . . . . . . . . . . 21
 |
103 | 102 | elpw 3975 |
. . . . . . . . . . . . . . . . . . . 20
 
  |
104 | 100, 103 | sylibr 212 |
. . . . . . . . . . . . . . . . . . 19
      

        
 
            
  
   |
105 | | simprr 756 |
. . . . . . . . . . . . . . . . . . . . 21
           

 
    |
106 | 105 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
      

        
 
            
     |
107 | | ffn 5668 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
108 | | dffn4 5735 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

      |
109 | 107, 108 | sylib 196 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
110 | | fodomfi 7702 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
  |
111 | 109, 110 | sylan2 474 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
  |
112 | 111 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
113 | 112 | adantll 713 |
. . . . . . . . . . . . . . . . . . . . 21
      
 
 
 

        
  |
114 | 113 | ad2ant2r 746 |
. . . . . . . . . . . . . . . . . . . 20
      

        
 
            
     |
115 | | domfi 7646 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
116 | 106, 114,
115 | syl2anc 661 |
. . . . . . . . . . . . . . . . . . 19
      

        
 
            
  
  |
117 | 104, 116 | elind 3649 |
. . . . . . . . . . . . . . . . . 18
      

        
 
            
  
     |
118 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
119 | | fveq2 5800 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           |
120 | 119 | ineq1d 3660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
         |
121 | 118, 120 | eqeq12d 2476 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
         |
122 | 121 | rspccv 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
      
         |
123 | | pm2.27 39 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
       
 
         |
124 | | inss1 3679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
           |
125 | | sseq1 3486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
       
   
             |
126 | 124, 125 | mpbiri 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
             |
127 | | ssel 3459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
     
       |
128 | 127 | a1dd 46 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
          
        |
129 | 126, 128 | syl 16 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
            
        |
130 | 129 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
             
         |
131 | 130 | 3imp 1182 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
                   |
132 | | fnfvelrn 5950 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
       |
133 | 132 | expcom 435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
         |
134 | 133 | 3ad2ant1 1009 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
               |
135 | 107, 134 | syl5 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
                   |
136 | 131, 135 | jcad 533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
                
        |
137 | 136 | 3exp 1187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
             
    
          |
138 | 123, 137 | syld 44 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       
 

                    |
139 | 138 | com3r 79 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
                
          |
140 | 139 | imp 429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
  
                
         |
141 | 140 | com3l 81 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
           
 
               |
142 | 141 | impcom 430 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      
                        |
143 | 122, 142 | sylan2 474 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           
 
 
              |
144 | | fvex 5810 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
145 | | eleq2 2527 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
       |
146 | | eleq1 2526 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             |
147 | 145, 146 | anbi12d 710 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
    
        |
148 | 144, 147 | spcev 3170 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          
      |
149 | 143, 148 | syl6 33 |
. . . . . . . . . . . . . . . . . . . . . . 23
           
 
 
        |
150 | 149 | exlimdv 1691 |
. . . . . . . . . . . . . . . . . . . . . 22
           
 
            |
151 | | eluni 4203 |
. . . . . . . . . . . . . . . . . . . . . 22
 
  
   |
152 | | eluni 4203 |
. . . . . . . . . . . . . . . . . . . . . 22
        |
153 | 150, 151,
152 | 3imtr4g 270 |
. . . . . . . . . . . . . . . . . . . . 21
           
 
      |
154 | 153 | ssrdv 3471 |
. . . . . . . . . . . . . . . . . . . 20
           
 
 
  |
155 | 154 | adantl 466 |
. . . . . . . . . . . . . . . . . . 19
      

        
 
            
    
  |
156 | | sseq1 3486 |
. . . . . . . . . . . . . . . . . . . 20
         |
157 | 156 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . 19
      

        
 
            
     
    |
158 | 155, 157 | mpbird 232 |
. . . . . . . . . . . . . . . . . 18
      

        
 
            
   
  |
159 | 117, 158 | jca 532 |
. . . . . . . . . . . . . . . . 17
      

        
 
            
   
 

    |
160 | 159 | ex 434 |
. . . . . . . . . . . . . . . 16
      
 
 
 

   
 
           
 

        |
161 | 160 | eximdv 1677 |
. . . . . . . . . . . . . . 15
      
 
 
 

   
 
        
             
    |
162 | 161 | ex 434 |
. . . . . . . . . . . . . 14
           

 
  
              
 
  
         |
163 | 162 | com23 78 |
. . . . . . . . . . . . 13
           

 
          
              
      |
164 | | unieq 4208 |
. . . . . . . . . . . . . . . 16
 
   |
165 | 164 | sseq2d 3493 |
. . . . . . . . . . . . . . 15
       |
166 | 165 | rspcev 3179 |
. . . . . . . . . . . . . 14
               |
167 | 166 | exlimiv 1689 |
. . . . . . . . . . . . 13
       
     
   |
168 | 163, 167 | syl8 70 |
. . . . . . . . . . . 12
           

 
          
             
     |
169 | 98, 168 | mpd 15 |
. . . . . . . . . . 11
           

 
  
     
    |
170 | 93, 169 | sylan2b 475 |
. . . . . . . . . 10
                              |
171 | 170 | rexlimdva 2947 |
. . . . . . . . 9
   

                
 
      |
172 | 82, 171 | syl5bir 218 |
. . . . . . . 8
   

     
                
    |
173 | 80, 172 | sylbird 235 |
. . . . . . 7
   

        ↾t   

       
       ↾t   
         |
174 | 173 | ex 434 |
. . . . . 6
  

        ↾t   

       
       ↾t   
          |
175 | 174 | com23 78 |
. . . . 5
  

      ↾t    
              
↾t      
 
       |
176 | 54, 175 | syld 44 |
. . . 4
  

   

↾t     
↾t          ↾t     
          |
177 | 176 | ralrimdva 2912 |
. . 3
      ↾t      ↾t          ↾t       
          |
178 | 4 | cmpsublem 19135 |
. . 3
                 ↾t      ↾t          ↾t       |
179 | 177, 178 | impbid 191 |
. 2
      ↾t      ↾t          ↾t    
  
          |
180 | 13, 179 | bitrd 253 |
1
     ↾t 
   
          |