Step | Hyp | Ref
| Expression |
1 | | df-rel 4841 |
. 2
           |
2 | | dfss2 3421 |
. . . . 5
  
              |
3 | | relop.1 |
. . . . . . . . . 10
 |
4 | | relop.2 |
. . . . . . . . . 10
 |
5 | 3, 4 | elop 4667 |
. . . . . . . . 9
      
      |
6 | | elvv 4893 |
. . . . . . . . 9
  
        |
7 | 5, 6 | imbi12i 328 |
. . . . . . . 8
    

     
 
 
  
      |
8 | | jaob 792 |
. . . . . . . 8
    
      
                 
           |
9 | 7, 8 | bitri 253 |
. . . . . . 7
    

               
           |
10 | 9 | albii 1691 |
. . . . . 6
         
            
      
       |
11 | | 19.26 1732 |
. . . . . 6
                
              
  
   
    
           |
12 | 10, 11 | bitri 253 |
. . . . 5
         
            
    
           |
13 | 2, 12 | bitri 253 |
. . . 4
  
                     
  
       |
14 | | snex 4641 |
. . . . . . 7
 
 |
15 | | eqeq1 2455 |
. . . . . . . 8
     
       |
16 | | eqeq1 2455 |
. . . . . . . . . 10
      
 
      |
17 | | eqcom 2458 |
. . . . . . . . . . 11
     
  
    |
18 | | vex 3048 |
. . . . . . . . . . . 12
 |
19 | | vex 3048 |
. . . . . . . . . . . 12
 |
20 | 18, 19, 3 | opeqsn 4697 |
. . . . . . . . . . 11
     

     |
21 | 17, 20 | bitri 253 |
. . . . . . . . . 10
     

     |
22 | 16, 21 | syl6bb 265 |
. . . . . . . . 9
      

      |
23 | 22 | 2exbidv 1770 |
. . . . . . . 8
      
  
           |
24 | 15, 23 | imbi12d 322 |
. . . . . . 7
             
  
              |
25 | 14, 24 | spcv 3140 |
. . . . . 6
            
    
           |
26 | | sneq 3978 |
. . . . . . . . 9
  
    |
27 | 26 | eqeq2d 2461 |
. . . . . . . 8
 
       |
28 | 27 | cbvexv 2117 |
. . . . . . 7
   

    |
29 | | ax6evr 1859 |
. . . . . . . . 9

 |
30 | | 19.41v 1830 |
. . . . . . . . 9
              |
31 | 29, 30 | mpbiran 929 |
. . . . . . . 8
           |
32 | 31 | exbii 1718 |
. . . . . . 7
     
  

    |
33 | | eqid 2451 |
. . . . . . . 8
 
   |
34 | 33 | a1bi 339 |
. . . . . . 7
     
  
  
 
           |
35 | 28, 32, 34 | 3bitr2ri 278 |
. . . . . 6
                    |
36 | 25, 35 | sylib 200 |
. . . . 5
            

    |
37 | | eqid 2451 |
. . . . . 6
    
  |
38 | | prex 4642 |
. . . . . . 7
    |
39 | | eqeq1 2455 |
. . . . . . . 8
   
   
  
      |
40 | | eqeq1 2455 |
. . . . . . . . 9
   
      
      |
41 | 40 | 2exbidv 1770 |
. . . . . . . 8
   
                    |
42 | 39, 41 | imbi12d 322 |
. . . . . . 7
   
       
         
               |
43 | 38, 42 | spcv 3140 |
. . . . . 6
                 
 
              |
44 | 37, 43 | mpi 20 |
. . . . 5
                          |
45 | | eqcom 2458 |
. . . . . . . . . 10
               |
46 | 18, 19, 3, 4 | opeqpr 4698 |
. . . . . . . . . 10
          
              |
47 | 45, 46 | bitri 253 |
. . . . . . . . 9
          
              |
48 | | idd 25 |
. . . . . . . . . 10
      
      
       |
49 | | eqtr2 2471 |
. . . . . . . . . . . . . 14
    
          |
50 | | vex 3048 |
. . . . . . . . . . . . . . . 16
 |
51 | 18, 19, 50 | preqsn 4159 |
. . . . . . . . . . . . . . 15
      
   |
52 | 51 | simplbi 462 |
. . . . . . . . . . . . . 14
        |
53 | 49, 52 | syl 17 |
. . . . . . . . . . . . 13
    
     |
54 | | dfsn2 3981 |
. . . . . . . . . . . . . . . . . . . 20
 
    |
55 | | preq2 4052 |
. . . . . . . . . . . . . . . . . . . 20
         |
56 | 54, 55 | syl5req 2498 |
. . . . . . . . . . . . . . . . . . 19
        |
57 | 56 | eqeq2d 2461 |
. . . . . . . . . . . . . . . . . 18
 
  
     |
58 | 54, 55 | syl5eq 2497 |
. . . . . . . . . . . . . . . . . . 19
  
     |
59 | 58 | eqeq2d 2461 |
. . . . . . . . . . . . . . . . . 18
 
        |
60 | 57, 59 | anbi12d 717 |
. . . . . . . . . . . . . . . . 17
        
  
       |
61 | 60 | biimpd 211 |
. . . . . . . . . . . . . . . 16
                   |
62 | 61 | expd 438 |
. . . . . . . . . . . . . . 15
 
        
        |
63 | 62 | com12 32 |
. . . . . . . . . . . . . 14
        
          |
64 | 63 | adantr 467 |
. . . . . . . . . . . . 13
    
       
          |
65 | 53, 64 | mpd 15 |
. . . . . . . . . . . 12
    
   
    
       |
66 | 65 | expcom 437 |
. . . . . . . . . . 11
                     |
67 | 66 | impd 433 |
. . . . . . . . . 10
             
       |
68 | 48, 67 | jaod 382 |
. . . . . . . . 9
       
           
  
       |
69 | 47, 68 | syl5bi 221 |
. . . . . . . 8
      
   
         |
70 | 69 | 2eximdv 1766 |
. . . . . . 7
          
  
      
       |
71 | 70 | exlimiv 1776 |
. . . . . 6
                             |
72 | 71 | imp 431 |
. . . . 5
               
      
      |
73 | 36, 44, 72 | syl2an 480 |
. . . 4
                   
  
           
      |
74 | 13, 73 | sylbi 199 |
. . 3
  
                |
75 | | simpr 463 |
. . . . . . . . . . 11
           |
76 | | equid 1855 |
. . . . . . . . . . . . . 14
 |
77 | 76 | jctl 544 |
. . . . . . . . . . . . 13
         |
78 | 18, 18, 3 | opeqsn 4697 |
. . . . . . . . . . . . 13
     

     |
79 | 77, 78 | sylibr 216 |
. . . . . . . . . . . 12
          |
80 | 79 | adantr 467 |
. . . . . . . . . . 11
         
    |
81 | 75, 80 | eqtr4d 2488 |
. . . . . . . . . 10
            |
82 | | opeq12 4168 |
. . . . . . . . . . . 12
 
         |
83 | 82 | eqeq2d 2461 |
. . . . . . . . . . 11
 
    
      |
84 | 18, 18, 83 | spc2ev 3142 |
. . . . . . . . . 10
            |
85 | 81, 84 | syl 17 |
. . . . . . . . 9
         
     |
86 | 85 | adantlr 721 |
. . . . . . . 8
                    |
87 | | preq12 4053 |
. . . . . . . . . . . 12
       
             |
88 | 87 | eqeq2d 2461 |
. . . . . . . . . . 11
       
               |
89 | 88 | biimpa 487 |
. . . . . . . . . 10
                       |
90 | 18, 19 | dfop 4165 |
. . . . . . . . . 10
            |
91 | 89, 90 | syl6eqr 2503 |
. . . . . . . . 9
                  |
92 | | opeq12 4168 |
. . . . . . . . . . 11
 
         |
93 | 92 | eqeq2d 2461 |
. . . . . . . . . 10
 
    
      |
94 | 18, 19, 93 | spc2ev 3142 |
. . . . . . . . 9
            |
95 | 91, 94 | syl 17 |
. . . . . . . 8
               
     |
96 | 86, 95 | jaodan 794 |
. . . . . . 7
           
       
     |
97 | 96 | ex 436 |
. . . . . 6
       
   
   
  
      |
98 | | elvv 4893 |
. . . . . 6
  
        |
99 | 97, 5, 98 | 3imtr4g 274 |
. . . . 5
       
         |
100 | 99 | ssrdv 3438 |
. . . 4
       
  
    |
101 | 100 | exlimivv 1778 |
. . 3
           
  
    |
102 | 74, 101 | impbii 191 |
. 2
  
                |
103 | 1, 102 | bitri 253 |
1
          
      |