Step | Hyp | Ref
| Expression |
1 | | xpeq1 4853 |
. . . . 5
       |
2 | 1 | pweqd 3947 |
. . . 4
         |
3 | | pweq 3945 |
. . . . . 6
 
   |
4 | 3 | raleqdv 2979 |
. . . . 5
  
    
         |
5 | | f1eq2 5788 |
. . . . . 6
             |
6 | 5 | rexbidv 2892 |
. . . . 5
  
              |
7 | 4, 6 | imbi12d 327 |
. . . 4
               
 
               |
8 | 2, 7 | raleqbidv 2987 |
. . 3
  
                
     
               |
9 | 8 | imbi2d 323 |
. 2
                     

     
                |
10 | | xpeq1 4853 |
. . . . 5
       |
11 | 10 | pweqd 3947 |
. . . 4
         |
12 | | pweq 3945 |
. . . . . 6
 
   |
13 | 12 | raleqdv 2979 |
. . . . 5
  
    
         |
14 | | f1eq2 5788 |
. . . . . 6
             |
15 | 14 | rexbidv 2892 |
. . . . 5
  
              |
16 | 13, 15 | imbi12d 327 |
. . . 4
               
 
               |
17 | 11, 16 | raleqbidv 2987 |
. . 3
  
                
     
               |
18 | 17 | imbi2d 323 |
. 2
                     

     
                |
19 | | bi2.04 368 |
. . . . 5
 
                                             |
20 | 19 | albii 1699 |
. . . 4
                                                   |
21 | | 19.21v 1794 |
. . . 4
                                  
                |
22 | 20, 21 | bitri 257 |
. . 3
                                  
                |
23 | | 0elpw 4570 |
. . . . . . . . . . . . 13
  |
24 | | f10 5859 |
. . . . . . . . . . . . 13
     |
25 | | f1eq1 5787 |
. . . . . . . . . . . . . 14

    
       |
26 | 25 | rspcev 3136 |
. . . . . . . . . . . . 13
 
              |
27 | 23, 24, 26 | mp2an 686 |
. . . . . . . . . . . 12
       |
28 | | f1eq2 5788 |
. . . . . . . . . . . . 13

    
       |
29 | 28 | rexbidv 2892 |
. . . . . . . . . . . 12

                |
30 | 27, 29 | mpbiri 241 |
. . . . . . . . . . 11

        |
31 | 30 | a1i 11 |
. . . . . . . . . 10
                                 
          
                 |
32 | | n0 3732 |
. . . . . . . . . . 11
    |
33 | | snelpwi 4645 |
. . . . . . . . . . . . . . . . . . 19
      |
34 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
35 | | imaeq2 5170 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
36 | 34, 35 | breq12d 4408 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
37 | 36 | rspcva 3134 |
. . . . . . . . . . . . . . . . . . . . 21
    
      
          |
38 | | vex 3034 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
39 | 38 | snnz 4081 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
40 | | snex 4641 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
41 | 40 | 0sdom 7721 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
    |
42 | 39, 41 | mpbir 214 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
43 | | sdomdomtr 7723 |
. . . . . . . . . . . . . . . . . . . . . . 23
            
        |
44 | 42, 43 | mpan 684 |
. . . . . . . . . . . . . . . . . . . . . 22
        
        |
45 | | vex 3034 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
46 | | imaexg 6749 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         |
47 | 45, 46 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
48 | 47 | 0sdom 7721 |
. . . . . . . . . . . . . . . . . . . . . 22
      
        |
49 | 44, 48 | sylib 201 |
. . . . . . . . . . . . . . . . . . . . 21
        
        |
50 | 37, 49 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
    
      
        |
51 | 50 | expcom 442 |
. . . . . . . . . . . . . . . . . . 19
 
        
         |
52 | 33, 51 | syl5 32 |
. . . . . . . . . . . . . . . . . 18
 
               |
53 | 52 | adantl 473 |
. . . . . . . . . . . . . . . . 17
           

         |
54 | 53 | ad2antlr 741 |
. . . . . . . . . . . . . . . 16
                                 
          
       
         |
55 | 54 | impr 631 |
. . . . . . . . . . . . . . 15
                                 
                 
 
        |
56 | | n0 3732 |
. . . . . . . . . . . . . . 15
      
         |
57 | 55, 56 | sylib 201 |
. . . . . . . . . . . . . 14
                                 
                 
 
         |
58 | | imaexg 6749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
       |
59 | | difexg 4545 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         
     |
60 | 45, 58, 59 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
         |
61 | 60 | 0dom 7720 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
         |
62 | | breq1 4398 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

        
           |
63 | 61, 62 | mpbiri 241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

    
     |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
     

                  |
65 | | simpll 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
      
     
                     |
66 | | elpwi 3951 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     
      |
67 | 66 | ad2antrl 742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
      
     
        
      |
68 | | difsnpss 4106 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35

      |
69 | 68 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
     |
70 | 69 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
      
     
               |
71 | 67, 70 | sspsstrd 3527 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
      
     
        
  |
72 | | simprr 774 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
      
     
           |
73 | 71, 72 | jca 541 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
      
     
         
   |
74 | | psseq1 3506 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
   |
75 | | neeq1 2705 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 
   |
76 | 74, 75 | anbi12d 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
  

     |
77 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   |
78 | | imaeq2 5170 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
           |
79 | 77, 78 | breq12d 4408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     
       |
80 | 76, 79 | imbi12d 327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         
 
         |
81 | 80 | spv 2117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
            
        |
82 | 65, 73, 81 | sylc 61 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
      
     
               |
83 | | domdifsn 7673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    
          |
84 | 82, 83 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
      
     
                   |
85 | 84 | expr 626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      
     

                  |
86 | 64, 85 | pm2.61dne 2729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      
     

                |
87 | 86 | adantlrr 735 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
      
                               |
88 | 87 | adantll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                             
        
 
              |
89 | | df-ss 3404 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
      
      |
90 | 66, 89 | sylib 201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
        |
91 | 90 | imaeq2d 5174 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
                |
92 | 91 | ineq1d 3624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
           
         
      |
93 | 92 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                             
        
 
         
                      |
94 | | indif2 3677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
               
     |
95 | | imassrn 5185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     |
96 | | elpwi 3951 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   
    |
97 | | rnss 5069 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
       |
98 | | rnxpss 5275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   |
99 | 97, 98 | syl6ss 3430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     |
100 | 96, 99 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
  |
101 | 95, 100 | syl5ss 3429 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       
  |
102 | | df-ss 3404 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
            |
103 | 101, 102 | sylib 201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                |
104 | 103 | difeq1d 3539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                        |
105 | 104 | ad2antrl 742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       
              
       
     |
106 | 94, 105 | syl5eq 2517 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       
            
               |
107 | 106 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                             
        
 
         
              |
108 | 93, 107 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                             
        
 
         
                    |
109 | 88, 108 | breqtrrd 4422 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                             
        
 
                      |
110 | 109 | ralrimiva 2809 |
. . . . . . . . . . . . . . . . . . . . . . 23
   

                       
         
          
            |
111 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
112 | | imainrect 5284 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
             
           |
113 | | imaeq2 5170 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                   |
114 | 112, 113 | syl5eqr 2519 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     
      
                      |
115 | 111, 114 | breq12d 4408 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                 
       
           |
116 | 115 | cbvralv 3005 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

        
      
   
                        |
117 | 110, 116 | sylib 201 |
. . . . . . . . . . . . . . . . . . . . . 22
   

                       
         
                       |
118 | 117 | adantllr 733 |
. . . . . . . . . . . . . . . . . . . . 21
                                 
                           
                        |
119 | | inss2 3644 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                       |
120 | | difss 3549 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
 |
121 | | xpss2 4949 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
              
 
      |
122 | 120, 121 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
           |
123 | 119, 122 | sstri 3427 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   |
124 | 45 | inex1 4537 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             |
125 | 124 | elpw 3948 |
. . . . . . . . . . . . . . . . . . . . . . 23
       
                                |
126 | 123, 125 | mpbir 214 |
. . . . . . . . . . . . . . . . . . . . . 22
                    |
127 | | simpllr 777 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                 
                           
                        |
128 | 69 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
      
      |
129 | 128 | ad2antll 743 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                 
                           
      |
130 | | vex 3034 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
131 | | difexg 4545 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
     |
132 | 130, 131 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
133 | | psseq1 3506 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             |
134 | | xpeq1 4853 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
               |
135 | 134 | pweqd 3947 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                 |
136 | | pweq 3945 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
             |
137 | 136 | raleqdv 2979 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
            
            |
138 | | f1eq2 5788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         
           |
139 | 138 | rexbidv 2892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           
             |
140 | 137, 139 | imbi12d 327 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       
           
 

                      |
141 | 135, 140 | raleqbidv 2987 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           
           
                                 |
142 | 133, 141 | imbi12d 327 |
. . . . . . . . . . . . . . . . . . . . . . . 24
            
            
 
                     
               |
143 | 132, 142 | spcv 3126 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                                             |
144 | 127, 129,
143 | sylc 61 |
. . . . . . . . . . . . . . . . . . . . . 22
                                 
                           
                                |
145 | | imaeq1 5169 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                   |
146 | 145 | breq2d 4407 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                 
       
           |
147 | 146 | ralbidv 2829 |
. . . . . . . . . . . . . . . . . . . . . . . 24
              
                                  |
148 | | pweq 3945 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             
 
 
   
       |
149 | 148 | rexeqdv 2980 |
. . . . . . . . . . . . . . . . . . . . . . . 24
              
        
                         |
150 | 147, 149 | imbi12d 327 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                                                                     |
151 | 150 | rspcva 3134 |
. . . . . . . . . . . . . . . . . . . . . 22
                     
        

                   
 

                                             |
152 | 126, 144,
151 | sylancr 676 |
. . . . . . . . . . . . . . . . . . . . 21
                                 
                           
 

                                             |
153 | 118, 152 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
                                 
                           
                        |
154 | | f1eq1 5787 |
. . . . . . . . . . . . . . . . . . . . 21
         
           |
155 | 154 | cbvrexv 3006 |
. . . . . . . . . . . . . . . . . . . 20
  
 
   
             
                        |
156 | 153, 155 | sylib 201 |
. . . . . . . . . . . . . . . . . . 19
                                 
                           
                        |
157 | | vex 3034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 |
158 | 38, 157 | elimasn 5199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
            |
159 | 158 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
            |
160 | 159 | snssd 4108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
              |
161 | 160 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
         
 
 
   
     
       |
162 | | elpwi 3951 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             
              |
163 | | inss1 3643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             |
164 | 162, 163 | syl6ss 3430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
             
  |
165 | 164 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
         
 
 
   
     
  |
166 | 161, 165 | unssd 3601 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         
 
 
   
     
     
   |
167 | 45 | elpw2 4565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
        
     
   |
168 | 166, 167 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
         
 
 
   
     
     
    |
169 | 168 | ad2ant2lr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     

                                          |
170 | 38, 157 | f1osn 5866 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
              |
171 | 170 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
 
   
                             |
172 | | f1f1orn 5839 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
        
          |
173 | 172 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
 
   
                        |
174 | | disjdif 3830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   
     |
175 | 174 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
 
   
                        |
176 | | incom 3616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
         |
177 | 162, 119 | syl6ss 3430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
             
 
   
      |
178 | | rnss 5069 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
                
      |
179 | | rnxpss 5275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
               |
180 | 178, 179 | syl6ss 3430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                 |
181 | 177, 180 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
             
      |
182 | | incom 3616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
                 |
183 | | disjdif 3830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
   
     |
184 | 182, 183 | eqtri 2493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
         |
185 | | ssdisj 3818 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
  
            
     |
186 | 181, 184,
185 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
              
     |
187 | 176, 186 | syl5eq 2517 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                
   |
188 | 187 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
 
   
                
   |
189 | | f1oun 5847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                                                                 |
190 | 171, 173,
175, 188, 189 | syl22anc 1293 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
 
   
                                       |
191 | 190 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     

                                                         |
192 | | snssi 4107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
  
  |
193 | 192 | ad2antrl 742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             
    |
194 | | undif 3839 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             |
195 | 193, 194 | sylib 201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
             
   
      |
196 | | f1oeq2 5819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                                
     
            |
197 | 195, 196 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
             
                                          |
198 | 197 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     

                                                       
     
            |
199 | 191, 198 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     

                                                 |
200 | | f1of1 5827 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                                 |
201 | | ssv 3438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     |
202 | | f1ss 5797 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                    
              |
203 | 200, 201,
202 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                             |
204 | 199, 203 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     

                                             |
205 | | f1eq1 5787 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                           |
206 | 205 | rspcev 3136 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                              |
207 | 169, 204,
206 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     

                                
       |
208 | 207 | rexlimdvaa 2872 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             
 

 
   
             
         |
209 | 208 | ex 441 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                              |
210 | 209 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . 22
           
 
      
 

 
   
             
          |
211 | 210 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . . . 21
   

                                                                 |
212 | 211 | impr 631 |
. . . . . . . . . . . . . . . . . . . 20
   

                       
                                         |
213 | 212 | adantllr 733 |
. . . . . . . . . . . . . . . . . . 19
                                 
                           
 

 
   
             
         |
214 | 156, 213 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
                                 
                           
        |
215 | 214 | expr 626 |
. . . . . . . . . . . . . . . . 17
                                 
          
                         |
216 | 215 | expd 443 |
. . . . . . . . . . . . . . . 16
                                 
          
       
       
         |
217 | 216 | impr 631 |
. . . . . . . . . . . . . . 15
                                 
                 
 
       
        |
218 | 217 | exlimdv 1787 |
. . . . . . . . . . . . . 14
                                 
                 
 
 
               |
219 | 57, 218 | mpd 15 |
. . . . . . . . . . . . 13
                                 
                 
 
        |
220 | 219 | expr 626 |
. . . . . . . . . . . 12
                                 
          
       
         |
221 | 220 | exlimdv 1787 |
. . . . . . . . . . 11
                                 
          
         
        |
222 | 32, 221 | syl5bi 225 |
. . . . . . . . . 10
                                 
          
                 |
223 | 31, 222 | pm2.61dne 2729 |
. . . . . . . . 9
                                 
          
               |
224 | | exanali 1729 |
. . . . . . . . . 10
          
            |
225 | | simprll 780 |
. . . . . . . . . . . . . . . . . . . 20
                                 
                  |
226 | | pssss 3514 |
. . . . . . . . . . . . . . . . . . . 20
   |
227 | 225, 226 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
                                 
                  |
228 | | sspwb 4649 |
. . . . . . . . . . . . . . . . . . 19

    |
229 | 227, 228 | sylib 201 |
. . . . . . . . . . . . . . . . . 18
                                 
                    |
230 | | simplrr 779 |
. . . . . . . . . . . . . . . . . 18
                                 
                        |
231 | | ssralv 3479 |
. . . . . . . . . . . . . . . . . 18
 
                 |
232 | 229, 230,
231 | sylc 61 |
. . . . . . . . . . . . . . . . 17
                                 
                        |
233 | | elpwi 3951 |
. . . . . . . . . . . . . . . . . . . . 21
 
  |
234 | | resima2 5144 |
. . . . . . . . . . . . . . . . . . . . 21
             |
235 | 233, 234 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
              |
236 | 235 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . . 19
       
      |
237 | 236 | breq2d 4407 |
. . . . . . . . . . . . . . . . . 18
      
 
       |
238 | 237 | ralbiia 2822 |
. . . . . . . . . . . . . . . . 17
 
    
          |
239 | 232, 238 | sylib 201 |
. . . . . . . . . . . . . . . 16
                                 
                   
      |
240 | | simplrl 778 |
. . . . . . . . . . . . . . . . . 18
                                 
                     |
241 | | ssres 5136 |
. . . . . . . . . . . . . . . . . . . . 21
           |
242 | | df-res 4851 |
. . . . . . . . . . . . . . . . . . . . . 22
      
    |
243 | | inxp 4972 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
244 | | inss2 3644 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
245 | | inss1 3643 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
246 | | xpss12 4945 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
      
 
    |
247 | 244, 245,
246 | mp2an 686 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
  |
248 | 243, 247 | eqsstri 3448 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
249 | 242, 248 | eqsstri 3448 |
. . . . . . . . . . . . . . . . . . . . 21
       |
250 | 241, 249 | syl6ss 3430 |
. . . . . . . . . . . . . . . . . . . 20
     
   |
251 | 96, 250 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
     
    |
252 | 45 | resex 5154 |
. . . . . . . . . . . . . . . . . . . 20
   |
253 | 252 | elpw 3948 |
. . . . . . . . . . . . . . . . . . 19
 
   
      |
254 | 251, 253 | sylibr 217 |
. . . . . . . . . . . . . . . . . 18
           |
255 | 240, 254 | syl 17 |
. . . . . . . . . . . . . . . . 17
                                 
                   
   |
256 | | simpllr 777 |
. . . . . . . . . . . . . . . . . 18
                                 
                        
               |
257 | | psseq1 3506 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
258 | | xpeq1 4853 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
259 | 258 | pweqd 3947 |
. . . . . . . . . . . . . . . . . . . . 21
         |
260 | | pweq 3945 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
261 | 260 | raleqdv 2979 |
. . . . . . . . . . . . . . . . . . . . . 22
  
    
         |
262 | | f1eq2 5788 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
263 | 262 | rexbidv 2892 |
. . . . . . . . . . . . . . . . . . . . . 22
  
              |
264 | 261, 263 | imbi12d 327 |
. . . . . . . . . . . . . . . . . . . . 21
               
 
               |
265 | 259, 264 | raleqbidv 2987 |
. . . . . . . . . . . . . . . . . . . 20
  
                
     
               |
266 | 257, 265 | imbi12d 327 |
. . . . . . . . . . . . . . . . . . 19
                     

     
                |
267 | 266 | spv 2117 |
. . . . . . . . . . . . . . . . . 18
                         
                   |
268 | 256, 225,
267 | sylc 61 |
. . . . . . . . . . . . . . . . 17
                                 
                 
                  |
269 | | imaeq1 5169 |
. . . . . . . . . . . . . . . . . . . . 21
               |
270 | 269 | breq2d 4407 |
. . . . . . . . . . . . . . . . . . . 20
       
 
       |
271 | 270 | ralbidv 2829 |
. . . . . . . . . . . . . . . . . . 19
    
    
           |
272 | | pweq 3945 |
. . . . . . . . . . . . . . . . . . . 20
   
     |
273 | 272 | rexeqdv 2980 |
. . . . . . . . . . . . . . . . . . 19
    
                |
274 | 271, 273 | imbi12d 327 |
. . . . . . . . . . . . . . . . . 18
                 
 
      
            |
275 | 274 | rspcva 3134 |
. . . . . . . . . . . . . . . . 17
            
                                 |
276 | 255, 268,
275 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
                                 
                                    |
277 | 239, 276 | mpd 15 |
. . . . . . . . . . . . . . 15
                                 
                          |
278 | | f1eq1 5787 |
. . . . . . . . . . . . . . . 16
             |
279 | 278 | cbvrexv 3006 |
. . . . . . . . . . . . . . 15
        
          |
280 | 277, 279 | sylib 201 |
. . . . . . . . . . . . . 14
                                 
                          |
281 | 226 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  

       |
282 | 281 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                   

            |
283 | | elpwi 3951 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
    |
284 | | difss 3549 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   |
285 | 283, 284 | syl6ss 3430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
  |
286 | 285 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                   

         
  |
287 | 282, 286 | unssd 3601 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                   

           
  |
288 | 130 | elpw2 4565 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
    |
289 | 287, 288 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   

               |
290 | | simprr 774 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
                |
291 | 290 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   

          
       |
292 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       |
293 | | imaeq2 5170 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
               |
294 | 292, 293 | breq12d 4408 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
           |
295 | 294 | rspcva 3134 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                      |
296 | 289, 291,
295 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   

                    |
297 | | imaundi 5254 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                 |
298 | | undif2 3834 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    |