Step | Hyp | Ref
| Expression |
1 | | brovpreldm 6873 |
. . 3
                    |
2 | | simpl 459 |
. . . . . . . . 9
 
   |
3 | | bropopvvv.p |
. . . . . . . . . 10
 
 
   |
4 | 3 | opabbidv 4466 |
. . . . . . . . 9
 
             |
5 | 2, 2, 4 | mpt2eq123dv 6353 |
. . . . . . . 8
 
              
    |
6 | | bropopvvv.o |
. . . . . . . 8
 
          |
7 | 5, 6 | ovmpt2ga 6426 |
. . . . . . 7
 
              
        |
8 | 7 | dmeqd 5037 |
. . . . . 6
 
                       |
9 | 8 | eleq2d 2514 |
. . . . 5
 
                
              |
10 | | dmoprabss 6378 |
. . . . . . . 8
     
          
   |
11 | 10 | sseli 3428 |
. . . . . . 7
  
      
          
       |
12 | | opelxp 4864 |
. . . . . . . 8
  
       |
13 | | df-br 4403 |
. . . . . . . . . . . . 13
          
             |
14 | | ne0i 3737 |
. . . . . . . . . . . . . 14
  
        
          |
15 | | bropopvvv.oo |
. . . . . . . . . . . . . . . . . . . 20
    
             
   |
16 | 15 | breqd 4413 |
. . . . . . . . . . . . . . . . . . 19
    
            
          |
17 | | brabv 6335 |
. . . . . . . . . . . . . . . . . . . . . 22
            |
18 | 17 | anim2i 573 |
. . . . . . . . . . . . . . . . . . . . 21
        
           |
19 | 18 | ex 436 |
. . . . . . . . . . . . . . . . . . . 20
 
        
 
       |
20 | 19 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
    
           


     |
21 | 16, 20 | sylbid 219 |
. . . . . . . . . . . . . . . . . 18
    
              


     |
22 | 21 | ex 436 |
. . . . . . . . . . . . . . . . 17
 
                


      |
23 | 22 | com23 81 |
. . . . . . . . . . . . . . . 16
 
                         |
24 | 23 | a1d 26 |
. . . . . . . . . . . . . . 15
 
                                   |
25 | 6 | mpt2ndm0 6510 |
. . . . . . . . . . . . . . . 16
         |
26 | | df-ov 6293 |
. . . . . . . . . . . . . . . . . 18
                    |
27 | | fveq1 5864 |
. . . . . . . . . . . . . . . . . 18
    
                    |
28 | 26, 27 | syl5eq 2497 |
. . . . . . . . . . . . . . . . 17
    
                 |
29 | | 0fv 5898 |
. . . . . . . . . . . . . . . . 17
        |
30 | 28, 29 | syl6eq 2501 |
. . . . . . . . . . . . . . . 16
    
          |
31 | | eqneqall 2634 |
. . . . . . . . . . . . . . . 16
        
        
            

 
 
       |
32 | 25, 30, 31 | 3syl 18 |
. . . . . . . . . . . . . . 15
                                     |
33 | 24, 32 | pm2.61i 168 |
. . . . . . . . . . . . . 14
        
            

 
 
      |
34 | 14, 33 | syl 17 |
. . . . . . . . . . . . 13
  
        
            

 
 
      |
35 | 13, 34 | sylbi 199 |
. . . . . . . . . . . 12
                                   |
36 | 35 | pm2.43i 49 |
. . . . . . . . . . 11
            

 
 
     |
37 | 36 | com12 32 |
. . . . . . . . . 10
 
               
     |
38 | 37 | anc2ri 561 |
. . . . . . . . 9
 
              
   

     |
39 | | df-3an 987 |
. . . . . . . . 9
      
 
      

    |
40 | 38, 39 | syl6ibr 231 |
. . . . . . . 8
 
               
 
     |
41 | 12, 40 | sylbi 199 |
. . . . . . 7
  
  
                
     |
42 | 11, 41 | syl 17 |
. . . . . 6
  
      
          
                
     |
43 | | df-mpt2 6295 |
. . . . . . 7
             
            |
44 | 43 | dmeqi 5036 |
. . . . . 6
              
 

        |
45 | 42, 44 | eleq2s 2547 |
. . . . 5
  
      
              


 
     |
46 | 9, 45 | syl6bi 232 |
. . . 4
 
                             


 
      |
47 | | 3ianor 1002 |
. . . . 5
   
      

     
     |
48 | | df-3or 986 |
. . . . . 6
       
       
         |
49 | | ianor 491 |
. . . . . . . 8
       |
50 | 25 | dmeqd 5037 |
. . . . . . . . . . 11
         |
51 | 50 | eleq2d 2514 |
. . . . . . . . . 10
          
      |
52 | | dm0 5048 |
. . . . . . . . . . 11
 |
53 | 52 | eleq2i 2521 |
. . . . . . . . . 10
  
      |
54 | 51, 53 | syl6bb 265 |
. . . . . . . . 9
          
      |
55 | | noel 3735 |
. . . . . . . . . 10
    |
56 | 55 | pm2.21i 135 |
. . . . . . . . 9
  
           
 
 
 
     |
57 | 54, 56 | syl6bi 232 |
. . . . . . . 8
                         
 
      |
58 | 49, 57 | sylbir 217 |
. . . . . . 7
                         
 
      |
59 | | anor 492 |
. . . . . . . . 9
 
 
   |
60 | | id 22 |
. . . . . . . . . . . . 13
   |
61 | 60 | ancri 555 |
. . . . . . . . . . . 12
 
   |
62 | 61 | adantr 467 |
. . . . . . . . . . 11
 
     |
63 | | mpt2exga 6869 |
. . . . . . . . . . 11
 
  
        |
64 | 62, 63 | syl 17 |
. . . . . . . . . 10
 
  
        |
65 | 64 | pm2.24d 138 |
. . . . . . . . 9
 
                                
 
       |
66 | 59, 65 | sylbir 217 |
. . . . . . . 8
 
   
                          


 
       |
67 | 66 | imp 431 |
. . . . . . 7
     
                             
 
      |
68 | 58, 67 | jaoi3 981 |
. . . . . 6
  
  
                             
 
      |
69 | 48, 68 | sylbi 199 |
. . . . 5
       
                         
 
      |
70 | 47, 69 | sylbi 199 |
. . . 4
   
                             
 
      |
71 | 46, 70 | pm2.61i 168 |
. . 3
  
                 


 
     |
72 | 1, 71 | syl 17 |
. 2
                       


 
     |
73 | 72 | pm2.43i 49 |
1
                
    |