Step | Hyp | Ref
| Expression |
1 | | xpassen.1 |
. . . 4
 |
2 | | xpassen.2 |
. . . 4
 |
3 | 1, 2 | xpex 4396 |
. . 3
   |
4 | | xpassen.3 |
. . 3
 |
5 | 3, 4 | xpex 4396 |
. 2
     |
6 | 2, 4 | xpex 4396 |
. . 3
   |
7 | 1, 6 | xpex 4396 |
. 2
     |
8 | | vex 2554 |
. . . . . . . . . 10
 |
9 | 8 | snex 3928 |
. . . . . . . . 9
 
 |
10 | 9 | dmex 4541 |
. . . . . . . 8
 
 |
11 | 10 | uniex 4140 |
. . . . . . 7
    |
12 | 11 | snex 3928 |
. . . . . 6
      |
13 | 12 | dmex 4541 |
. . . . 5
    
 |
14 | 13 | uniex 4140 |
. . . 4
     
 |
15 | 12 | rnex 4542 |
. . . . . 6
    
 |
16 | 15 | uniex 4140 |
. . . . 5
     
 |
17 | 9 | rnex 4542 |
. . . . . 6
 
 |
18 | 17 | uniex 4140 |
. . . . 5
    |
19 | 16, 18 | opex 3957 |
. . . 4
             |
20 | 14, 19 | opex 3957 |
. . 3
                      |
21 | 20 | a1i 9 |
. 2
    
                       |
22 | | vex 2554 |
. . . . . . . 8
 |
23 | 22 | snex 3928 |
. . . . . . 7
   |
24 | 23 | dmex 4541 |
. . . . . 6
 
 |
25 | 24 | uniex 4140 |
. . . . 5
    |
26 | 23 | rnex 4542 |
. . . . . . . . 9
 
 |
27 | 26 | uniex 4140 |
. . . . . . . 8
    |
28 | 27 | snex 3928 |
. . . . . . 7
      |
29 | 28 | dmex 4541 |
. . . . . 6
    
 |
30 | 29 | uniex 4140 |
. . . . 5
       |
31 | 25, 30 | opex 3957 |
. . . 4
             |
32 | 28 | rnex 4542 |
. . . . 5
    
 |
33 | 32 | uniex 4140 |
. . . 4
       |
34 | 31, 33 | opex 3957 |
. . 3
                      |
35 | 34 | a1i 9 |
. 2
  
 
                       |
36 | | sneq 3378 |
. . . . . . . . . . . . . . . . 17
        
          |
37 | 36 | dmeqd 4480 |
. . . . . . . . . . . . . . . 16
                   |
38 | 37 | unieqd 3582 |
. . . . . . . . . . . . . . 15
                     |
39 | 38 | sneqd 3380 |
. . . . . . . . . . . . . 14
           
             |
40 | 39 | dmeqd 4480 |
. . . . . . . . . . . . 13
           
     
       |
41 | 40 | unieqd 3582 |
. . . . . . . . . . . 12
                           |
42 | | vex 2554 |
. . . . . . . . . . . . . . . . . 18
 |
43 | | vex 2554 |
. . . . . . . . . . . . . . . . . 18
 |
44 | 42, 43 | opex 3957 |
. . . . . . . . . . . . . . . . 17
  
 |
45 | | vex 2554 |
. . . . . . . . . . . . . . . . 17
 |
46 | 44, 45 | op1sta 4745 |
. . . . . . . . . . . . . . . 16
             |
47 | 46 | sneqi 3379 |
. . . . . . . . . . . . . . 15
                 |
48 | 47 | dmeqi 4479 |
. . . . . . . . . . . . . 14
                 |
49 | 48 | unieqi 3581 |
. . . . . . . . . . . . 13
      
            |
50 | 42, 43 | op1sta 4745 |
. . . . . . . . . . . . 13
       |
51 | 49, 50 | eqtri 2057 |
. . . . . . . . . . . 12
      
      |
52 | 41, 51 | syl6req 2086 |
. . . . . . . . . . 11
               |
53 | 39 | rneqd 4506 |
. . . . . . . . . . . . . 14
           
     
       |
54 | 53 | unieqd 3582 |
. . . . . . . . . . . . 13
                           |
55 | 47 | rneqi 4505 |
. . . . . . . . . . . . . . 15
                 |
56 | 55 | unieqi 3581 |
. . . . . . . . . . . . . 14
      
            |
57 | 42, 43 | op2nda 4748 |
. . . . . . . . . . . . . 14
       |
58 | 56, 57 | eqtri 2057 |
. . . . . . . . . . . . 13
      
      |
59 | 54, 58 | syl6req 2086 |
. . . . . . . . . . . 12
               |
60 | 36 | rneqd 4506 |
. . . . . . . . . . . . . 14
                   |
61 | 60 | unieqd 3582 |
. . . . . . . . . . . . 13
                     |
62 | 44, 45 | op2nda 4748 |
. . . . . . . . . . . . 13
          |
63 | 61, 62 | syl6req 2086 |
. . . . . . . . . . . 12
            |
64 | 59, 63 | opeq12d 3548 |
. . . . . . . . . . 11
                        |
65 | 52, 64 | opeq12d 3548 |
. . . . . . . . . 10
                                    |
66 | | sneq 3378 |
. . . . . . . . . . . . . . 15
        
          |
67 | 66 | dmeqd 4480 |
. . . . . . . . . . . . . 14
                   |
68 | 67 | unieqd 3582 |
. . . . . . . . . . . . 13
                     |
69 | 43, 45 | opex 3957 |
. . . . . . . . . . . . . 14
  
 |
70 | 42, 69 | op1sta 4745 |
. . . . . . . . . . . . 13
          |
71 | 68, 70 | syl6req 2086 |
. . . . . . . . . . . 12
            |
72 | 66 | rneqd 4506 |
. . . . . . . . . . . . . . . . 17
                   |
73 | 72 | unieqd 3582 |
. . . . . . . . . . . . . . . 16
                     |
74 | 73 | sneqd 3380 |
. . . . . . . . . . . . . . 15
           
             |
75 | 74 | dmeqd 4480 |
. . . . . . . . . . . . . 14
                         |
76 | 75 | unieqd 3582 |
. . . . . . . . . . . . 13
                           |
77 | 42, 69 | op2nda 4748 |
. . . . . . . . . . . . . . . . 17
             |
78 | 77 | sneqi 3379 |
. . . . . . . . . . . . . . . 16
                 |
79 | 78 | dmeqi 4479 |
. . . . . . . . . . . . . . 15
                 |
80 | 79 | unieqi 3581 |
. . . . . . . . . . . . . 14
                   |
81 | 43, 45 | op1sta 4745 |
. . . . . . . . . . . . . 14
       |
82 | 80, 81 | eqtri 2057 |
. . . . . . . . . . . . 13
             |
83 | 76, 82 | syl6req 2086 |
. . . . . . . . . . . 12
               |
84 | 71, 83 | opeq12d 3548 |
. . . . . . . . . . 11
                        |
85 | 74 | rneqd 4506 |
. . . . . . . . . . . . 13
                         |
86 | 85 | unieqd 3582 |
. . . . . . . . . . . 12
                           |
87 | 78 | rneqi 4505 |
. . . . . . . . . . . . . 14
                 |
88 | 87 | unieqi 3581 |
. . . . . . . . . . . . 13
                   |
89 | 43, 45 | op2nda 4748 |
. . . . . . . . . . . . 13
       |
90 | 88, 89 | eqtri 2057 |
. . . . . . . . . . . 12
             |
91 | 86, 90 | syl6req 2086 |
. . . . . . . . . . 11
               |
92 | 84, 91 | opeq12d 3548 |
. . . . . . . . . 10
         
  
                       |
93 | 65, 92 | eq2tri 2096 |
. . . . . . . . 9
                              
     
                        |
94 | | anass 381 |
. . . . . . . . 9
  
   
    |
95 | 93, 94 | anbi12i 433 |
. . . . . . . 8
     
  
                       
  
 
     
                      

     |
96 | | an32 496 |
. . . . . . . 8
     
  
 
  
                                                           |
97 | | an32 496 |
. . . . . . . 8
        
    
                             
                       
     |
98 | 95, 96, 97 | 3bitr4i 201 |
. . . . . . 7
     
  
 
  
                             
    
                        |
99 | 98 | exbii 1493 |
. . . . . 6
            
  
                               
    
                        |
100 | | 19.41v 1779 |
. . . . . 6
            
  
                            
  
 
  
                        |
101 | | 19.41v 1779 |
. . . . . 6
          
    
                               
    
                        |
102 | 99, 100, 101 | 3bitr3i 199 |
. . . . 5
            
  
                               
    
                        |
103 | 102 | 2exbii 1494 |
. . . 4
           
  
 
  
                             
     
    
                        |
104 | | 19.41vv 1780 |
. . . 4
           
  
 
  
                             
  
  
 
  
                        |
105 | | 19.41vv 1780 |
. . . 4
              
    
                             
     
    
                        |
106 | 103, 104,
105 | 3bitr3i 199 |
. . 3
           
  
 
  
                             
     
    
                        |
107 | | elxp 4305 |
. . . . 5
    
          
    |
108 | | excom 1551 |
. . . . 5
             
          
    |
109 | | elxp 4305 |
. . . . . . . . 9
  
        
    |
110 | 109 | anbi1i 431 |
. . . . . . . 8
    
                 
       |
111 | | an12 495 |
. . . . . . . 8
    

      

  
    |
112 | | 19.41vv 1780 |
. . . . . . . 8
         

                 
 

  
    |
113 | 110, 111,
112 | 3bitr4i 201 |
. . . . . . 7
    

                
       |
114 | 113 | 2exbii 1494 |
. . . . . 6
             
             
 

  
    |
115 | | exrot4 1578 |
. . . . . 6
                 
                  
 

  
    |
116 | | anass 381 |
. . . . . . . . 9
      
               
  
     |
117 | 116 | exbii 1493 |
. . . . . . . 8
        
 

  
    
    
          |
118 | | opeq1 3540 |
. . . . . . . . . . . 12
      
        |
119 | 118 | eqeq2d 2048 |
. . . . . . . . . . 11
                 |
120 | 119 | anbi1d 438 |
. . . . . . . . . 10
             
  
    |
121 | 120 | anbi2d 437 |
. . . . . . . . 9
      
        
    
  
     |
122 | 44, 121 | ceqsexv 2587 |
. . . . . . . 8
        
         
    
  
    |
123 | | an12 495 |
. . . . . . . 8
  
                  
     |
124 | 117, 122,
123 | 3bitri 195 |
. . . . . . 7
        
 

  
          
     |
125 | 124 | 3exbii 1495 |
. . . . . 6
                 
                         |
126 | 114, 115,
125 | 3bitri 195 |
. . . . 5
             
                    |
127 | 107, 108,
126 | 3bitri 195 |
. . . 4
    
                    |
128 | 127 | anbi1i 431 |
. . 3
     
                                     
  
                        |
129 | | elxp 4305 |
. . . . 5
  
 
        
      |
130 | | elxp 4305 |
. . . . . . . . . 10
  
        
    |
131 | 130 | anbi2i 430 |
. . . . . . . . 9
         
 
  
               |
132 | | anass 381 |
. . . . . . . . 9
         
           |
133 | | 19.42vv 1785 |
. . . . . . . . . 10
         
 
  
              
   
     |
134 | | an12 495 |
. . . . . . . . . . . 12
       
  
         
    
     |
135 | | anass 381 |
. . . . . . . . . . . . 13
       
      

     |
136 | 135 | anbi2i 430 |
. . . . . . . . . . . 12
    
 
    
  
         
      |
137 | 134, 136 | bitri 173 |
. . . . . . . . . . 11
       
  
        
  


      |
138 | 137 | 2exbii 1494 |
. . . . . . . . . 10
         
 
  
        
   
  


      |
139 | 133, 138 | bitr3i 175 |
. . . . . . . . 9
                       
   
  


      |
140 | 131, 132,
139 | 3bitr3i 199 |
. . . . . . . 8
    

        
   
  


      |
141 | 140 | exbii 1493 |
. . . . . . 7
       
                  

      |
142 | | exrot3 1577 |
. . . . . . 7
       
   
  


             

  


      |
143 | | opeq2 3541 |
. . . . . . . . . . 11
               |
144 | 143 | eqeq2d 2048 |
. . . . . . . . . 10
                 |
145 | 144 | anbi1d 438 |
. . . . . . . . 9
                    
        |
146 | 69, 145 | ceqsexv 2587 |
. . . . . . . 8
       
  


           

     |
147 | 146 | 2exbii 1494 |
. . . . . . 7
       
   
  


              
       |
148 | 141, 142,
147 | 3bitri 195 |
. . . . . 6
       
        
     
       |
149 | 148 | exbii 1493 |
. . . . 5
                          
       |
150 | 129, 149 | bitri 173 |
. . . 4
  
 
            
       |
151 | 150 | anbi1i 431 |
. . 3
     
                                   
    
                        |
152 | 106, 128,
151 | 3bitr4i 201 |
. 2
     
                      
   
                        |
153 | 5, 7, 21, 35, 152 | en2i 6186 |
1
    
    |