Step | Hyp | Ref
| Expression |
1 | | funrel 5234 |
. . . . 5

  |
2 | 1 | adantr 276 |
. . . 4
  

 
  |
3 | 2 | ralimi 2540 |
. . 3
 


   
  |
4 | | reluni 4750 |
. . 3
 
   |
5 | 3, 4 | sylibr 134 |
. 2
 


      |
6 | | r19.28av 2613 |
. . . 4
  

    
    |
7 | 6 | ralimi 2540 |
. . 3
 


   

 
    |
8 | | ssel 3150 |
. . . . . . . . . . . . 13
    
      |
9 | 8 | anim1d 336 |
. . . . . . . . . . . 12
         
           |
10 | | dffun4 5228 |
. . . . . . . . . . . . . . 15
            
   
    |
11 | 10 | simprbi 275 |
. . . . . . . . . . . . . 14

              
   |
12 | 11 | 19.21bbi 1559 |
. . . . . . . . . . . . 13

              |
13 | 12 | 19.21bi 1558 |
. . . . . . . . . . . 12

    
   
   |
14 | 9, 13 | syl9r 73 |
. . . . . . . . . . 11


    
   
    |
15 | 14 | adantl 277 |
. . . . . . . . . 10
   
        
    |
16 | | ssel 3150 |
. . . . . . . . . . . . 13
    
      |
17 | 16 | anim2d 337 |
. . . . . . . . . . . 12
         
           |
18 | | dffun4 5228 |
. . . . . . . . . . . . . . 15
            
   
    |
19 | 18 | simprbi 275 |
. . . . . . . . . . . . . 14

              
   |
20 | 19 | 19.21bbi 1559 |
. . . . . . . . . . . . 13

              |
21 | 20 | 19.21bi 1558 |
. . . . . . . . . . . 12

    
   
   |
22 | 17, 21 | syl9r 73 |
. . . . . . . . . . 11


    
   
    |
23 | 22 | adantr 276 |
. . . . . . . . . 10
   
        
    |
24 | 15, 23 | jaod 717 |
. . . . . . . . 9
    
     
   
    |
25 | 24 | imp 124 |
. . . . . . . 8
    
      
   
   |
26 | 25 | ralimi 2540 |
. . . . . . 7
 
 
 
               |
27 | 26 | ralimi 2540 |
. . . . . 6
 

 
 
   
            |
28 | | funeq 5237 |
. . . . . . . . . 10
 
   |
29 | | sseq1 3179 |
. . . . . . . . . . 11
 
   |
30 | | sseq2 3180 |
. . . . . . . . . . 11
 
   |
31 | 29, 30 | orbi12d 793 |
. . . . . . . . . 10
  
 
    |
32 | 28, 31 | anbi12d 473 |
. . . . . . . . 9
  

   
     |
33 | | sseq2 3180 |
. . . . . . . . . . 11
 
   |
34 | | sseq1 3179 |
. . . . . . . . . . 11
 
   |
35 | 33, 34 | orbi12d 793 |
. . . . . . . . . 10
  
 
    |
36 | 35 | anbi2d 464 |
. . . . . . . . 9
  

   
     |
37 | 32, 36 | cbvral2v 2717 |
. . . . . . . 8
 



  

 
    |
38 | | ralcom 2640 |
. . . . . . . . 9
 



  

 
    |
39 | | orcom 728 |
. . . . . . . . . . . 12
 

    |
40 | | sseq1 3179 |
. . . . . . . . . . . . 13
 
   |
41 | | sseq2 3180 |
. . . . . . . . . . . . 13
 
   |
42 | 40, 41 | orbi12d 793 |
. . . . . . . . . . . 12
  
 
    |
43 | 39, 42 | bitrid 192 |
. . . . . . . . . . 11
  
 
    |
44 | 43 | anbi2d 464 |
. . . . . . . . . 10
  

   
     |
45 | | funeq 5237 |
. . . . . . . . . . 11
 
   |
46 | | sseq2 3180 |
. . . . . . . . . . . 12
 
   |
47 | | sseq1 3179 |
. . . . . . . . . . . 12
 
   |
48 | 46, 47 | orbi12d 793 |
. . . . . . . . . . 11
  
 
    |
49 | 45, 48 | anbi12d 473 |
. . . . . . . . . 10
  

   
     |
50 | 44, 49 | cbvral2v 2717 |
. . . . . . . . 9
 



  

 
    |
51 | 38, 50 | bitri 184 |
. . . . . . . 8
 



  

 
    |
52 | 37, 51 | anbi12i 460 |
. . . . . . 7
   
 
     
  
 

     


     |
53 | | anidm 396 |
. . . . . . 7
   
 
     
  


 
    |
54 | | anandir 591 |
. . . . . . . . 9
    
    
         |
55 | 54 | 2ralbii 2485 |
. . . . . . . 8
 

 
 
  

  
         |
56 | | r19.26-2 2606 |
. . . . . . . 8
 

 

 
 
       
  

 
     |
57 | 55, 56 | bitr2i 185 |
. . . . . . 7
   
 
     
  


  
     |
58 | 52, 53, 57 | 3bitr3i 210 |
. . . . . 6
 



  

   
    |
59 | | eluni 3813 |
. . . . . . . . . 10
    
         |
60 | | eluni 3813 |
. . . . . . . . . 10
    
         |
61 | 59, 60 | anbi12i 460 |
. . . . . . . . 9
          
      

          |
62 | | eeanv 1932 |
. . . . . . . . 9
              
 
      

          |
63 | | an4 586 |
. . . . . . . . . . 11
          
 
    
         |
64 | | ancom 266 |
. . . . . . . . . . 11
            
 
            |
65 | 63, 64 | bitri 184 |
. . . . . . . . . 10
          
 
 
            |
66 | 65 | 2exbii 1606 |
. . . . . . . . 9
              
 
          
       |
67 | 61, 62, 66 | 3bitr2i 208 |
. . . . . . . 8
          
          
       |
68 | 67 | imbi1i 238 |
. . . . . . 7
                        
        |
69 | | 19.23v 1883 |
. . . . . . 7
            
     
      
             |
70 | | r2al 2496 |
. . . . . . . 8
 

        

               
    |
71 | | impexp 263 |
. . . . . . . . 9
        
     
 
              |
72 | 71 | 2albii 1471 |
. . . . . . . 8
       

                         
    |
73 | | 19.23v 1883 |
. . . . . . . . 9
     
          
         
        |
74 | 73 | albii 1470 |
. . . . . . . 8
       

                     
        |
75 | 70, 72, 74 | 3bitr2ri 209 |
. . . . . . 7
            
     


    
   
   |
76 | 68, 69, 75 | 3bitr2i 208 |
. . . . . 6
             

            |
77 | 27, 58, 76 | 3imtr4i 201 |
. . . . 5
 



                |
78 | 77 | alrimiv 1874 |
. . . 4
 



                  |
79 | 78 | alrimivv 1875 |
. . 3
 



                      |
80 | 7, 79 | syl 14 |
. 2
 


                       |
81 | | dffun4 5228 |
. 2
 
                       |
82 | 5, 80, 81 | sylanbrc 417 |
1
 


      |