Step | Hyp | Ref
| Expression |
1 | | fundmen.1 |
. . . 4
 |
2 | 1 | dmex 4889 |
. . 3
 |
3 | 2 | a1i 9 |
. 2

  |
4 | 1 | a1i 9 |
. 2

  |
5 | | funfvop 5624 |
. . 3
            |
6 | 5 | ex 115 |
. 2

           |
7 | | funrel 5229 |
. . 3

  |
8 | | elreldm 4849 |
. . . 4
       |
9 | 8 | ex 115 |
. . 3


     |
10 | 7, 9 | syl 14 |
. 2


     |
11 | | df-rel 4630 |
. . . . . . . . 9

    |
12 | 7, 11 | sylib 122 |
. . . . . . . 8

    |
13 | 12 | sselda 3155 |
. . . . . . 7
       |
14 | | elvv 4685 |
. . . . . . 7
  
  
     |
15 | 13, 14 | sylib 122 |
. . . . . 6
     
     |
16 | | inteq 3845 |
. . . . . . . . . . . . . . . . 17
           |
17 | 16 | inteqd 3847 |
. . . . . . . . . . . . . . . 16
             |
18 | | vex 2740 |
. . . . . . . . . . . . . . . . 17
 |
19 | | vex 2740 |
. . . . . . . . . . . . . . . . 17
 |
20 | 18, 19 | op1stb 4475 |
. . . . . . . . . . . . . . . 16
    
 |
21 | 17, 20 | eqtrdi 2226 |
. . . . . . . . . . . . . . 15
        |
22 | | eqeq1 2184 |
. . . . . . . . . . . . . . 15
         |
23 | 21, 22 | syl5ibr 156 |
. . . . . . . . . . . . . 14
          |
24 | | opeq1 3776 |
. . . . . . . . . . . . . 14
   
     |
25 | 23, 24 | syl6 33 |
. . . . . . . . . . . . 13
         
      |
26 | 25 | imp 124 |
. . . . . . . . . . . 12
   
            |
27 | | eqeq2 2187 |
. . . . . . . . . . . . . 14
          
      |
28 | 27 | biimprcd 160 |
. . . . . . . . . . . . 13
       
         |
29 | 28 | adantl 277 |
. . . . . . . . . . . 12
   
                 |
30 | 26, 29 | mpd 13 |
. . . . . . . . . . 11
   
         |
31 | 30 | ancoms 268 |
. . . . . . . . . 10
    
        |
32 | 31 | adantl 277 |
. . . . . . . . 9
  
              |
33 | 30 | eleq1d 2246 |
. . . . . . . . . . . . . . 15
   
           |
34 | 33 | adantl 277 |
. . . . . . . . . . . . . 14
    
    

      |
35 | | funopfv 5551 |
. . . . . . . . . . . . . . 15

           |
36 | 35 | adantr 276 |
. . . . . . . . . . . . . 14
    
    
           |
37 | 34, 36 | sylbid 150 |
. . . . . . . . . . . . 13
    
    

       |
38 | 37 | exp32 365 |
. . . . . . . . . . . 12

      
          |
39 | 38 | com24 87 |
. . . . . . . . . . 11


                |
40 | 39 | imp43 355 |
. . . . . . . . . 10
  
               |
41 | 40 | opeq2d 3783 |
. . . . . . . . 9
  
               
     |
42 | 32, 41 | eqtr4d 2213 |
. . . . . . . 8
  
                  |
43 | 42 | exp32 365 |
. . . . . . 7
      
              |
44 | 43 | exlimdvv 1897 |
. . . . . 6
                        |
45 | 15, 44 | mpd 13 |
. . . . 5
                |
46 | 45 | adantrl 478 |
. . . 4
  
               |
47 | | inteq 3845 |
. . . . . . . . 9
                   |
48 | 47 | inteqd 3847 |
. . . . . . . 8
                     |
49 | 48 | adantl 277 |
. . . . . . 7
  
                      |
50 | | vex 2740 |
. . . . . . . . 9
 |
51 | | funfvex 5528 |
. . . . . . . . 9
         |
52 | | op1stbg 4476 |
. . . . . . . . 9
               
  |
53 | 50, 51, 52 | sylancr 414 |
. . . . . . . 8
           
  |
54 | 53 | adantr 276 |
. . . . . . 7
  
                 
  |
55 | 49, 54 | eqtr2d 2211 |
. . . . . 6
  
             |
56 | 55 | ex 115 |
. . . . 5
                |
57 | 56 | adantrr 479 |
. . . 4
  
               |
58 | 46, 57 | impbid 129 |
. . 3
  
               |
59 | 58 | ex 115 |
. 2

 

  
           |
60 | 3, 4, 6, 10, 59 | en3d 6763 |
1

  |