Step | Hyp | Ref
| Expression |
1 | | df-rel 4295 |
. 2
     
     |
2 | | dfss2 2928 |
. . . . 5
        
  
     |
3 | | vex 2554 |
. . . . . . . . . 10
 |
4 | | relop.1 |
. . . . . . . . . 10
 |
5 | | relop.2 |
. . . . . . . . . 10
 |
6 | 3, 4, 5 | elop 3959 |
. . . . . . . . 9
      
      |
7 | | elvv 4345 |
. . . . . . . . 9
  
  
     |
8 | 6, 7 | imbi12i 228 |
. . . . . . . 8
    
      
             |
9 | | jaob 630 |
. . . . . . . 8
    
   
  
              

             |
10 | 8, 9 | bitri 173 |
. . . . . . 7
    
             

             |
11 | 10 | albii 1356 |
. . . . . 6
         
     
  
      
   
       |
12 | | 19.26 1367 |
. . . . . 6
             

              
 
  
         
  
       |
13 | 11, 12 | bitri 173 |
. . . . 5
         
     
  
         
  
       |
14 | 2, 13 | bitri 173 |
. . . 4
           
  
         
  
       |
15 | | snexgOLD 3926 |
. . . . . . . 8
  
  |
16 | 4, 15 | ax-mp 7 |
. . . . . . 7
 
 |
17 | | eqeq1 2043 |
. . . . . . . 8
     
 
     |
18 | | eqeq1 2043 |
. . . . . . . . . 10
        
      |
19 | | eqcom 2039 |
. . . . . . . . . . 11
  
     
    |
20 | | vex 2554 |
. . . . . . . . . . . 12
 |
21 | | vex 2554 |
. . . . . . . . . . . 12
 |
22 | 20, 21, 4 | opeqsn 3980 |
. . . . . . . . . . 11
     

     |
23 | 19, 22 | bitri 173 |
. . . . . . . . . 10
  
         |
24 | 18, 23 | syl6bb 185 |
. . . . . . . . 9
              |
25 | 24 | 2exbidv 1745 |
. . . . . . . 8
      
              |
26 | 17, 25 | imbi12d 223 |
. . . . . . 7
             
  
 
            |
27 | 16, 26 | spcv 2640 |
. . . . . 6
     
  
             
      |
28 | | sneq 3378 |
. . . . . . . . 9
  
    |
29 | 28 | eqeq2d 2048 |
. . . . . . . 8
 
       |
30 | 29 | cbvexv 1792 |
. . . . . . 7
 
 

    |
31 | | a9ev 1584 |
. . . . . . . . . 10

 |
32 | | equcom 1590 |
. . . . . . . . . . 11
   |
33 | 32 | exbii 1493 |
. . . . . . . . . 10
 

  |
34 | 31, 33 | mpbi 133 |
. . . . . . . . 9

 |
35 | | 19.41v 1779 |
. . . . . . . . 9
      
 
     |
36 | 34, 35 | mpbiran 846 |
. . . . . . . 8
      
    |
37 | 36 | exbii 1493 |
. . . . . . 7
              |
38 | | eqid 2037 |
. . . . . . . 8
 
   |
39 | 38 | a1bi 232 |
. . . . . . 7
                  
      |
40 | 30, 37, 39 | 3bitr2ri 198 |
. . . . . 6
                    |
41 | 27, 40 | sylib 127 |
. . . . 5
     
  
         |
42 | | eqid 2037 |
. . . . . 6
    
  |
43 | | prexgOLD 3937 |
. . . . . . . 8
 
   
  |
44 | 4, 5, 43 | mp2an 402 |
. . . . . . 7
    |
45 | | eqeq1 2043 |
. . . . . . . 8
   

       
    |
46 | | eqeq1 2043 |
. . . . . . . . 9
   

     
      |
47 | 46 | 2exbidv 1745 |
. . . . . . . 8
   
                    |
48 | 45, 47 | imbi12d 223 |
. . . . . . 7
   
 
 
   
      
          
       |
49 | 44, 48 | spcv 2640 |
. . . . . 6
     
   
                 
      |
50 | 42, 49 | mpi 15 |
. . . . 5
     
   
                |
51 | | eqcom 2039 |
. . . . . . . . . 10
  
            |
52 | 20, 21, 4, 5 | opeqpr 3981 |
. . . . . . . . . 10
     
    
              |
53 | 51, 52 | bitri 173 |
. . . . . . . . 9
  
            
         |
54 | | idd 21 |
. . . . . . . . . 10
           
   
     |
55 | | eqtr2 2055 |
. . . . . . . . . . . . . 14
               |
56 | | vex 2554 |
. . . . . . . . . . . . . . . 16
 |
57 | 20, 21, 56 | preqsn 3537 |
. . . . . . . . . . . . . . 15
  
       |
58 | 57 | simplbi 259 |
. . . . . . . . . . . . . 14
  
     |
59 | 55, 58 | syl 14 |
. . . . . . . . . . . . 13
          |
60 | | dfsn2 3381 |
. . . . . . . . . . . . . . . . . . . 20
 
    |
61 | | preq2 3439 |
. . . . . . . . . . . . . . . . . . . 20
  
      |
62 | 60, 61 | syl5req 2082 |
. . . . . . . . . . . . . . . . . . 19
  
     |
63 | 62 | eqeq2d 2048 |
. . . . . . . . . . . . . . . . . 18
 
        |
64 | 60, 61 | syl5eq 2081 |
. . . . . . . . . . . . . . . . . . 19
  
 
   |
65 | 64 | eqeq2d 2048 |
. . . . . . . . . . . . . . . . . 18
 
        |
66 | 63, 65 | anbi12d 442 |
. . . . . . . . . . . . . . . . 17
  
 
   
  
       |
67 | 66 | biimpd 132 |
. . . . . . . . . . . . . . . 16
  
 
   

   
     |
68 | 67 | expd 245 |
. . . . . . . . . . . . . . 15
 
   
             |
69 | 68 | com12 27 |
. . . . . . . . . . . . . 14
   


 

   
      |
70 | 69 | adantr 261 |
. . . . . . . . . . . . 13
           

   
      |
71 | 59, 70 | mpd 13 |
. . . . . . . . . . . 12
          

   
     |
72 | 71 | expcom 109 |
. . . . . . . . . . 11
     
   

   
      |
73 | 72 | impd 242 |
. . . . . . . . . 10
          

   
     |
74 | 54, 73 | jaod 636 |
. . . . . . . . 9
              
     
 
       |
75 | 53, 74 | syl5bi 141 |
. . . . . . . 8
      
   
   
     |
76 | 75 | 2eximdv 1759 |
. . . . . . 7
          
  
              |
77 | 76 | exlimiv 1486 |
. . . . . 6
 
 
      
          
       |
78 | 77 | imp 115 |
. . . . 5
  
                 
 
      |
79 | 41, 50, 78 | syl2an 273 |
. . . 4
             
  
 
   
             
    |
80 | 14, 79 | sylbi 114 |
. . 3
              
    |
81 | | simpr 103 |
. . . . . . . . . . 11
           |
82 | | equid 1586 |
. . . . . . . . . . . . . 14
 |
83 | 82 | jctl 297 |
. . . . . . . . . . . . 13
         |
84 | 20, 20, 4 | opeqsn 3980 |
. . . . . . . . . . . . 13
     

     |
85 | 83, 84 | sylibr 137 |
. . . . . . . . . . . 12
          |
86 | 85 | adantr 261 |
. . . . . . . . . . 11
              |
87 | 81, 86 | eqtr4d 2072 |
. . . . . . . . . 10
            |
88 | | opeq12 3542 |
. . . . . . . . . . . 12
 
   
     |
89 | 88 | eqeq2d 2048 |
. . . . . . . . . . 11
 
           |
90 | 20, 20, 89 | spc2ev 2642 |
. . . . . . . . . 10
      
     |
91 | 87, 90 | syl 14 |
. . . . . . . . 9
               |
92 | 91 | adantlr 446 |
. . . . . . . 8
    
               |
93 | | preq12 3440 |
. . . . . . . . . . . 12
     
    
     
    |
94 | 93 | eqeq2d 2048 |
. . . . . . . . . . 11
     
                 |
95 | 94 | biimpa 280 |
. . . . . . . . . 10
    
     
       
    |
96 | 20, 21 | dfop 3539 |
. . . . . . . . . 10
  
     
   |
97 | 95, 96 | syl6eqr 2087 |
. . . . . . . . 9
    
     
       |
98 | | opeq12 3542 |
. . . . . . . . . . 11
 
   
     |
99 | 98 | eqeq2d 2048 |
. . . . . . . . . 10
 
           |
100 | 20, 21, 99 | spc2ev 2642 |
. . . . . . . . 9
      
     |
101 | 97, 100 | syl 14 |
. . . . . . . 8
    
     
    
     |
102 | 92, 101 | jaodan 709 |
. . . . . . 7
    
      
       
     |
103 | 102 | ex 108 |
. . . . . 6
     
     
 
    
      |
104 | | elvv 4345 |
. . . . . 6
  
  
     |
105 | 103, 6, 104 | 3imtr4g 194 |
. . . . 5
     
     
     |
106 | 105 | ssrdv 2945 |
. . . 4
     
         |
107 | 106 | exlimivv 1773 |
. . 3
                   |
108 | 80, 107 | impbii 117 |
. 2
                   |
109 | 1, 108 | bitri 173 |
1
            
    |