Step | Hyp | Ref
| Expression |
1 | | funrel 4862 |
. . . . 5
   |
2 | 1 | adantr 261 |
. . . 4
  
     |
3 | 2 | ralimi 2378 |
. . 3
 
    
   |
4 | | reluni 4403 |
. . 3
 
   |
5 | 3, 4 | sylibr 137 |
. 2
 
    
   |
6 | | r19.28av 2443 |
. . . 4
  
   
      |
7 | 6 | ralimi 2378 |
. . 3
 
    
   
    |
8 | | ssel 2933 |
. . . . . . . . . . . . 13
       
   |
9 | 8 | anim1d 319 |
. . . . . . . . . . . 12
                     |
10 | | dffun4 4856 |
. . . . . . . . . . . . . . 15
                
    |
11 | 10 | simprbi 260 |
. . . . . . . . . . . . . 14
                   |
12 | 11 | 19.21bbi 1448 |
. . . . . . . . . . . . 13
               |
13 | 12 | 19.21bi 1447 |
. . . . . . . . . . . 12
        
    |
14 | 9, 13 | syl9r 67 |
. . . . . . . . . . 11
               |
15 | 14 | adantl 262 |
. . . . . . . . . 10
  
              |
16 | | ssel 2933 |
. . . . . . . . . . . . 13
       
   |
17 | 16 | anim2d 320 |
. . . . . . . . . . . 12
                     |
18 | | dffun4 4856 |
. . . . . . . . . . . . . . 15
            
   
    |
19 | 18 | simprbi 260 |
. . . . . . . . . . . . . 14
              
    |
20 | 19 | 19.21bbi 1448 |
. . . . . . . . . . . . 13
               |
21 | 20 | 19.21bi 1447 |
. . . . . . . . . . . 12
         
   |
22 | 17, 21 | syl9r 67 |
. . . . . . . . . . 11
          
    |
23 | 22 | adantr 261 |
. . . . . . . . . 10
  
              |
24 | 15, 23 | jaod 636 |
. . . . . . . . 9
  
 
     
   
    |
25 | 24 | imp 115 |
. . . . . . . 8
                   |
26 | 25 | ralimi 2378 |
. . . . . . 7
 
  
   
            |
27 | 26 | ralimi 2378 |
. . . . . 6
 
    
            
   |
28 | | funeq 4864 |
. . . . . . . . . 10
     |
29 | | sseq1 2960 |
. . . . . . . . . . 11
     |
30 | | sseq2 2961 |
. . . . . . . . . . 11
     |
31 | 29, 30 | orbi12d 706 |
. . . . . . . . . 10
  
 
    |
32 | 28, 31 | anbi12d 442 |
. . . . . . . . 9
             |
33 | | sseq2 2961 |
. . . . . . . . . . 11
     |
34 | | sseq1 2960 |
. . . . . . . . . . 11
     |
35 | 33, 34 | orbi12d 706 |
. . . . . . . . . 10
  
 
    |
36 | 35 | anbi2d 437 |
. . . . . . . . 9
             |
37 | 32, 36 | cbvral2v 2535 |
. . . . . . . 8
 
  
     
    |
38 | | ralcom 2467 |
. . . . . . . . 9
 
  
     
    |
39 | | orcom 646 |
. . . . . . . . . . . 12
 
     |
40 | | sseq1 2960 |
. . . . . . . . . . . . 13
     |
41 | | sseq2 2961 |
. . . . . . . . . . . . 13
     |
42 | 40, 41 | orbi12d 706 |
. . . . . . . . . . . 12
  
 
    |
43 | 39, 42 | syl5bb 181 |
. . . . . . . . . . 11
  
 
    |
44 | 43 | anbi2d 437 |
. . . . . . . . . 10
             |
45 | | funeq 4864 |
. . . . . . . . . . 11
     |
46 | | sseq2 2961 |
. . . . . . . . . . . 12
     |
47 | | sseq1 2960 |
. . . . . . . . . . . 12
     |
48 | 46, 47 | orbi12d 706 |
. . . . . . . . . . 11
  
 
    |
49 | 45, 48 | anbi12d 442 |
. . . . . . . . . 10
             |
50 | 44, 49 | cbvral2v 2535 |
. . . . . . . . 9
 
  
     
    |
51 | 38, 50 | bitri 173 |
. . . . . . . 8
 
  
     
    |
52 | 37, 51 | anbi12i 433 |
. . . . . . 7
  
      
         
     
     |
53 | | anidm 376 |
. . . . . . 7
  
      
     
       |
54 | | anandir 525 |
. . . . . . . . 9
                   |
55 | 54 | 2ralbii 2326 |
. . . . . . . 8
 
    
        
       |
56 | | r19.26-2 2436 |
. . . . . . . 8
 
     
         
     
     |
57 | 55, 56 | bitr2i 174 |
. . . . . . 7
  
      
     
         |
58 | 52, 53, 57 | 3bitr3i 199 |
. . . . . 6
 
  
       
    |
59 | | eluni 3574 |
. . . . . . . . . 10
          
   |
60 | | eluni 3574 |
. . . . . . . . . 10
          
   |
61 | 59, 60 | anbi12i 433 |
. . . . . . . . 9
          
                  |
62 | | eeanv 1804 |
. . . . . . . . 9
                                   |
63 | | an4 520 |
. . . . . . . . . . 11
                    
      |
64 | | ancom 253 |
. . . . . . . . . . 11
              
            |
65 | 63, 64 | bitri 173 |
. . . . . . . . . 10
              
            |
66 | 65 | 2exbii 1494 |
. . . . . . . . 9
                              
    |
67 | 61, 62, 66 | 3bitr2i 197 |
. . . . . . . 8
          
             
    |
68 | 67 | imbi1i 227 |
. . . . . . 7
        
  
       
    
        |
69 | | 19.23v 1760 |
. . . . . . 7
       
    
                    
 
   |
70 | | r2al 2337 |
. . . . . . . 8
 
         
      
         
    |
71 | | impexp 250 |
. . . . . . . . 9
           
 
  
     
   
    |
72 | 71 | 2albii 1357 |
. . . . . . . 8
       
    
           
         
    |
73 | | 19.23v 1760 |
. . . . . . . . 9
             
 
             
 
   |
74 | 73 | albii 1356 |
. . . . . . . 8
       
    
            
    
        |
75 | 70, 72, 74 | 3bitr2ri 198 |
. . . . . . 7
       
    
      
             |
76 | 68, 69, 75 | 3bitr2i 197 |
. . . . . 6
        
  
 
             |
77 | 27, 58, 76 | 3imtr4i 190 |
. . . . 5
 
  
            
   |
78 | 77 | alrimiv 1751 |
. . . 4
 
  
           
  
   |
79 | 78 | alrimivv 1752 |
. . 3
 
  
               
  
   |
80 | 7, 79 | syl 14 |
. 2
 
    
             
  
   |
81 | | dffun4 4856 |
. 2
 
               
  
    |
82 | 5, 80, 81 | sylanbrc 394 |
1
 
    
   |