Step | Hyp | Ref
| Expression |
1 | | vex 2554 |
. . . . . . . . . 10
 |
2 | | vex 2554 |
. . . . . . . . . 10
 |
3 | | eleq1 2097 |
. . . . . . . . . . . 12
 
       |
4 | 3 | anbi1d 438 |
. . . . . . . . . . 11
  
 
     
      |
5 | | eqeq1 2043 |
. . . . . . . . . . . . . 14
 
  
      |
6 | 5 | anbi1d 438 |
. . . . . . . . . . . . 13
  
                  |
7 | 6 | anbi1d 438 |
. . . . . . . . . . . 12
               
 
  
            |
8 | 7 | 4exbidv 1747 |
. . . . . . . . . . 11
              
        
                         |
9 | 4, 8 | anbi12d 442 |
. . . . . . . . . 10
     
                                
                          |
10 | | eleq1 2097 |
. . . . . . . . . . . 12
 
       |
11 | 10 | anbi2d 437 |
. . . . . . . . . . 11
  
 
     
      |
12 | | eqeq1 2043 |
. . . . . . . . . . . . . 14
 
  
      |
13 | 12 | anbi2d 437 |
. . . . . . . . . . . . 13
  
                  |
14 | 13 | anbi1d 438 |
. . . . . . . . . . . 12
               
 
  
            |
15 | 14 | 4exbidv 1747 |
. . . . . . . . . . 11
              
        
                         |
16 | 11, 15 | anbi12d 442 |
. . . . . . . . . 10
     
                                
                          |
17 | | df-enq0 6407 |
. . . . . . . . . 10
~Q0    
 
 
               
            |
18 | 1, 2, 9, 16, 17 | brab 4000 |
. . . . . . . . 9
 ~Q0    
                            |
19 | | vex 2554 |
. . . . . . . . . 10
 |
20 | | eleq1 2097 |
. . . . . . . . . . . 12
 
       |
21 | 20 | anbi1d 438 |
. . . . . . . . . . 11
  
 
     
      |
22 | | eqeq1 2043 |
. . . . . . . . . . . . . 14
 
  
      |
23 | 22 | anbi1d 438 |
. . . . . . . . . . . . 13
  
      
           |
24 | 23 | anbi1d 438 |
. . . . . . . . . . . 12
          
             
        |
25 | 24 | 4exbidv 1747 |
. . . . . . . . . . 11
                  
                       
      |
26 | 21, 25 | anbi12d 442 |
. . . . . . . . . 10
     
                   
                               
       |
27 | | eleq1 2097 |
. . . . . . . . . . . 12
 
       |
28 | 27 | anbi2d 437 |
. . . . . . . . . . 11
  
 
     
      |
29 | | eqeq1 2043 |
. . . . . . . . . . . . . 14
 
  
      |
30 | 29 | anbi2d 437 |
. . . . . . . . . . . . 13
  
      
           |
31 | 30 | anbi1d 438 |
. . . . . . . . . . . 12
          
             
        |
32 | 31 | 4exbidv 1747 |
. . . . . . . . . . 11
                  
                       
      |
33 | 28, 32 | anbi12d 442 |
. . . . . . . . . 10
     
                   
                               
       |
34 | | df-enq0 6407 |
. . . . . . . . . 10
~Q0    
 
 
                   
        |
35 | 2, 19, 26, 33, 34 | brab 4000 |
. . . . . . . . 9
 ~Q0    
                   
        |
36 | 18, 35 | anbi12i 433 |
. . . . . . . 8
  ~Q0
~Q0      
                           
 
                   
         |
37 | 36 | biimpi 113 |
. . . . . . 7
  ~Q0
~Q0      
                           
 
                   
         |
38 | | an4 520 |
. . . . . . 7
                                 
 
                   
              

                   
        
                  
       |
39 | 37, 38 | sylib 127 |
. . . . . 6
  ~Q0
~Q0      
     
                       
                   
         |
40 | | 3anass 888 |
. . . . . . . 8
              
      |
41 | | anass 381 |
. . . . . . . . 9
    
     
                    |
42 | | anass 381 |
. . . . . . . . . 10
    
  
        
      |
43 | 42 | anbi2i 430 |
. . . . . . . . 9
     
 
  
            
       |
44 | | anidm 376 |
. . . . . . . . . . 11
      
    |
45 | 44 | anbi1i 431 |
. . . . . . . . . 10
    
  
     
     |
46 | 45 | anbi2i 430 |
. . . . . . . . 9
     
 
  
         
      |
47 | 41, 43, 46 | 3bitr2i 197 |
. . . . . . . 8
    
     
                |
48 | 40, 47 | bitr4i 176 |
. . . . . . 7
                         |
49 | 48 | anbi1i 431 |
. . . . . 6
    
 
                         
                  
            

                   
        
                  
       |
50 | 39, 49 | sylibr 137 |
. . . . 5
  ~Q0
~Q0   
 
    
             
        
                  
       |
51 | | ee8anv 1807 |
. . . . . 6
                      
        
 
      
                            
                  
      |
52 | 51 | anbi2i 430 |
. . . . 5
    
 
                        
        
 
      
          
                           
                  
       |
53 | 50, 52 | sylibr 137 |
. . . 4
  ~Q0
~Q0   
 
    
                              
 
      
         |
54 | | 19.42vvvv 1787 |
. . . . . . 7
            
          
        
 
      
          
                  
        
 
      
         |
55 | 54 | 2exbii 1494 |
. . . . . 6
                
          
        
 
      
                
                         
 
      
         |
56 | 55 | 2exbii 1494 |
. . . . 5
                    
          
        
 
      
                  
 
                         
 
      
         |
57 | | 19.42vvvv 1787 |
. . . . 5
            
                  
        
 
      
          
                                   
 
      
         |
58 | 56, 57 | bitri 173 |
. . . 4
                    
          
        
 
      
          
                                   
 
      
         |
59 | 53, 58 | sylibr 137 |
. . 3
  ~Q0
~Q0                     
          
        
 
      
         |
60 | | 3simpb 901 |
. . . . . . . . 9
                 |
61 | 60 | adantr 261 |
. . . . . . . 8
    
 
                 
 
      
         
     |
62 | | simplll 485 |
. . . . . . . . . 10
               
 
      
           |
63 | | simprlr 490 |
. . . . . . . . . 10
               
 
      
           |
64 | 62, 63 | jca 290 |
. . . . . . . . 9
               
 
      
                |
65 | 64 | adantl 262 |
. . . . . . . 8
    
 
                 
 
      
                 |
66 | | oveq1 5462 |
. . . . . . . . . . . . . . . 16

  
   |
67 | 63 | adantl 262 |
. . . . . . . . . . . . . . . . . . . . . 22
    
 
                 
 
      
            |
68 | | simpl3 908 |
. . . . . . . . . . . . . . . . . . . . . 22
    
 
                 
 
      
           |
69 | 67, 68 | eqeltrrd 2112 |
. . . . . . . . . . . . . . . . . . . . 21
    
 
                 
 
      
              |
70 | | opelxp 4317 |
. . . . . . . . . . . . . . . . . . . . 21
      
   |
71 | 69, 70 | sylib 127 |
. . . . . . . . . . . . . . . . . . . 20
    
 
                 
 
      
           |
72 | 71 | simprd 107 |
. . . . . . . . . . . . . . . . . . 19
    
 
                 
 
      
         |
73 | | pinn 6293 |
. . . . . . . . . . . . . . . . . . 19
   |
74 | 72, 73 | syl 14 |
. . . . . . . . . . . . . . . . . 18
    
 
                 
 
      
         |
75 | | nnm0r 5997 |
. . . . . . . . . . . . . . . . . 18
     |
76 | 74, 75 | syl 14 |
. . . . . . . . . . . . . . . . 17
    
 
                 
 
      
           |
77 | 76 | eqeq2d 2048 |
. . . . . . . . . . . . . . . 16
    
 
                 
 
      
             
   |
78 | 66, 77 | syl5ib 143 |
. . . . . . . . . . . . . . 15
    
 
                 
 
      
       
     |
79 | | simprr 484 |
. . . . . . . . . . . . . . . . . 18
               
 
      
       
    |
80 | | eqtr2 2055 |
. . . . . . . . . . . . . . . . . . . . . 22
    
   
  
     |
81 | | vex 2554 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
82 | | vex 2554 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
83 | 81, 82 | opth 3965 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
84 | 80, 83 | sylib 127 |
. . . . . . . . . . . . . . . . . . . . 21
    
   

   |
85 | | oveq1 5462 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
86 | | oveq1 5462 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
87 | 85, 86 | eqeqan12d 2052 |
. . . . . . . . . . . . . . . . . . . . 21
 
   
         |
88 | 84, 87 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
    
   
 

         |
89 | 88 | ad2ant2lr 479 |
. . . . . . . . . . . . . . . . . . 19
                         
     |
90 | 89 | ad2ant2r 478 |
. . . . . . . . . . . . . . . . . 18
               
 
      
        
         |
91 | 79, 90 | mpbird 156 |
. . . . . . . . . . . . . . . . 17
               
 
      
       
    |
92 | 91 | eqeq1d 2045 |
. . . . . . . . . . . . . . . 16
               
 
      
        
     |
93 | 92 | adantl 262 |
. . . . . . . . . . . . . . 15
    
 
                 
 
      
         
     |
94 | 78, 93 | sylibd 138 |
. . . . . . . . . . . . . 14
    
 
                 
 
      
       
     |
95 | | simpllr 486 |
. . . . . . . . . . . . . . . . . . . 20
               
 
      
           |
96 | 95 | adantl 262 |
. . . . . . . . . . . . . . . . . . 19
    
 
                 
 
      
            |
97 | | simpl2 907 |
. . . . . . . . . . . . . . . . . . 19
    
 
                 
 
      
           |
98 | 96, 97 | eqeltrrd 2112 |
. . . . . . . . . . . . . . . . . 18
    
 
                 
 
      
         
    |
99 | | opelxp 4317 |
. . . . . . . . . . . . . . . . . 18
      
   |
100 | 98, 99 | sylib 127 |
. . . . . . . . . . . . . . . . 17
    
 
                 
 
      
           |
101 | 100 | simprd 107 |
. . . . . . . . . . . . . . . 16
    
 
                 
 
      
         |
102 | | pinn 6293 |
. . . . . . . . . . . . . . . 16
   |
103 | 101, 102 | syl 14 |
. . . . . . . . . . . . . . 15
    
 
                 
 
      
         |
104 | 71 | simpld 105 |
. . . . . . . . . . . . . . 15
    
 
                 
 
      
         |
105 | | nnm00 6038 |
. . . . . . . . . . . . . . 15
 
   

    |
106 | 103, 104,
105 | syl2anc 391 |
. . . . . . . . . . . . . 14
    
 
                 
 
      
         
     |
107 | 94, 106 | sylibd 138 |
. . . . . . . . . . . . 13
    
 
                 
 
      
       

    |
108 | | elni2 6298 |
. . . . . . . . . . . . . . . 16
     |
109 | 108 | simprbi 260 |
. . . . . . . . . . . . . . 15
   |
110 | 101, 109 | syl 14 |
. . . . . . . . . . . . . 14
    
 
                 
 
      
         |
111 | | n0i 3223 |
. . . . . . . . . . . . . 14

  |
112 | | biorf 662 |
. . . . . . . . . . . . . 14
  
    |
113 | 110, 111,
112 | 3syl 17 |
. . . . . . . . . . . . 13
    
 
                 
 
      
       
     |
114 | 107, 113 | sylibrd 158 |
. . . . . . . . . . . 12
    
 
                 
 
      
       
   |
115 | 62 | adantl 262 |
. . . . . . . . . . . . . . . . . 18
    
 
                 
 
      
            |
116 | | simpl1 906 |
. . . . . . . . . . . . . . . . . 18
    
 
                 
 
      
           |
117 | 115, 116 | eqeltrrd 2112 |
. . . . . . . . . . . . . . . . 17
    
 
                 
 
      
         
    |
118 | | opelxp 4317 |
. . . . . . . . . . . . . . . . 17
      
   |
119 | 117, 118 | sylib 127 |
. . . . . . . . . . . . . . . 16
    
 
                 
 
      
           |
120 | 119 | simprd 107 |
. . . . . . . . . . . . . . 15
    
 
                 
 
      
         |
121 | | pinn 6293 |
. . . . . . . . . . . . . . 15
   |
122 | 120, 121 | syl 14 |
. . . . . . . . . . . . . 14
    
 
                 
 
      
         |
123 | | nnm0 5993 |
. . . . . . . . . . . . . 14
     |
124 | 122, 123 | syl 14 |
. . . . . . . . . . . . 13
    
 
                 
 
      
           |
125 | | oveq2 5463 |
. . . . . . . . . . . . . 14

      |
126 | 125 | eqeq1d 2045 |
. . . . . . . . . . . . 13

 

     |
127 | 124, 126 | syl5ibrcom 146 |
. . . . . . . . . . . 12
    
 
                 
 
      
       
     |
128 | 114, 127 | syld 40 |
. . . . . . . . . . 11
    
 
                 
 
      
       
     |
129 | | oveq2 5463 |
. . . . . . . . . . . . . . . 16

      |
130 | 124 | eqeq2d 2048 |
. . . . . . . . . . . . . . . 16
    
 
                 
 
      
             
   |
131 | 129, 130 | syl5ib 143 |
. . . . . . . . . . . . . . 15
    
 
                 
 
      
       
     |
132 | | simprlr 490 |
. . . . . . . . . . . . . . . 16
    
 
                 
 
      
             |
133 | 132 | eqeq1d 2045 |
. . . . . . . . . . . . . . 15
    
 
                 
 
      
         
     |
134 | 131, 133 | sylibrd 158 |
. . . . . . . . . . . . . 14
    
 
                 
 
      
       
     |
135 | 119 | simpld 105 |
. . . . . . . . . . . . . . 15
    
 
                 
 
      
         |
136 | | nnm00 6038 |
. . . . . . . . . . . . . . 15
 
   

    |
137 | 135, 103,
136 | syl2anc 391 |
. . . . . . . . . . . . . 14
    
 
                 
 
      
         
     |
138 | 134, 137 | sylibd 138 |
. . . . . . . . . . . . 13
    
 
                 
 
      
       

    |
139 | | biorf 662 |
. . . . . . . . . . . . . . 15
 

    |
140 | | orcom 646 |
. . . . . . . . . . . . . . 15
   
   |
141 | 139, 140 | syl6bb 185 |
. . . . . . . . . . . . . 14
 

    |
142 | 110, 111,
141 | 3syl 17 |
. . . . . . . . . . . . 13
    
 
                 
 
      
       
     |
143 | 138, 142 | sylibrd 158 |
. . . . . . . . . . . 12
    
 
                 
 
      
       
   |
144 | | oveq1 5462 |
. . . . . . . . . . . . . 14

  
   |
145 | 144 | eqeq1d 2045 |
. . . . . . . . . . . . 13

 

     |
146 | 76, 145 | syl5ibrcom 146 |
. . . . . . . . . . . 12
    
 
                 
 
      
       
     |
147 | 143, 146 | syld 40 |
. . . . . . . . . . 11
    
 
                 
 
      
       
     |
148 | 128, 147 | jcad 291 |
. . . . . . . . . 10
    
 
                 
 
      
       
 

      |
149 | | eqtr3 2056 |
. . . . . . . . . . 11
   
  
      |
150 | 149 | eqcomd 2042 |
. . . . . . . . . 10
   
  
      |
151 | 148, 150 | syl6 29 |
. . . . . . . . 9
    
 
                 
 
      
       
       |
152 | | simplr 482 |
. . . . . . . . . . . . . . . . 17
               
 
      
       
    |
153 | 91, 152 | oveq12d 5473 |
. . . . . . . . . . . . . . . 16
               
 
      
        
      
    |
154 | 153 | adantl 262 |
. . . . . . . . . . . . . . 15
    
 
                 
 
      
                     |
155 | 100 | simpld 105 |
. . . . . . . . . . . . . . . . 17
    
 
                 
 
      
         |
156 | | nnmcl 5999 |
. . . . . . . . . . . . . . . . 17
 
  
  |
157 | 155, 74, 156 | syl2anc 391 |
. . . . . . . . . . . . . . . 16
    
 
                 
 
      
           |
158 | | nnmcom 6007 |
. . . . . . . . . . . . . . . . 17
 
  
    |
159 | 158 | adantl 262 |
. . . . . . . . . . . . . . . 16
       
              
           
          

    |
160 | | nnmass 6005 |
. . . . . . . . . . . . . . . . 17
 
  
        |
161 | 160 | adantl 262 |
. . . . . . . . . . . . . . . 16
       
              
           
                    |
162 | 157, 135,
103, 159, 161 | caov13d 5626 |
. . . . . . . . . . . . . . 15
    
 
                 
 
      
                     |
163 | | nnmcl 5999 |
. . . . . . . . . . . . . . . . 17
 
  
  |
164 | 122, 155,
163 | syl2anc 391 |
. . . . . . . . . . . . . . . 16
    
 
                 
 
      
           |
165 | 161, 103,
104, 164 | caovassd 5602 |
. . . . . . . . . . . . . . 15
    
 
                 
 
      
                     |
166 | 154, 162,
165 | 3eqtr3d 2077 |
. . . . . . . . . . . . . 14
    
 
                 
 
      
         
           |
167 | | nnmcl 5999 |
. . . . . . . . . . . . . . . 16
  

       |
168 | 135, 157,
167 | syl2anc 391 |
. . . . . . . . . . . . . . 15
    
 
                 
 
      
             |
169 | | nnmcl 5999 |
. . . . . . . . . . . . . . . 16
  

       |
170 | 104, 164,
169 | syl2anc 391 |
. . . . . . . . . . . . . . 15
    
 
                 
 
      
             |
171 | | nnmcan 6028 |
. . . . . . . . . . . . . . 15
              
      
     
 
       |
172 | 103, 168,
170, 110, 171 | syl31anc 1137 |
. . . . . . . . . . . . . 14
    
 
                 
 
      
               
     
 
       |
173 | 166, 172 | mpbid 135 |
. . . . . . . . . . . . 13
    
 
                 
 
      
                 |
174 | 135, 155,
74, 159, 161 | caov12d 5624 |
. . . . . . . . . . . . 13
    
 
                 
 
      
                 |
175 | 104, 122,
155, 159, 161 | caov13d 5626 |
. . . . . . . . . . . . 13
    
 
                 
 
      
                 |
176 | 173, 174,
175 | 3eqtr3d 2077 |
. . . . . . . . . . . 12
    
 
                 
 
      
                 |
177 | 176 | adantr 261 |
. . . . . . . . . . 11
       
              
           
                  |
178 | | nnmcl 5999 |
. . . . . . . . . . . . . 14
 
  
  |
179 | 135, 74, 178 | syl2anc 391 |
. . . . . . . . . . . . 13
    
 
                 
 
      
           |
180 | | nnmcl 5999 |
. . . . . . . . . . . . . 14
 
  
  |
181 | 122, 104,
180 | syl2anc 391 |
. . . . . . . . . . . . 13
    
 
                 
 
      
           |
182 | 155, 179,
181 | 3jca 1083 |
. . . . . . . . . . . 12
    
 
                 
 
      
         
     |
183 | | nnmcan 6028 |
. . . . . . . . . . . 12
    
          
 
       |
184 | 182, 183 | sylan 267 |
. . . . . . . . . . 11
       
              
           
              
 
       |
185 | 177, 184 | mpbid 135 |
. . . . . . . . . 10
       
              
           
              |
186 | 185 | ex 108 |
. . . . . . . . 9
    
 
                 
 
      
       
       |
187 | | 0elnn 4283 |
. . . . . . . . . 10
 
   |
188 | 155, 187 | syl 14 |
. . . . . . . . 9
    
 
                 
 
      
       
   |
189 | 151, 186,
188 | mpjaod 637 |
. . . . . . . 8
    
 
                 
 
      
             |
190 | 61, 65, 189 | jca32 293 |
. . . . . . 7
    
 
                 
 
      
             
 
      
        |
191 | 190 | 2eximi 1489 |
. . . . . 6
                   
        
 
      
              
  
 
      
        |
192 | 191 | exlimivv 1773 |
. . . . 5
            
          
        
 
      
              
  
 
      
        |
193 | 192 | exlimivv 1773 |
. . . 4
                
          
        
 
      
              
  
 
      
        |
194 | 193 | 2eximi 1489 |
. . 3
                    
          
        
 
      
                  
  
 
      
        |
195 | 59, 194 | syl 14 |
. 2
  ~Q0
~Q0             
  
 
      
        |
196 | | 19.42vvvv 1787 |
. . 3
            
  
 
      
            
                  
      |
197 | 5 | anbi1d 438 |
. . . . . . 7
  
      
           |
198 | 197 | anbi1d 438 |
. . . . . 6
          
    
 
  
   
        |
199 | 198 | 4exbidv 1747 |
. . . . 5
              
   
    
                  
      |
200 | 4, 199 | anbi12d 442 |
. . . 4
     
                   
            
     |