Step | Hyp | Ref
| Expression |
1 | | brdomi 6749 |
. 2

       |
2 | | f1f 5422 |
. . . . . . . 8
           |
3 | | ffvelcdm 5650 |
. . . . . . . . 9
                   |
4 | 3 | ex 115 |
. . . . . . . 8
                   |
5 | 2, 4 | syl 14 |
. . . . . . 7
                   |
6 | 5 | anim2d 337 |
. . . . . 6
            
                |
7 | 6 | adantld 278 |
. . . . 5
           
       
        
           |
8 | | elxp4 5117 |
. . . . 5
  
     
       
       |
9 | | opelxp 4657 |
. . . . 5
               
              |
10 | 7, 8, 9 | 3imtr4g 205 |
. . . 4
            
             |
11 | 10 | adantl 277 |
. . 3
              
             |
12 | | elxp2 4645 |
. . . . . 6
  


     |
13 | | elxp2 4645 |
. . . . . 6
  


     |
14 | | vex 2741 |
. . . . . . . . . . . . . . . . . 18
 |
15 | | vex 2741 |
. . . . . . . . . . . . . . . . . . 19
 |
16 | | vex 2741 |
. . . . . . . . . . . . . . . . . . 19
 |
17 | 15, 16 | fvex 5536 |
. . . . . . . . . . . . . . . . . 18
     |
18 | 14, 17 | opth 4238 |
. . . . . . . . . . . . . . . . 17
                           |
19 | | f1fveq 5773 |
. . . . . . . . . . . . . . . . . . 19
      
          
   |
20 | 19 | ancoms 268 |
. . . . . . . . . . . . . . . . . 18
  

                 |
21 | 20 | anbi2d 464 |
. . . . . . . . . . . . . . . . 17
  

               

    |
22 | 18, 21 | bitrid 192 |
. . . . . . . . . . . . . . . 16
  

            
            |
23 | 22 | ex 115 |
. . . . . . . . . . . . . . 15
 
                    

     |
24 | 23 | ad2ant2l 508 |
. . . . . . . . . . . . . 14
  


                     

     |
25 | 24 | imp 124 |
. . . . . . . . . . . . 13
     
 
            
            |
26 | 25 | adantlr 477 |
. . . . . . . . . . . 12
      
 
        
            
            |
27 | | sneq 3604 |
. . . . . . . . . . . . . . . . . 18
             |
28 | 27 | dmeqd 4830 |
. . . . . . . . . . . . . . . . 17
   
 
       |
29 | 28 | unieqd 3821 |
. . . . . . . . . . . . . . . 16
      
        |
30 | 14, 16 | op1sta 5111 |
. . . . . . . . . . . . . . . 16
       |
31 | 29, 30 | eqtrdi 2226 |
. . . . . . . . . . . . . . 15
      
  |
32 | 27 | rneqd 4857 |
. . . . . . . . . . . . . . . . . 18
   
 
       |
33 | 32 | unieqd 3821 |
. . . . . . . . . . . . . . . . 17
      
        |
34 | 14, 16 | op2nda 5114 |
. . . . . . . . . . . . . . . . 17
       |
35 | 33, 34 | eqtrdi 2226 |
. . . . . . . . . . . . . . . 16
      
  |
36 | 35 | fveq2d 5520 |
. . . . . . . . . . . . . . 15
                 |
37 | 31, 36 | opeq12d 3787 |
. . . . . . . . . . . . . 14
        
                 |
38 | | sneq 3604 |
. . . . . . . . . . . . . . . . . 18
             |
39 | 38 | dmeqd 4830 |
. . . . . . . . . . . . . . . . 17
   
 
       |
40 | 39 | unieqd 3821 |
. . . . . . . . . . . . . . . 16
               |
41 | | vex 2741 |
. . . . . . . . . . . . . . . . 17
 |
42 | | vex 2741 |
. . . . . . . . . . . . . . . . 17
 |
43 | 41, 42 | op1sta 5111 |
. . . . . . . . . . . . . . . 16
       |
44 | 40, 43 | eqtrdi 2226 |
. . . . . . . . . . . . . . 15
         |
45 | 38 | rneqd 4857 |
. . . . . . . . . . . . . . . . . 18
   
 
       |
46 | 45 | unieqd 3821 |
. . . . . . . . . . . . . . . . 17
               |
47 | 41, 42 | op2nda 5114 |
. . . . . . . . . . . . . . . . 17
       |
48 | 46, 47 | eqtrdi 2226 |
. . . . . . . . . . . . . . . 16
         |
49 | 48 | fveq2d 5520 |
. . . . . . . . . . . . . . 15
                 |
50 | 44, 49 | opeq12d 3787 |
. . . . . . . . . . . . . 14
                          |
51 | 37, 50 | eqeqan12d 2193 |
. . . . . . . . . . . . 13
    
   
             
                              |
52 | 51 | ad2antlr 489 |
. . . . . . . . . . . 12
      
 
        
          
                                      |
53 | | eqeq12 2190 |
. . . . . . . . . . . . . 14
    
   

         |
54 | 14, 16 | opth 4238 |
. . . . . . . . . . . . . 14
       
   |
55 | 53, 54 | bitrdi 196 |
. . . . . . . . . . . . 13
    
   

     |
56 | 55 | ad2antlr 489 |
. . . . . . . . . . . 12
      
 
        
           |
57 | 26, 52, 56 | 3bitr4d 220 |
. . . . . . . . . . 11
      
 
        
          
                        |
58 | 57 | exp53 377 |
. . . . . . . . . 10
 
       
        
                                  |
59 | 58 | com23 78 |
. . . . . . . . 9
 
      

        
                                  |
60 | 59 | rexlimivv 2600 |
. . . . . . . 8
  
         
          
                           |
61 | 60 | rexlimdvv 2601 |
. . . . . . 7
  
    

                                        |
62 | 61 | imp 124 |
. . . . . 6
   
  


        
                               |
63 | 12, 13, 62 | syl2anb 291 |
. . . . 5
   
                                       |
64 | 63 | com12 30 |
. . . 4
        

       
                         |
65 | 64 | adantl 277 |
. . 3
          

       
                         |
66 | | xpdom.2 |
. . . . 5
 |
67 | | reldom 6745 |
. . . . . 6
 |
68 | 67 | brrelex1i 4670 |
. . . . 5

  |
69 | | xpexg 4741 |
. . . . 5
 
     |
70 | 66, 68, 69 | sylancr 414 |
. . . 4

    |
71 | 70 | adantr 276 |
. . 3
           |
72 | 67 | brrelex2i 4671 |
. . . . 5

  |
73 | | xpexg 4741 |
. . . . 5
 
     |
74 | 66, 72, 73 | sylancr 414 |
. . . 4

    |
75 | 74 | adantr 276 |
. . 3
           |
76 | 11, 65, 71, 75 | dom3d 6774 |
. 2
             |
77 | 1, 76 | exlimddv 1898 |
1

      |