Step | Hyp | Ref
| Expression |
1 | | vex 2554 |
. . . 4
 |
2 | | vex 2554 |
. . . 4
 |
3 | 1, 2 | opex 3957 |
. . 3
  
 |
4 | | vex 2554 |
. . 3
 |
5 | | opexg 3955 |
. . 3
    

        |
6 | 3, 4, 5 | mp2an 402 |
. 2
       |
7 | 3, 4 | eqvinop 3971 |
. . . . 5
     
              
      |
8 | 7 | biimpi 113 |
. . . 4
     
              
      |
9 | | eqeq1 2043 |
. . . . . . . 8
         
        
    |
10 | | vex 2554 |
. . . . . . . . 9
 |
11 | | vex 2554 |
. . . . . . . . 9
 |
12 | 10, 11 | opth1 3964 |
. . . . . . . 8
      
  
     |
13 | 9, 12 | syl6bi 152 |
. . . . . . 7
         
       |
14 | 1, 2 | eqvinop 3971 |
. . . . . . . . 9
        
            |
15 | | opeq1 3540 |
. . . . . . . . . . . . 13
      
        |
16 | 15 | eqeq2d 2048 |
. . . . . . . . . . . 12
       
         |
17 | 1, 2, 4 | otth2 3969 |
. . . . . . . . . . . . . . . . . . 19
   
  
      
   |
18 | | df-3an 886 |
. . . . . . . . . . . . . . . . . . 19
 
  
    |
19 | 17, 18 | bitri 173 |
. . . . . . . . . . . . . . . . . 18
   
  
       

   |
20 | 19 | anbi1i 431 |
. . . . . . . . . . . . . . . . 17
      
     
 
  
     |
21 | | anass 381 |
. . . . . . . . . . . . . . . . 17
          
    |
22 | | anass 381 |
. . . . . . . . . . . . . . . . 17
  
            |
23 | 20, 21, 22 | 3bitri 195 |
. . . . . . . . . . . . . . . 16
      
     
 



     |
24 | 23 | 3exbii 1495 |
. . . . . . . . . . . . . . 15
            
     
 
       
      |
25 | | oprabidlem 5479 |
. . . . . . . . . . . . . . . . . 18
      

               |
26 | 25 | eximi 1488 |
. . . . . . . . . . . . . . . . 17
       
         
   
     |
27 | | excom 1551 |
. . . . . . . . . . . . . . . . 17
       
             
     |
28 | | excom 1551 |
. . . . . . . . . . . . . . . . 17
                 
   
     |
29 | 26, 27, 28 | 3imtr4i 190 |
. . . . . . . . . . . . . . . 16
       
         
   
     |
30 | | oprabidlem 5479 |
. . . . . . . . . . . . . . . 16
                     
     |
31 | | oprabidlem 5479 |
. . . . . . . . . . . . . . . . . 18
      
            |
32 | 31 | anim2i 324 |
. . . . . . . . . . . . . . . . 17
       
               |
33 | 32 | eximi 1488 |
. . . . . . . . . . . . . . . 16
        
                  |
34 | 29, 30, 33 | 3syl 17 |
. . . . . . . . . . . . . . 15
       
                   |
35 | 24, 34 | sylbi 114 |
. . . . . . . . . . . . . 14
            
     
 
  
           |
36 | | euequ1 1992 |
. . . . . . . . . . . . . . . . . . 19

 |
37 | | eupick 1976 |
. . . . . . . . . . . . . . . . . . 19
     
                      |
38 | 36, 37 | mpan 400 |
. . . . . . . . . . . . . . . . . 18
                         |
39 | | euequ1 1992 |
. . . . . . . . . . . . . . . . . . . 20
  |
40 | | eupick 1976 |
. . . . . . . . . . . . . . . . . . . 20
     
      
       |
41 | 39, 40 | mpan 400 |
. . . . . . . . . . . . . . . . . . 19
        

       |
42 | | euequ1 1992 |
. . . . . . . . . . . . . . . . . . . 20
  |
43 | | eupick 1976 |
. . . . . . . . . . . . . . . . . . . 20
     
  
   |
44 | 42, 43 | mpan 400 |
. . . . . . . . . . . . . . . . . . 19
     
   |
45 | 41, 44 | syl6 29 |
. . . . . . . . . . . . . . . . . 18
        


    |
46 | 38, 45 | syl6 29 |
. . . . . . . . . . . . . . . . 17
                     |
47 | 46 | 3impd 1117 |
. . . . . . . . . . . . . . . 16
                   |
48 | 17, 47 | syl5bi 141 |
. . . . . . . . . . . . . . 15
                  
     
    |
49 | 48 | com12 27 |
. . . . . . . . . . . . . 14
   
  
            
         |
50 | 35, 49 | syl5 28 |
. . . . . . . . . . . . 13
   
  
                  
     
 
   |
51 | | eqeq1 2043 |
. . . . . . . . . . . . . . 15
     
 
  
  
     
         |
52 | | eqcom 2039 |
. . . . . . . . . . . . . . 15
         
  
          
   |
53 | 51, 52 | syl6bb 185 |
. . . . . . . . . . . . . 14
     
 
  
  
          
    |
54 | 53 | anbi1d 438 |
. . . . . . . . . . . . . . . 16
     
     
  
      
     
     |
55 | 54 | 3exbidv 1746 |
. . . . . . . . . . . . . . 15
     
             
 
           
     
     |
56 | 55 | imbi1d 220 |
. . . . . . . . . . . . . 14
     
              
 
                   
 
    |
57 | 53, 56 | imbi12d 223 |
. . . . . . . . . . . . 13
     
     
  
          
  
      
  
                  
     
 
     |
58 | 50, 57 | mpbiri 157 |
. . . . . . . . . . . 12
     
 
  
  
          
  
     |
59 | 16, 58 | syl6bi 152 |
. . . . . . . . . . 11
           
  
          
  
      |
60 | 59 | adantr 261 |
. . . . . . . . . 10
                
                  
 
     |
61 | 60 | exlimivv 1773 |
. . . . . . . . 9
           
    
  

                  
 
     |
62 | 14, 61 | sylbi 114 |
. . . . . . . 8
           
  
          
  
      |
63 | 62 | com3l 75 |
. . . . . . 7
         
 
             
  
      |
64 | 13, 63 | mpdd 36 |
. . . . . 6
         
             
 
    |
65 | 64 | adantr 261 |
. . . . 5
          
    
                  
 
    |
66 | 65 | exlimivv 1773 |
. . . 4
           
          
  
          
  
     |
67 | 8, 66 | mpcom 32 |
. . 3
     
             
 
   |
68 | | 19.8a 1479 |
. . . . 5
        
  
  
  
   |
69 | | 19.8a 1479 |
. . . . 5
      
  
     
  
  
   |
70 | | 19.8a 1479 |
. . . . 5
          
 
                |
71 | 68, 69, 70 | 3syl 17 |
. . . 4
        
                |
72 | 71 | ex 108 |
. . 3
     
                   |
73 | 67, 72 | impbid 120 |
. 2
     
             
 
   |
74 | | df-oprab 5459 |
. 2
   
  
        
  
  
   |
75 | 6, 73, 74 | elab2 2684 |
1
   
  
   
  
   |