Step | Hyp | Ref
| Expression |
1 | | relres 5138 |
. . 3
         |
2 | 1 | a1i 11 |
. 2
   

                    |
3 | | dmfco 5954 |
. . . . . . . . 9
    
        |
4 | 3 | biimpd 212 |
. . . . . . . 8
    

       |
5 | 4 | funfni 5686 |
. . . . . . 7
 
  

       |
6 | | dmressnsn 5149 |
. . . . . . . 8
                     |
7 | | eleq2 2538 |
. . . . . . . . . 10
                       
         |
8 | | elsn 3973 |
. . . . . . . . . . 11
             |
9 | | dmressnsn 5149 |
. . . . . . . . . . . . . . . . 17
             |
10 | | dffun7 5615 |
. . . . . . . . . . . . . . . . . . 19
      
       
                   |
11 | | snidg 3986 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
    |
12 | 11 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
       |
13 | | eleq2 2538 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         
           |
14 | 13 | eqcoms 2479 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        
            |
15 | 14 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
     
         |
16 | 12, 15 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . 23
         
           |
17 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     |
18 | 17 | isseti 3037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
      |
19 | | eqcom 2478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
    
      |
20 | | fnbrfvb 5919 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
 
           |
21 | 19, 20 | syl5bb 265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
 
           |
22 | 21 | biimpd 212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 
           |
23 | | breq1 4398 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
           
     |
24 | 23 | eqcoms 2479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
           
     |
25 | 24 | biimpcd 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                 |
26 | 22, 25 | anim12ii 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
  

      
              |
27 | 26 | eximdv 1772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
  

      
 
               |
28 | 18, 27 | mpi 20 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
  

      
          |
29 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
   |
30 | | vex 3034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 |
31 | | brcog 5006 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
                 |
32 | 29, 30, 31 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 
                 |
33 | 32 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
  

      
    
           |
34 | 28, 33 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  

      
 
    |
35 | | snidg 3986 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     |
36 | 35 | biantrud 515 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     
           |
37 | 30 | brres 5117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
        
          |
38 | 36, 37 | syl6rbbr 272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                 |
39 | 38 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
  

      
        
 
     |
40 | 34, 39 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  

      
          |
41 | 40 | ex 441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 
                   |
42 | 41 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
            
   
 
                  |
43 | | breq1 4398 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                     |
44 | 43 | eqcoms 2479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                     |
45 | 44 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
            
   
 
        
           |
46 | 42, 45 | sylibd 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
            
   
 
                  |
47 | 46 | alrimiv 1781 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
            
   
 
                    |
48 | | moim 2368 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
         
                              |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            
   
 
                     |
50 | 49 | ex 441 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          

    

                      |
51 | 50 | com23 80 |
. . . . . . . . . . . . . . . . . . . . . . 23
          

    
         

            |
52 | 16, 51 | rspcimdv 3137 |
. . . . . . . . . . . . . . . . . . . . . 22
         
                    
 
             |
53 | 52 | ex 441 |
. . . . . . . . . . . . . . . . . . . . 21
        
                    
 
              |
54 | 53 | com13 82 |
. . . . . . . . . . . . . . . . . . . 20
 
                
  
 
        
             |
55 | 54 | adantl 473 |
. . . . . . . . . . . . . . . . . . 19
                                     
 
              |
56 | 10, 55 | sylbi 200 |
. . . . . . . . . . . . . . . . . 18
       
  
 
        
             |
57 | 56 | com13 82 |
. . . . . . . . . . . . . . . . 17
        
   
 
                    |
58 | 9, 57 | mpcom 36 |
. . . . . . . . . . . . . . . 16
   
 
                   |
59 | 58 | imp31 439 |
. . . . . . . . . . . . . . 15
   

                    |
60 | 17 | snid 3988 |
. . . . . . . . . . . . . . . . . 18
           |
61 | 60 | biantru 513 |
. . . . . . . . . . . . . . . . 17
      
                    |
62 | 61 | a1i 11 |
. . . . . . . . . . . . . . . 16
   

                                      |
63 | 62 | mobidv 2340 |
. . . . . . . . . . . . . . 15
   

                  
                       |
64 | 59, 63 | mpbid 215 |
. . . . . . . . . . . . . 14
   

                                |
65 | 64 | adantl 473 |
. . . . . . . . . . . . 13
                 
                         |
66 | | breq1 4398 |
. . . . . . . . . . . . . . . 16
                                 |
67 | 30 | brres 5117 |
. . . . . . . . . . . . . . . 16
              
                    |
68 | 66, 67 | syl6rbb 270 |
. . . . . . . . . . . . . . 15
                       
             |
69 | 68 | adantr 472 |
. . . . . . . . . . . . . 14
                 
                                   |
70 | 69 | mobidv 2340 |
. . . . . . . . . . . . 13
                 
                          
           |
71 | 65, 70 | mpbid 215 |
. . . . . . . . . . . 12
                 
   
            |
72 | 71 | ex 441 |
. . . . . . . . . . 11
                 
                |
73 | 8, 72 | sylbi 200 |
. . . . . . . . . 10
          
                         |
74 | 7, 73 | syl6bi 236 |
. . . . . . . . 9
                       
   

          
              |
75 | 74 | com23 80 |
. . . . . . . 8
                           
          
               |
76 | 6, 75 | syl 17 |
. . . . . . 7
                 
          
               |
77 | 5, 76 | syl6com 35 |
. . . . . 6
     
   

           
                       |
78 | 77 | a1d 25 |
. . . . 5
   
 
                   
          
                 |
79 | 78 | imp31 439 |
. . . 4
   

                      
          
               |
80 | 79 | pm2.43i 48 |
. . 3
   

           
                     |
81 | 80 | ralrimiv 2808 |
. 2
   

          

                     |
82 | | dffun7 5615 |
. 2
        
 
       
           
           |
83 | 2, 81, 82 | sylanbrc 677 |
1
   

                    |