Step | Hyp | Ref
| Expression |
1 | | r19.28av 2754 |
. . . 4
 
   
  
    |
2 | 1 | ralimi 2690 |
. . 3
 

   
   
    |
3 | | ssel 3268 |
. . . . . . . . . . . . 13

   
      |
4 | 3 | anim1d 547 |
. . . . . . . . . . . 12

      
     
       |
5 | | dffun4 5122 |
. . . . . . . . . . . . 13
           
       |
6 | | sp 1747 |
. . . . . . . . . . . . . . 15
           
         
   |
7 | 6 | sps 1754 |
. . . . . . . . . . . . . 14
         
           
     |
8 | 7 | sps 1754 |
. . . . . . . . . . . . 13
             
         
     |
9 | 5, 8 | sylbi 187 |
. . . . . . . . . . . 12
     
       |
10 | 4, 9 | syl9r 67 |
. . . . . . . . . . 11
 
      
      |
11 | 10 | adantl 452 |
. . . . . . . . . 10
       

        |
12 | | ssel 3268 |
. . . . . . . . . . . . 13

   
      |
13 | 12 | anim2d 548 |
. . . . . . . . . . . 12

      
     
       |
14 | | dffun4 5122 |
. . . . . . . . . . . . 13
           
       |
15 | | sp 1747 |
. . . . . . . . . . . . . . 15
           
         
   |
16 | 15 | sps 1754 |
. . . . . . . . . . . . . 14
         
         
       |
17 | 16 | sps 1754 |
. . . . . . . . . . . . 13
             
         
     |
18 | 14, 17 | sylbi 187 |
. . . . . . . . . . . 12
     
       |
19 | 13, 18 | syl9r 67 |
. . . . . . . . . . 11
 
      
      |
20 | 19 | adantr 451 |
. . . . . . . . . 10
       

        |
21 | 11, 20 | jaod 369 |
. . . . . . . . 9
    
       
      |
22 | 21 | imp 418 |
. . . . . . . 8
             
     |
23 | 22 | ralimi 2690 |
. . . . . . 7
 
  
   
      
     |
24 | 23 | ralimi 2690 |
. . . . . 6
 
      
     

       |
25 | | funeq 5128 |
. . . . . . . . . 10
 
   |
26 | | sseq1 3293 |
. . . . . . . . . . 11
     |
27 | | sseq2 3294 |
. . . . . . . . . . 11
     |
28 | 26, 27 | orbi12d 690 |
. . . . . . . . . 10
  
 
    |
29 | 25, 28 | anbi12d 691 |
. . . . . . . . 9
       
     |
30 | | sseq2 3294 |
. . . . . . . . . . 11
     |
31 | | sseq1 3293 |
. . . . . . . . . . 11
     |
32 | 30, 31 | orbi12d 690 |
. . . . . . . . . 10
  
 
    |
33 | 32 | anbi2d 684 |
. . . . . . . . 9
       
     |
34 | 29, 33 | cbvral2v 2844 |
. . . . . . . 8
 
  
     
    |
35 | | ralcom 2772 |
. . . . . . . . 9
 
  
     
    |
36 | | orcom 376 |
. . . . . . . . . . . 12
 
 
   |
37 | | sseq1 3293 |
. . . . . . . . . . . . 13
     |
38 | | sseq2 3294 |
. . . . . . . . . . . . 13
     |
39 | 37, 38 | orbi12d 690 |
. . . . . . . . . . . 12
  
 
    |
40 | 36, 39 | syl5bb 248 |
. . . . . . . . . . 11
  
 
    |
41 | 40 | anbi2d 684 |
. . . . . . . . . 10
       
     |
42 | | funeq 5128 |
. . . . . . . . . . 11
 
   |
43 | | sseq2 3294 |
. . . . . . . . . . . 12
     |
44 | | sseq1 3293 |
. . . . . . . . . . . 12
     |
45 | 43, 44 | orbi12d 690 |
. . . . . . . . . . 11
  
 
    |
46 | 42, 45 | anbi12d 691 |
. . . . . . . . . 10
       
     |
47 | 41, 46 | cbvral2v 2844 |
. . . . . . . . 9
 
  
     
    |
48 | 35, 47 | bitri 240 |
. . . . . . . 8
 
  
     
    |
49 | 34, 48 | anbi12i 678 |
. . . . . . 7
  
 
    

        
     
     |
50 | | anidm 625 |
. . . . . . 7
  
 
    

    
 
     |
51 | | anandir 802 |
. . . . . . . . 9
         
         |
52 | 51 | 2ralbii 2641 |
. . . . . . . 8
 
      
    
         |
53 | | r19.26-2 2748 |
. . . . . . . 8
 
   
           
     
     |
54 | 52, 53 | bitr2i 241 |
. . . . . . 7
  
  
   

    
         |
55 | 49, 50, 54 | 3bitr3i 266 |
. . . . . 6
 
  
            |
56 | | eluni 3895 |
. . . . . . . . . 10
  
           |
57 | | eluni 3895 |
. . . . . . . . . 10
  
           |
58 | 56, 57 | anbi12i 678 |
. . . . . . . . 9
       
         
     

    |
59 | | eeanv 1913 |
. . . . . . . . 9
         
    
        
     

    |
60 | | an4 797 |
. . . . . . . . . . 11
     
    
           
    |
61 | | ancom 437 |
. . . . . . . . . . 11
       
  
        
       |
62 | 60, 61 | bitri 240 |
. . . . . . . . . 10
     
    
        
       |
63 | 62 | 2exbii 1583 |
. . . . . . . . 9
         
    
            
       |
64 | 58, 59, 63 | 3bitr2i 264 |
. . . . . . . 8
       
             
       |
65 | 64 | imbi1i 315 |
. . . . . . 7
                        
        |
66 | | 19.23v 1891 |
. . . . . . . . 9
          
               
        |
67 | 66 | albii 1566 |
. . . . . . . 8
       
                 
             |
68 | | impexp 433 |
. . . . . . . . . 10
        
       
         
    |
69 | 68 | 2albii 1567 |
. . . . . . . . 9
       
                
    

        |
70 | | r2al 2652 |
. . . . . . . . 9
 
    

                  
      |
71 | 69, 70 | bitr4i 243 |
. . . . . . . 8
       
           
       
     |
72 | | 19.23v 1891 |
. . . . . . . 8
       
                      
        |
73 | 67, 71, 72 | 3bitr3ri 267 |
. . . . . . 7
       
           
       
     |
74 | 65, 73 | bitri 240 |
. . . . . 6
             
       
     |
75 | 24, 55, 74 | 3imtr4i 257 |
. . . . 5
 
  
         
  
   |
76 | 75 | alrimiv 1631 |
. . . 4
 
  
                  |
77 | 76 | alrimivv 1632 |
. . 3
 
  
                      |
78 | 2, 77 | syl 15 |
. 2
 

   
                    |
79 | | dffun4 5122 |
. 2
 
                    |
80 | 78, 79 | sylibr 203 |
1
 

   
   |