Step | Hyp | Ref
| Expression |
1 | | df-rel 4630 |
. 2
           |
2 | | dfss2 3144 |
. . . . 5
  
              |
3 | | vex 2740 |
. . . . . . . . . 10
 |
4 | | relop.1 |
. . . . . . . . . 10
 |
5 | | relop.2 |
. . . . . . . . . 10
 |
6 | 3, 4, 5 | elop 4228 |
. . . . . . . . 9
      
      |
7 | | elvv 4685 |
. . . . . . . . 9
  
        |
8 | 6, 7 | imbi12i 239 |
. . . . . . . 8
    

     
 
 
  
      |
9 | | jaob 710 |
. . . . . . . 8
    
      
                 
           |
10 | 8, 9 | bitri 184 |
. . . . . . 7
    

               
           |
11 | 10 | albii 1470 |
. . . . . 6
         
            
      
       |
12 | | 19.26 1481 |
. . . . . 6
                
              
  
   
    
           |
13 | 11, 12 | bitri 184 |
. . . . 5
         
            
    
           |
14 | 2, 13 | bitri 184 |
. . . 4
  
                     
  
       |
15 | 4 | snex 4182 |
. . . . . . 7
 
 |
16 | | eqeq1 2184 |
. . . . . . . 8
     
       |
17 | | eqeq1 2184 |
. . . . . . . . . 10
      
 
      |
18 | | eqcom 2179 |
. . . . . . . . . . 11
     
  
    |
19 | | vex 2740 |
. . . . . . . . . . . 12
 |
20 | | vex 2740 |
. . . . . . . . . . . 12
 |
21 | 19, 20, 4 | opeqsn 4249 |
. . . . . . . . . . 11
     

     |
22 | 18, 21 | bitri 184 |
. . . . . . . . . 10
     

     |
23 | 17, 22 | bitrdi 196 |
. . . . . . . . 9
      

      |
24 | 23 | 2exbidv 1868 |
. . . . . . . 8
      
  
           |
25 | 16, 24 | imbi12d 234 |
. . . . . . 7
             
  
              |
26 | 15, 25 | spcv 2831 |
. . . . . 6
            
    
           |
27 | | sneq 3602 |
. . . . . . . . 9
  
    |
28 | 27 | eqeq2d 2189 |
. . . . . . . 8
 
       |
29 | 28 | cbvexv 1918 |
. . . . . . 7
   

    |
30 | | a9ev 1697 |
. . . . . . . . . 10
  |
31 | | equcom 1706 |
. . . . . . . . . . 11

  |
32 | 31 | exbii 1605 |
. . . . . . . . . 10
  
  |
33 | 30, 32 | mpbi 145 |
. . . . . . . . 9

 |
34 | | 19.41v 1902 |
. . . . . . . . 9
              |
35 | 33, 34 | mpbiran 940 |
. . . . . . . 8
           |
36 | 35 | exbii 1605 |
. . . . . . 7
     
  

    |
37 | | eqid 2177 |
. . . . . . . 8
 
   |
38 | 37 | a1bi 243 |
. . . . . . 7
     
  
  
 
           |
39 | 29, 36, 38 | 3bitr2ri 209 |
. . . . . 6
                    |
40 | 26, 39 | sylib 122 |
. . . . 5
            

    |
41 | | eqid 2177 |
. . . . . 6
    
  |
42 | | prexg 4208 |
. . . . . . . 8
 
   
  |
43 | 4, 5, 42 | mp2an 426 |
. . . . . . 7
    |
44 | | eqeq1 2184 |
. . . . . . . 8
   
   
  
      |
45 | | eqeq1 2184 |
. . . . . . . . 9
   
      
      |
46 | 45 | 2exbidv 1868 |
. . . . . . . 8
   
                    |
47 | 44, 46 | imbi12d 234 |
. . . . . . 7
   
       
         
               |
48 | 43, 47 | spcv 2831 |
. . . . . 6
                 
 
              |
49 | 41, 48 | mpi 15 |
. . . . 5
                          |
50 | | eqcom 2179 |
. . . . . . . . . 10
               |
51 | 19, 20, 4, 5 | opeqpr 4250 |
. . . . . . . . . 10
          
              |
52 | 50, 51 | bitri 184 |
. . . . . . . . 9
          
              |
53 | | idd 21 |
. . . . . . . . . 10
      
      
       |
54 | | eqtr2 2196 |
. . . . . . . . . . . . . 14
    
          |
55 | | vex 2740 |
. . . . . . . . . . . . . . . 16
 |
56 | 19, 20, 55 | preqsn 3773 |
. . . . . . . . . . . . . . 15
      
   |
57 | 56 | simplbi 274 |
. . . . . . . . . . . . . 14
        |
58 | 54, 57 | syl 14 |
. . . . . . . . . . . . 13
    
     |
59 | | dfsn2 3605 |
. . . . . . . . . . . . . . . . . . . 20
 
    |
60 | | preq2 3669 |
. . . . . . . . . . . . . . . . . . . 20
         |
61 | 59, 60 | eqtr2id 2223 |
. . . . . . . . . . . . . . . . . . 19
        |
62 | 61 | eqeq2d 2189 |
. . . . . . . . . . . . . . . . . 18
 
  
     |
63 | 59, 60 | eqtrid 2222 |
. . . . . . . . . . . . . . . . . . 19
  
     |
64 | 63 | eqeq2d 2189 |
. . . . . . . . . . . . . . . . . 18
 
        |
65 | 62, 64 | anbi12d 473 |
. . . . . . . . . . . . . . . . 17
        
  
       |
66 | 65 | biimpd 144 |
. . . . . . . . . . . . . . . 16
                   |
67 | 66 | expd 258 |
. . . . . . . . . . . . . . 15
 
        
        |
68 | 67 | com12 30 |
. . . . . . . . . . . . . 14
        
          |
69 | 68 | adantr 276 |
. . . . . . . . . . . . 13
    
       
          |
70 | 58, 69 | mpd 13 |
. . . . . . . . . . . 12
    
   
    
       |
71 | 70 | expcom 116 |
. . . . . . . . . . 11
                     |
72 | 71 | impd 254 |
. . . . . . . . . 10
             
       |
73 | 53, 72 | jaod 717 |
. . . . . . . . 9
       
           
  
       |
74 | 52, 73 | biimtrid 152 |
. . . . . . . 8
      
   
         |
75 | 74 | 2eximdv 1882 |
. . . . . . 7
          
  
      
       |
76 | 75 | exlimiv 1598 |
. . . . . 6
                             |
77 | 76 | imp 124 |
. . . . 5
               
      
      |
78 | 40, 49, 77 | syl2an 289 |
. . . 4
                   
  
           
      |
79 | 14, 78 | sylbi 121 |
. . 3
  
                |
80 | | simpr 110 |
. . . . . . . . . . 11
           |
81 | | equid 1701 |
. . . . . . . . . . . . . 14
 |
82 | 81 | jctl 314 |
. . . . . . . . . . . . 13
         |
83 | 19, 19, 4 | opeqsn 4249 |
. . . . . . . . . . . . 13
     

     |
84 | 82, 83 | sylibr 134 |
. . . . . . . . . . . 12
          |
85 | 84 | adantr 276 |
. . . . . . . . . . 11
         
    |
86 | 80, 85 | eqtr4d 2213 |
. . . . . . . . . 10
            |
87 | | opeq12 3778 |
. . . . . . . . . . . 12
 
         |
88 | 87 | eqeq2d 2189 |
. . . . . . . . . . 11
 
    
      |
89 | 19, 19, 88 | spc2ev 2833 |
. . . . . . . . . 10
            |
90 | 86, 89 | syl 14 |
. . . . . . . . 9
         
     |
91 | 90 | adantlr 477 |
. . . . . . . 8
                    |
92 | | preq12 3670 |
. . . . . . . . . . . 12
       
             |
93 | 92 | eqeq2d 2189 |
. . . . . . . . . . 11
       
               |
94 | 93 | biimpa 296 |
. . . . . . . . . 10
                       |
95 | 19, 20 | dfop 3775 |
. . . . . . . . . 10
            |
96 | 94, 95 | eqtr4di 2228 |
. . . . . . . . 9
                  |
97 | | opeq12 3778 |
. . . . . . . . . . 11
 
         |
98 | 97 | eqeq2d 2189 |
. . . . . . . . . 10
 
    
      |
99 | 19, 20, 98 | spc2ev 2833 |
. . . . . . . . 9
            |
100 | 96, 99 | syl 14 |
. . . . . . . 8
               
     |
101 | 91, 100 | jaodan 797 |
. . . . . . 7
           
       
     |
102 | 101 | ex 115 |
. . . . . 6
       
   
   
  
      |
103 | | elvv 4685 |
. . . . . 6
  
        |
104 | 102, 6, 103 | 3imtr4g 205 |
. . . . 5
       
         |
105 | 104 | ssrdv 3161 |
. . . 4
       
  
    |
106 | 105 | exlimivv 1896 |
. . 3
           
  
    |
107 | 79, 106 | impbii 126 |
. 2
  
                |
108 | 1, 107 | bitri 184 |
1
          
      |