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

       |
2 | | f1f 5784 |
. . . . . . . 8
           |
3 | | ffvelrn 6025 |
. . . . . . . . 9
                   |
4 | 3 | ex 436 |
. . . . . . . 8
                   |
5 | 2, 4 | syl 17 |
. . . . . . 7
                   |
6 | 5 | anim2d 569 |
. . . . . 6
            
                |
7 | 6 | adantld 469 |
. . . . 5
           
       
        
           |
8 | | elxp4 6742 |
. . . . 5
  
     
       
       |
9 | | opelxp 4867 |
. . . . 5
               
              |
10 | 7, 8, 9 | 3imtr4g 274 |
. . . 4
            
             |
11 | 10 | adantl 468 |
. . 3
              
             |
12 | | elxp2 4855 |
. . . . . 6
  


     |
13 | | elxp2 4855 |
. . . . . 6
  


     |
14 | | vex 3050 |
. . . . . . . . . . . . . . . . . 18
 |
15 | | fvex 5880 |
. . . . . . . . . . . . . . . . . 18
     |
16 | 14, 15 | opth 4679 |
. . . . . . . . . . . . . . . . 17
                           |
17 | | f1fveq 6168 |
. . . . . . . . . . . . . . . . . . 19
      
          
   |
18 | 17 | ancoms 455 |
. . . . . . . . . . . . . . . . . 18
  

                 |
19 | 18 | anbi2d 711 |
. . . . . . . . . . . . . . . . 17
  

               

    |
20 | 16, 19 | syl5bb 261 |
. . . . . . . . . . . . . . . 16
  

            
            |
21 | 20 | ex 436 |
. . . . . . . . . . . . . . 15
 
                    

     |
22 | 21 | ad2ant2l 753 |
. . . . . . . . . . . . . 14
  


                     

     |
23 | 22 | imp 431 |
. . . . . . . . . . . . 13
     
 
            
            |
24 | 23 | adantlr 722 |
. . . . . . . . . . . 12
      
 
        
            
            |
25 | | sneq 3980 |
. . . . . . . . . . . . . . . . . 18
             |
26 | 25 | dmeqd 5040 |
. . . . . . . . . . . . . . . . 17
   
 
       |
27 | 26 | unieqd 4211 |
. . . . . . . . . . . . . . . 16
      
        |
28 | | vex 3050 |
. . . . . . . . . . . . . . . . 17
 |
29 | 14, 28 | op1sta 5321 |
. . . . . . . . . . . . . . . 16
       |
30 | 27, 29 | syl6eq 2503 |
. . . . . . . . . . . . . . 15
      
  |
31 | 25 | rneqd 5065 |
. . . . . . . . . . . . . . . . . 18
   
 
       |
32 | 31 | unieqd 4211 |
. . . . . . . . . . . . . . . . 17
      
        |
33 | 14, 28 | op2nda 5324 |
. . . . . . . . . . . . . . . . 17
       |
34 | 32, 33 | syl6eq 2503 |
. . . . . . . . . . . . . . . 16
      
  |
35 | 34 | fveq2d 5874 |
. . . . . . . . . . . . . . 15
                 |
36 | 30, 35 | opeq12d 4177 |
. . . . . . . . . . . . . 14
        
                 |
37 | | sneq 3980 |
. . . . . . . . . . . . . . . . . 18
             |
38 | 37 | dmeqd 5040 |
. . . . . . . . . . . . . . . . 17
   
 
       |
39 | 38 | unieqd 4211 |
. . . . . . . . . . . . . . . 16
               |
40 | | vex 3050 |
. . . . . . . . . . . . . . . . 17
 |
41 | | vex 3050 |
. . . . . . . . . . . . . . . . 17
 |
42 | 40, 41 | op1sta 5321 |
. . . . . . . . . . . . . . . 16
       |
43 | 39, 42 | syl6eq 2503 |
. . . . . . . . . . . . . . 15
         |
44 | 37 | rneqd 5065 |
. . . . . . . . . . . . . . . . . 18
   
 
       |
45 | 44 | unieqd 4211 |
. . . . . . . . . . . . . . . . 17
               |
46 | 40, 41 | op2nda 5324 |
. . . . . . . . . . . . . . . . 17
       |
47 | 45, 46 | syl6eq 2503 |
. . . . . . . . . . . . . . . 16
         |
48 | 47 | fveq2d 5874 |
. . . . . . . . . . . . . . 15
                 |
49 | 43, 48 | opeq12d 4177 |
. . . . . . . . . . . . . 14
                          |
50 | 36, 49 | eqeqan12d 2469 |
. . . . . . . . . . . . 13
    
   
             
                              |
51 | 50 | ad2antlr 734 |
. . . . . . . . . . . 12
      
 
        
          
                                      |
52 | | eqeq12 2466 |
. . . . . . . . . . . . . 14
    
   

         |
53 | 14, 28 | opth 4679 |
. . . . . . . . . . . . . 14
       
   |
54 | 52, 53 | syl6bb 265 |
. . . . . . . . . . . . 13
    
   

     |
55 | 54 | ad2antlr 734 |
. . . . . . . . . . . 12
      
 
        
           |
56 | 24, 51, 55 | 3bitr4d 289 |
. . . . . . . . . . 11
      
 
        
          
                        |
57 | 56 | exp53 623 |
. . . . . . . . . 10
 
       
        
                                  |
58 | 57 | com23 81 |
. . . . . . . . 9
 
      

        
                                  |
59 | 58 | rexlimivv 2886 |
. . . . . . . 8
  
         
          
                           |
60 | 59 | rexlimdvv 2887 |
. . . . . . 7
  
    

                                        |
61 | 60 | imp 431 |
. . . . . 6
   
  


        
                               |
62 | 12, 13, 61 | syl2anb 482 |
. . . . 5
   
                                       |
63 | 62 | com12 32 |
. . . 4
        

       
                         |
64 | 63 | adantl 468 |
. . 3
          

       
                         |
65 | | xpdom.2 |
. . . . 5
 |
66 | | reldom 7580 |
. . . . . 6
 |
67 | 66 | brrelexi 4878 |
. . . . 5

  |
68 | | xpexg 6598 |
. . . . 5
 
     |
69 | 65, 67, 68 | sylancr 670 |
. . . 4

    |
70 | 69 | adantr 467 |
. . 3
           |
71 | 66 | brrelex2i 4879 |
. . . . 5

  |
72 | | xpexg 6598 |
. . . . 5
 
     |
73 | 65, 71, 72 | sylancr 670 |
. . . 4

    |
74 | 73 | adantr 467 |
. . 3
           |
75 | 11, 64, 70, 74 | dom3d 7616 |
. 2
             |
76 | 1, 75 | exlimddv 1783 |
1

      |