Step | Hyp | Ref
| Expression |
1 | | anass 661 |
. 2
   

   

      
 
 
  

          |
2 | | df-3an 1009 |
. . 3
 
  
 
      |
3 | 2 | anbi1i 709 |
. 2
  
    
      
   
              |
4 | | df-cvm 30051 |
. . . 4
CovMap                        

 
           ↾t    
↾t         |
5 | 4 | elmpt2cl 6530 |
. . 3
  CovMap 
    |
6 | | oveq12 6317 |
. . . . . . 7
 
       |
7 | | simpr 468 |
. . . . . . . . . 10
 
   |
8 | 7 | unieqd 4200 |
. . . . . . . . 9
 
     |
9 | | iscvm.2 |
. . . . . . . . 9
  |
10 | 8, 9 | syl6eqr 2523 |
. . . . . . . 8
 
    |
11 | | simpl 464 |
. . . . . . . . . . . . 13
 
   |
12 | 11 | pweqd 3947 |
. . . . . . . . . . . 12
 
     |
13 | 12 | difeq1d 3539 |
. . . . . . . . . . 11
 
             |
14 | | oveq1 6315 |
. . . . . . . . . . . . . . . 16
  ↾t   ↾t    |
15 | | oveq1 6315 |
. . . . . . . . . . . . . . . 16
  ↾t   ↾t    |
16 | 14, 15 | oveqan12d 6327 |
. . . . . . . . . . . . . . 15
 
   ↾t    
↾t     ↾t     ↾t     |
17 | 16 | eleq2d 2534 |
. . . . . . . . . . . . . 14
 
     
↾t     ↾t  
   
↾t     ↾t      |
18 | 17 | anbi2d 718 |
. . . . . . . . . . . . 13
 
          
    ↾t    
↾t            
    ↾t    
↾t       |
19 | 18 | ralbidv 2829 |
. . . . . . . . . . . 12
 
           
    ↾t    
↾t             
    ↾t    
↾t       |
20 | 19 | anbi2d 718 |
. . . . . . . . . . 11
 
                      
↾t     ↾t            
 

         
↾t     ↾t        |
21 | 13, 20 | rexeqbidv 2988 |
. . . . . . . . . 10
 
               

 
           ↾t    
↾t    
             

 
           ↾t    
↾t        |
22 | 21 | anbi2d 718 |
. . . . . . . . 9
 
                

 
           ↾t    
↾t     

             

 
           ↾t    
↾t         |
23 | 7, 22 | rexeqbidv 2988 |
. . . . . . . 8
 
                 

 
           ↾t    
↾t     


             

 
           ↾t    
↾t         |
24 | 10, 23 | raleqbidv 2987 |
. . . . . . 7
 
     

             

 
           ↾t    
↾t     



             

 
           ↾t    
↾t         |
25 | 6, 24 | rabeqbidv 3026 |
. . . . . 6
 
       

             

 
           ↾t    
↾t          


             

 
           ↾t    
↾t         |
26 | | ovex 6336 |
. . . . . . 7
   |
27 | 26 | rabex 4550 |
. . . . . 6
   

                            
↾t     ↾t        |
28 | 25, 4, 27 | ovmpt2a 6446 |
. . . . 5
 
  CovMap     


             

 
           ↾t    
↾t         |
29 | 28 | eleq2d 2534 |
. . . 4
 
   CovMap 
    

        
                  
↾t     ↾t          |
30 | | id 22 |
. . . . . . . . . . . 12
   |
31 | | pwexg 4585 |
. . . . . . . . . . . . . 14
 
  |
32 | 31 | adantr 472 |
. . . . . . . . . . . . 13
 
    |
33 | | difexg 4545 |
. . . . . . . . . . . . 13
         |
34 | | rabexg 4549 |
. . . . . . . . . . . . 13
                            
    ↾t    
↾t        |
35 | 32, 33, 34 | 3syl 18 |
. . . . . . . . . . . 12
 
                       
    ↾t    
↾t        |
36 | | iscvm.1 |
. . . . . . . . . . . . 13
                       
    ↾t    
↾t        |
37 | 36 | fvmpt2 5972 |
. . . . . . . . . . . 12
         
                  
↾t     ↾t                        
 

         
↾t     ↾t        |
38 | 30, 35, 37 | syl2anr 486 |
. . . . . . . . . . 11
   

           
                  
↾t     ↾t        |
39 | 38 | neeq1d 2702 |
. . . . . . . . . 10
   

                           
    ↾t    
↾t         |
40 | | rabn0 3755 |
. . . . . . . . . 10
        
                  
↾t     ↾t     
                       
    ↾t    
↾t       |
41 | 39, 40 | syl6bb 269 |
. . . . . . . . 9
   

             
                  
↾t     ↾t        |
42 | 41 | anbi2d 718 |
. . . . . . . 8
   

      

                       
    ↾t    
↾t         |
43 | 42 | rexbidva 2889 |
. . . . . . 7
 
        
 
        
                  
↾t     ↾t         |
44 | 43 | ralbidv 2829 |
. . . . . 6
 
         
 

        
                  
↾t     ↾t         |
45 | 44 | anbi2d 718 |
. . . . 5
 
    



     
  



                       
    ↾t    
↾t          |
46 | | cnveq 5013 |
. . . . . . . . . . . . 13
 
   |
47 | 46 | imaeq1d 5173 |
. . . . . . . . . . . 12
             |
48 | 47 | eqeq2d 2481 |
. . . . . . . . . . 11
  
              |
49 | | reseq1 5105 |
. . . . . . . . . . . . . 14
       |
50 | 49 | eleq1d 2533 |
. . . . . . . . . . . . 13
      ↾t     ↾t  
   
↾t     ↾t      |
51 | 50 | anbi2d 718 |
. . . . . . . . . . . 12
          
    ↾t    
↾t            
    ↾t    
↾t       |
52 | 51 | ralbidv 2829 |
. . . . . . . . . . 11
  
        
    ↾t    
↾t             
    ↾t    
↾t       |
53 | 48, 52 | anbi12d 725 |
. . . . . . . . . 10
         
 

         
↾t     ↾t            
 

         
↾t     ↾t        |
54 | 53 | rexbidv 2892 |
. . . . . . . . 9
  
 
                        
↾t     ↾t     
 
           
 

         
↾t     ↾t        |
55 | 54 | anbi2d 718 |
. . . . . . . 8
                

 
           ↾t    
↾t     

                       
    ↾t    
↾t         |
56 | 55 | rexbidv 2892 |
. . . . . . 7
  

        
                  
↾t     ↾t       
        
                  
↾t     ↾t         |
57 | 56 | ralbidv 2829 |
. . . . . 6
  


        
                  
↾t     ↾t       

        
                  
↾t     ↾t         |
58 | 57 | elrab 3184 |
. . . . 5
    


             

 
           ↾t    
↾t                                    
    ↾t    
↾t         |
59 | 45, 58 | syl6bbr 271 |
. . . 4
 
    



     
    

        
                  
↾t     ↾t          |
60 | 29, 59 | bitr4d 264 |
. . 3
 
   CovMap 
  



         |
61 | 5, 60 | biadan2 654 |
. 2
  CovMap     
  

          |
62 | 1, 3, 61 | 3bitr4ri 286 |
1
  CovMap       

         |