Step | Hyp | Ref
| Expression |
1 | | xpassen.1 |
. . . 4
 |
2 | | xpassen.2 |
. . . 4
 |
3 | 1, 2 | xpex 6583 |
. . 3
   |
4 | | xpassen.3 |
. . 3
 |
5 | 3, 4 | xpex 6583 |
. 2
     |
6 | 2, 4 | xpex 6583 |
. . 3
   |
7 | 1, 6 | xpex 6583 |
. 2
     |
8 | | opex 4637 |
. . 3
                      |
9 | 8 | a1i 11 |
. 2
                            |
10 | | opex 4637 |
. . 3
              
       |
11 | 10 | a1i 11 |
. 2
  
                
        |
12 | | sneq 3946 |
. . . . . . . . . . . . . . . . 17
        
          |
13 | 12 | dmeqd 5015 |
. . . . . . . . . . . . . . . 16
                   |
14 | 13 | unieqd 4178 |
. . . . . . . . . . . . . . 15
                     |
15 | 14 | sneqd 3948 |
. . . . . . . . . . . . . 14
                         |
16 | 15 | dmeqd 5015 |
. . . . . . . . . . . . 13
           
             |
17 | 16 | unieqd 4178 |
. . . . . . . . . . . 12
            
              |
18 | | opex 4637 |
. . . . . . . . . . . . . . . . 17
  
 |
19 | | vex 3016 |
. . . . . . . . . . . . . . . . 17
 |
20 | 18, 19 | op1sta 5297 |
. . . . . . . . . . . . . . . 16
             |
21 | 20 | sneqi 3947 |
. . . . . . . . . . . . . . 15
                 |
22 | 21 | dmeqi 5014 |
. . . . . . . . . . . . . 14
          
      |
23 | 22 | unieqi 4177 |
. . . . . . . . . . . . 13
                   |
24 | | vex 3016 |
. . . . . . . . . . . . . 14
 |
25 | | vex 3016 |
. . . . . . . . . . . . . 14
 |
26 | 24, 25 | op1sta 5297 |
. . . . . . . . . . . . 13
       |
27 | 23, 26 | eqtri 2474 |
. . . . . . . . . . . 12
             |
28 | 17, 27 | syl6req 2503 |
. . . . . . . . . . 11
               |
29 | 15 | rneqd 5040 |
. . . . . . . . . . . . . 14
           
             |
30 | 29 | unieqd 4178 |
. . . . . . . . . . . . 13
            
              |
31 | 21 | rneqi 5039 |
. . . . . . . . . . . . . . 15
          
      |
32 | 31 | unieqi 4177 |
. . . . . . . . . . . . . 14
                   |
33 | 24, 25 | op2nda 5300 |
. . . . . . . . . . . . . 14
       |
34 | 32, 33 | eqtri 2474 |
. . . . . . . . . . . . 13
             |
35 | 30, 34 | syl6req 2503 |
. . . . . . . . . . . 12
               |
36 | 12 | rneqd 5040 |
. . . . . . . . . . . . . 14
                   |
37 | 36 | unieqd 4178 |
. . . . . . . . . . . . 13
                     |
38 | 18, 19 | op2nda 5300 |
. . . . . . . . . . . . 13
          |
39 | 37, 38 | syl6req 2503 |
. . . . . . . . . . . 12
            |
40 | 35, 39 | opeq12d 4144 |
. . . . . . . . . . 11
                        |
41 | 28, 40 | opeq12d 4144 |
. . . . . . . . . 10
                                    |
42 | | sneq 3946 |
. . . . . . . . . . . . . . 15
                   |
43 | 42 | dmeqd 5015 |
. . . . . . . . . . . . . 14
                   |
44 | 43 | unieqd 4178 |
. . . . . . . . . . . . 13
                     |
45 | | opex 4637 |
. . . . . . . . . . . . . 14
    |
46 | 24, 45 | op1sta 5297 |
. . . . . . . . . . . . 13
          |
47 | 44, 46 | syl6req 2503 |
. . . . . . . . . . . 12
            |
48 | 42 | rneqd 5040 |
. . . . . . . . . . . . . . . . 17
                   |
49 | 48 | unieqd 4178 |
. . . . . . . . . . . . . . . 16
                     |
50 | 49 | sneqd 3948 |
. . . . . . . . . . . . . . 15
                         |
51 | 50 | dmeqd 5015 |
. . . . . . . . . . . . . 14
                         |
52 | 51 | unieqd 4178 |
. . . . . . . . . . . . 13
                           |
53 | 24, 45 | op2nda 5300 |
. . . . . . . . . . . . . . . . 17
             |
54 | 53 | sneqi 3947 |
. . . . . . . . . . . . . . . 16
                 |
55 | 54 | dmeqi 5014 |
. . . . . . . . . . . . . . 15
                 |
56 | 55 | unieqi 4177 |
. . . . . . . . . . . . . 14
                   |
57 | 25, 19 | op1sta 5297 |
. . . . . . . . . . . . . 14
     
 |
58 | 56, 57 | eqtri 2474 |
. . . . . . . . . . . . 13
             |
59 | 52, 58 | syl6req 2503 |
. . . . . . . . . . . 12
               |
60 | 47, 59 | opeq12d 4144 |
. . . . . . . . . . 11
         
              |
61 | 50 | rneqd 5040 |
. . . . . . . . . . . . 13
                         |
62 | 61 | unieqd 4178 |
. . . . . . . . . . . 12
                           |
63 | 54 | rneqi 5039 |
. . . . . . . . . . . . . 14
                 |
64 | 63 | unieqi 4177 |
. . . . . . . . . . . . 13
                   |
65 | 25, 19 | op2nda 5300 |
. . . . . . . . . . . . 13
     
 |
66 | 64, 65 | eqtri 2474 |
. . . . . . . . . . . 12
             |
67 | 62, 66 | syl6req 2503 |
. . . . . . . . . . 11
               |
68 | 60, 67 | opeq12d 4144 |
. . . . . . . . . 10
                                    |
69 | 41, 68 | eq2tri 2513 |
. . . . . . . . 9
       
                     
                               |
70 | | anass 659 |
. . . . . . . . 9
  




    |
71 | 69, 70 | anbi12i 708 |
. . . . . . . 8
        
                       

 
       
                             |
72 | | an32 812 |
. . . . . . . 8
        
 

 
                             
                       

    |
73 | | an32 812 |
. . . . . . . 8
        


                                                              |
74 | 71, 72, 73 | 3bitr4i 285 |
. . . . . . 7
        
 

 
                             


                           |
75 | 74 | exbii 1722 |
. . . . . 6
            

 
                                 
  
              
         |
76 | | 19.41v 1834 |
. . . . . 6
            

 
                                 

 
                        |
77 | | 19.41v 1834 |
. . . . . 6
            
  
              
                


                           |
78 | 75, 76, 77 | 3bitr3i 283 |
. . . . 5
            

 
                                 
  
              
         |
79 | 78 | 2exbii 1723 |
. . . 4
                

 
                                     
  
              
         |
80 | | 19.41vv 1835 |
. . . 4
                

 
                                     

 
                        |
81 | | 19.41vv 1835 |
. . . 4
                
  
              
                    


                           |
82 | 79, 80, 81 | 3bitr3i 283 |
. . 3
                

 
                                     
  
              
         |
83 | | elxp 4829 |
. . . . 5
    
               |
84 | | excom 1931 |
. . . . 5
           
            
    |
85 | | elxp 4829 |
. . . . . . . . 9
  
        
    |
86 | 85 | anbi1i 706 |
. . . . . . . 8
    
    
            
       |
87 | | an12 811 |
. . . . . . . 8
       
    
        |
88 | | 19.41vv 1835 |
. . . . . . . 8
          
 
     
            
       |
89 | 86, 87, 88 | 3bitr4i 285 |
. . . . . . 7
       
           
          |
90 | 89 | 2exbii 1723 |
. . . . . 6
           
               
 
        |
91 | | exrot4 1936 |
. . . . . 6
             

 
     
                
       |
92 | | anass 659 |
. . . . . . . . 9
      
 
     
                |
93 | 92 | exbii 1722 |
. . . . . . . 8
           
    
       

         |
94 | | opeq1 4136 |
. . . . . . . . . . . 12
      
        |
95 | 94 | eqeq2d 2462 |
. . . . . . . . . . 11
                 |
96 | 95 | anbi1d 716 |
. . . . . . . . . 10
                     |
97 | 96 | anbi2d 715 |
. . . . . . . . 9
      
      
 
       
     |
98 | 18, 97 | ceqsexv 3052 |
. . . . . . . 8
                          
    |
99 | | an12 811 |
. . . . . . . 8
  

        
        

    |
100 | 93, 98, 99 | 3bitri 279 |
. . . . . . 7
           
    
        

    |
101 | 100 | 3exbii 1724 |
. . . . . 6
             

 
     
                    |
102 | 90, 91, 101 | 3bitri 279 |
. . . . 5
           
                

    |
103 | 83, 84, 102 | 3bitri 279 |
. . . 4
    
                    |
104 | 103 | anbi1i 706 |
. . 3
     
                                     

 
                        |
105 | | elxp 4829 |
. . . . 5
  
 
        
      |
106 | | elxp 4829 |
. . . . . . . . . 10
  
        
    |
107 | 106 | anbi2i 705 |
. . . . . . . . 9
         
    
               |
108 | | anass 659 |
. . . . . . . . 9
         
           |
109 | | 19.42vv 1840 |
. . . . . . . . . 10
               
  
    
               |
110 | | an12 811 |
. . . . . . . . . . . 12
           
  
         

     |
111 | | anass 659 |
. . . . . . . . . . . . 13
       
       
     |
112 | 111 | anbi2i 705 |
. . . . . . . . . . . 12
           
  
         
      |
113 | 110, 112 | bitri 257 |
. . . . . . . . . . 11
           
  
         
      |
114 | 113 | 2exbii 1723 |
. . . . . . . . . 10
               
  
             
      |
115 | 109, 114 | bitr3i 259 |
. . . . . . . . 9
                              
 
      |
116 | 107, 108,
115 | 3bitr3i 283 |
. . . . . . . 8
    

               
 
      |
117 | 116 | exbii 1722 |
. . . . . . 7
       
                   
      |
118 | | exrot3 1935 |
. . . . . . 7
                
                   
      |
119 | | opeq2 4137 |
. . . . . . . . . . 11
               |
120 | 119 | eqeq2d 2462 |
. . . . . . . . . 10
                 |
121 | 120 | anbi1d 716 |
. . . . . . . . 9
                    


      |
122 | 45, 121 | ceqsexv 3052 |
. . . . . . . 8
            
          


     |
123 | 122 | 2exbii 1723 |
. . . . . . 7
                
              


     |
124 | 117, 118,
123 | 3bitri 279 |
. . . . . 6
       
              


     |
125 | 124 | exbii 1722 |
. . . . 5
        

                  
     |
126 | 105, 125 | bitri 257 |
. . . 4
  
 
            


     |
127 | 126 | anbi1i 706 |
. . 3
     
              
                    


                           |
128 | 82, 104, 127 | 3bitr4i 285 |
. 2
     
                          
              
         |
129 | 5, 7, 9, 11, 128 | en2i 7594 |
1
    
    |