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

  |
4 | 1 | a1i 9 |
. 2

  |
5 | | funfvop 5279 |
. . 3
            |
6 | 5 | ex 108 |
. 2

           |
7 | | funrel 4919 |
. . 3

  |
8 | | elreldm 4560 |
. . . 4
       |
9 | 8 | ex 108 |
. . 3


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


     |
11 | | df-rel 4352 |
. . . . . . . . 9

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

    |
13 | 12 | sselda 2945 |
. . . . . . 7
       |
14 | | elvv 4402 |
. . . . . . 7
  
  
     |
15 | 13, 14 | sylib 127 |
. . . . . 6
     
     |
16 | | inteq 3618 |
. . . . . . . . . . . . . . . . 17
           |
17 | 16 | inteqd 3620 |
. . . . . . . . . . . . . . . 16
             |
18 | | vex 2560 |
. . . . . . . . . . . . . . . . 17
 |
19 | | vex 2560 |
. . . . . . . . . . . . . . . . 17
 |
20 | 18, 19 | op1stb 4209 |
. . . . . . . . . . . . . . . 16
    
 |
21 | 17, 20 | syl6eq 2088 |
. . . . . . . . . . . . . . 15
        |
22 | | eqeq1 2046 |
. . . . . . . . . . . . . . 15
         |
23 | 21, 22 | syl5ibr 145 |
. . . . . . . . . . . . . 14
          |
24 | | opeq1 3549 |
. . . . . . . . . . . . . 14
   
     |
25 | 23, 24 | syl6 29 |
. . . . . . . . . . . . 13
         
      |
26 | 25 | imp 115 |
. . . . . . . . . . . 12
   
            |
27 | | eqeq2 2049 |
. . . . . . . . . . . . . 14
          
      |
28 | 27 | biimprcd 149 |
. . . . . . . . . . . . 13
       
         |
29 | 28 | adantl 262 |
. . . . . . . . . . . 12
   
                 |
30 | 26, 29 | mpd 13 |
. . . . . . . . . . 11
   
         |
31 | 30 | ancoms 255 |
. . . . . . . . . 10
    
        |
32 | 31 | adantl 262 |
. . . . . . . . 9
  
              |
33 | 30 | eleq1d 2106 |
. . . . . . . . . . . . . . 15
   
           |
34 | 33 | adantl 262 |
. . . . . . . . . . . . . 14
    
    

      |
35 | | funopfv 5213 |
. . . . . . . . . . . . . . 15

           |
36 | 35 | adantr 261 |
. . . . . . . . . . . . . 14
    
    
           |
37 | 34, 36 | sylbid 139 |
. . . . . . . . . . . . 13
    
    

       |
38 | 37 | exp32 347 |
. . . . . . . . . . . 12

      
          |
39 | 38 | com24 81 |
. . . . . . . . . . 11


                |
40 | 39 | imp43 337 |
. . . . . . . . . 10
  
               |
41 | 40 | opeq2d 3556 |
. . . . . . . . 9
  
               
     |
42 | 32, 41 | eqtr4d 2075 |
. . . . . . . 8
  
                  |
43 | 42 | exp32 347 |
. . . . . . 7
      
              |
44 | 43 | exlimdvv 1777 |
. . . . . 6
                        |
45 | 15, 44 | mpd 13 |
. . . . 5
                |
46 | 45 | adantrl 447 |
. . . 4
  
               |
47 | | inteq 3618 |
. . . . . . . . 9
                   |
48 | 47 | inteqd 3620 |
. . . . . . . 8
                     |
49 | 48 | adantl 262 |
. . . . . . 7
  
                      |
50 | | vex 2560 |
. . . . . . . . 9
 |
51 | | funfvex 5192 |
. . . . . . . . 9
         |
52 | | op1stbg 4210 |
. . . . . . . . 9
               
  |
53 | 50, 51, 52 | sylancr 393 |
. . . . . . . 8
           
  |
54 | 53 | adantr 261 |
. . . . . . 7
  
                 
  |
55 | 49, 54 | eqtr2d 2073 |
. . . . . 6
  
             |
56 | 55 | ex 108 |
. . . . 5
                |
57 | 56 | adantrr 448 |
. . . 4
  
               |
58 | 46, 57 | impbid 120 |
. . 3
  
               |
59 | 58 | ex 108 |
. 2

 

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

  |