Proof of Theorem cvmsval
Step | Hyp | Ref
| Expression |
1 | | cvmcov.1 |
. . 3
                       
    ↾t    
↾t        |
2 | 1 | cvmsi 30000 |
. 2
     

  
              
    ↾t    
↾t        |
3 | | 3anass 990 |
. . 3
  
  
              
    ↾t    
↾t     

 
                 
    ↾t    
↾t         |
4 | | id 22 |
. . . . . . . 8
   |
5 | | pwexg 4590 |
. . . . . . . . 9
 
  |
6 | | difexg 4554 |
. . . . . . . . 9
         |
7 | | rabexg 4556 |
. . . . . . . . 9
                            
    ↾t    
↾t        |
8 | 5, 6, 7 | 3syl 18 |
. . . . . . . 8
              
 

         
↾t     ↾t        |
9 | | imaeq2 5167 |
. . . . . . . . . . . 12
             |
10 | 9 | eqeq2d 2463 |
. . . . . . . . . . 11
  
     
        |
11 | | oveq2 6303 |
. . . . . . . . . . . . . . 15
  ↾t   ↾t    |
12 | 11 | oveq2d 6311 |
. . . . . . . . . . . . . 14
  
↾t     ↾t    
↾t     ↾t     |
13 | 12 | eleq2d 2516 |
. . . . . . . . . . . . 13
      ↾t     ↾t  
   
↾t     ↾t      |
14 | 13 | anbi2d 711 |
. . . . . . . . . . . 12
          
    ↾t    
↾t            
    ↾t    
↾t       |
15 | 14 | ralbidv 2829 |
. . . . . . . . . . 11
  
        
    ↾t    
↾t             
    ↾t    
↾t       |
16 | 10, 15 | anbi12d 718 |
. . . . . . . . . 10
         
 

         
↾t     ↾t            
 

         
↾t     ↾t        |
17 | 16 | rabbidv 3038 |
. . . . . . . . 9
              
 

         
↾t     ↾t                   
 

         
↾t     ↾t        |
18 | 17, 1 | fvmptg 5951 |
. . . . . . . 8
         
                  
↾t     ↾t                        
 

         
↾t     ↾t        |
19 | 4, 8, 18 | syl2anr 481 |
. . . . . . 7
 
                  
 

         
↾t     ↾t        |
20 | 19 | eleq2d 2516 |
. . . . . 6
 
                   
 

         
↾t     ↾t         |
21 | | unieq 4209 |
. . . . . . . . . 10
     |
22 | 21 | eqeq1d 2455 |
. . . . . . . . 9
  
     
        |
23 | | difeq1 3546 |
. . . . . . . . . . . 12
 
         |
24 | 23 | raleqdv 2995 |
. . . . . . . . . . 11
  

                 |
25 | 24 | anbi1d 712 |
. . . . . . . . . 10
          
    ↾t    
↾t            
    ↾t    
↾t       |
26 | 25 | raleqbi1dv 2997 |
. . . . . . . . 9
  
        
    ↾t    
↾t    
            
↾t     ↾t       |
27 | 22, 26 | anbi12d 718 |
. . . . . . . 8
         
 

         
↾t     ↾t            
 
           ↾t     ↾t        |
28 | 27 | elrab 3198 |
. . . . . . 7
              
 

         
↾t     ↾t                            
    ↾t    
↾t        |
29 | | eldifsn 4100 |
. . . . . . . . 9
     
     |
30 | | elpw2g 4569 |
. . . . . . . . . . 11
 
    |
31 | 30 | adantr 467 |
. . . . . . . . . 10
 
  
   |
32 | 31 | anbi1d 712 |
. . . . . . . . 9
 
    
     |
33 | 29, 32 | syl5bb 261 |
. . . . . . . 8
 
      
     |
34 | 33 | anbi1d 712 |
. . . . . . 7
 
                        
    ↾t    
↾t     
    
              
    ↾t    
↾t         |
35 | 28, 34 | syl5bb 261 |
. . . . . 6
 
         
                  
↾t     ↾t          
              
    ↾t    
↾t         |
36 | 20, 35 | bitrd 257 |
. . . . 5
 
                         
    ↾t    
↾t         |
37 | 36 | biimprd 227 |
. . . 4
 
      
              
    ↾t    
↾t             |
38 | 37 | expimpd 608 |
. . 3
                      
    ↾t    
↾t      
       |
39 | 3, 38 | syl5bi 221 |
. 2
   
                 
    ↾t    
↾t             |
40 | 2, 39 | impbid2 208 |
1
 
   

   
              
    ↾t    
↾t         |