Step | Hyp | Ref
| Expression |
1 | | vex 2740 |
. . . . . . . . . 10
 |
2 | | vex 2740 |
. . . . . . . . . 10
 |
3 | | eleq1 2240 |
. . . . . . . . . . . 12
   
     |
4 | 3 | anbi1d 465 |
. . . . . . . . . . 11
    
     
      |
5 | | eqeq1 2184 |
. . . . . . . . . . . . . 14
    
      |
6 | 5 | anbi1d 465 |
. . . . . . . . . . . . 13
                     |
7 | 6 | anbi1d 465 |
. . . . . . . . . . . 12
               
    
            |
8 | 7 | 4exbidv 1870 |
. . . . . . . . . . 11
              
        
                         |
9 | 4, 8 | anbi12d 473 |
. . . . . . . . . 10
        
                          
                             |
10 | | eleq1 2240 |
. . . . . . . . . . . 12
   
     |
11 | 10 | anbi2d 464 |
. . . . . . . . . . 11
    
     
      |
12 | | eqeq1 2184 |
. . . . . . . . . . . . . 14
    
      |
13 | 12 | anbi2d 464 |
. . . . . . . . . . . . 13
                     |
14 | 13 | anbi1d 465 |
. . . . . . . . . . . 12
               
    
            |
15 | 14 | 4exbidv 1870 |
. . . . . . . . . . 11
              
        
                         |
16 | 11, 15 | anbi12d 473 |
. . . . . . . . . 10
        
                          
                             |
17 | | df-enq0 7422 |
. . . . . . . . . 10
~Q0        
                            |
18 | 1, 2, 9, 16, 17 | brab 4272 |
. . . . . . . . 9
 ~Q0    
                            |
19 | | vex 2740 |
. . . . . . . . . 10
 |
20 | | eleq1 2240 |
. . . . . . . . . . . 12
   
     |
21 | 20 | anbi1d 465 |
. . . . . . . . . . 11
    
     
      |
22 | | eqeq1 2184 |
. . . . . . . . . . . . . 14
    
      |
23 | 22 | anbi1d 465 |
. . . . . . . . . . . . 13
         
   
       |
24 | 23 | anbi1d 465 |
. . . . . . . . . . . 12
      
             
            |
25 | 24 | 4exbidv 1870 |
. . . . . . . . . . 11
                  
    
                         |
26 | 21, 25 | anbi12d 473 |
. . . . . . . . . 10
        
                          
                             |
27 | | eleq1 2240 |
. . . . . . . . . . . 12
   
     |
28 | 27 | anbi2d 464 |
. . . . . . . . . . 11
    
     
      |
29 | | eqeq1 2184 |
. . . . . . . . . . . . . 14
    
      |
30 | 29 | anbi2d 464 |
. . . . . . . . . . . . 13
         
   
       |
31 | 30 | anbi1d 465 |
. . . . . . . . . . . 12
      
             
            |
32 | 31 | 4exbidv 1870 |
. . . . . . . . . . 11
                  
    
                         |
33 | 28, 32 | anbi12d 473 |
. . . . . . . . . 10
        
                          
                             |
34 | | df-enq0 7422 |
. . . . . . . . . 10
~Q0        
                            |
35 | 2, 19, 26, 33, 34 | brab 4272 |
. . . . . . . . 9
 ~Q0    
                            |
36 | 18, 35 | anbi12i 460 |
. . . . . . . 8
  ~Q0
~Q0 
    
                                                           |
37 | 36 | biimpi 120 |
. . . . . . 7
  ~Q0
~Q0         
                                                        |
38 | | an4 586 |
. . . . . . 7
        
                                                     
    
                       
                                   |
39 | 37, 38 | sylib 122 |
. . . . . 6
  ~Q0
~Q0         
                    
                                   |
40 | | 3anass 982 |
. . . . . . . 8
                     |
41 | | anass 401 |
. . . . . . . . 9
    
         
                |
42 | | anass 401 |
. . . . . . . . . 10
    
                  |
43 | 42 | anbi2i 457 |
. . . . . . . . 9
       
      
                |
44 | | anidm 396 |
. . . . . . . . . . 11
      
    |
45 | 44 | anbi1i 458 |
. . . . . . . . . 10
    
              |
46 | 45 | anbi2i 457 |
. . . . . . . . 9
       
      
            |
47 | 41, 43, 46 | 3bitr2i 208 |
. . . . . . . 8
    
         
            |
48 | 40, 47 | bitr4i 187 |
. . . . . . 7
            
            |
49 | 48 | anbi1i 458 |
. . . . . 6
    
 
                                                 
    
                       
                                   |
50 | 39, 49 | sylibr 134 |
. . . . 5
  ~Q0
~Q0     
 
                                                    |
51 | | ee8anv 1935 |
. . . . . 6
                      
                 
                                                      |
52 | 51 | anbi2i 457 |
. . . . 5
    
 
                        
                 
          
    
                                                 |
53 | 50, 52 | sylibr 134 |
. . . 4
  ~Q0
~Q0     
 
                        
                 
         |
54 | | 19.42vvvv 1913 |
. . . . . . 7
            
 
                                 
        
             
                 
         |
55 | 54 | 2exbii 1606 |
. . . . . 6
                
    
                       
                
                
                 
         |
56 | 55 | 2exbii 1606 |
. . . . 5
                    
    
                       
                  
 
                              
             |
57 | | 19.42vvvv 1913 |
. . . . 5
                 
             
                 
          
    
                     
                 
         |
58 | 56, 57 | bitri 184 |
. . . 4
                    
    
                       
          
    
                     
                 
         |
59 | 53, 58 | sylibr 134 |
. . 3
  ~Q0
~Q0                     
    
                       
         |
60 | | 3simpb 995 |
. . . . . . . . 9
        
        |
61 | 60 | adantr 276 |
. . . . . . . 8
    
 
                                          |
62 | | simplll 533 |
. . . . . . . . . 10
                    
         
     |
63 | | simprlr 538 |
. . . . . . . . . 10
                    
         
     |
64 | 62, 63 | jca 306 |
. . . . . . . . 9
                    
         
          |
65 | 64 | adantl 277 |
. . . . . . . 8
    
 
                                     
      |
66 | | oveq1 5881 |
. . . . . . . . . . . . . . . 16

  
   |
67 | 63 | adantl 277 |
. . . . . . . . . . . . . . . . . . . . . 22
    
 
                                       |
68 | | simpl3 1002 |
. . . . . . . . . . . . . . . . . . . . . 22
    
 
                                      |
69 | 67, 68 | eqeltrrd 2255 |
. . . . . . . . . . . . . . . . . . . . 21
    
 
                                         |
70 | | opelxp 4656 |
. . . . . . . . . . . . . . . . . . . . 21
          |
71 | 69, 70 | sylib 122 |
. . . . . . . . . . . . . . . . . . . 20
    
 
                                  
   |
72 | 71 | simprd 114 |
. . . . . . . . . . . . . . . . . . 19
    
 
                                    |
73 | | pinn 7307 |
. . . . . . . . . . . . . . . . . . 19
   |
74 | 72, 73 | syl 14 |
. . . . . . . . . . . . . . . . . 18
    
 
                                    |
75 | | nnm0r 6479 |
. . . . . . . . . . . . . . . . . 18
     |
76 | 74, 75 | syl 14 |
. . . . . . . . . . . . . . . . 17
    
 
                                      |
77 | 76 | eqeq2d 2189 |
. . . . . . . . . . . . . . . 16
    
 
                                      
     |
78 | 66, 77 | imbitrid 154 |
. . . . . . . . . . . . . . 15
    
 
                                        |
79 | | simprr 531 |
. . . . . . . . . . . . . . . . . 18
                    
         
      |
80 | | eqtr2 2196 |
. . . . . . . . . . . . . . . . . . . . . 22
    
   
  
     |
81 | | vex 2740 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
82 | | vex 2740 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
83 | 81, 82 | opth 4237 |
. . . . . . . . . . . . . . . . . . . . . 22
       
   |
84 | 80, 83 | sylib 122 |
. . . . . . . . . . . . . . . . . . . . 21
    
   
    |
85 | | oveq1 5881 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
86 | | oveq1 5881 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
87 | 85, 86 | eqeqan12d 2193 |
. . . . . . . . . . . . . . . . . . . . 21
 
             |
88 | 84, 87 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
    
   
    
       |
89 | 88 | ad2ant2lr 510 |
. . . . . . . . . . . . . . . . . . 19
                  
    
       |
90 | 89 | ad2ant2r 509 |
. . . . . . . . . . . . . . . . . 18
                    
         
    
       |
91 | 79, 90 | mpbird 167 |
. . . . . . . . . . . . . . . . 17
                    
         
      |
92 | 91 | eqeq1d 2186 |
. . . . . . . . . . . . . . . 16
                    
         
  
     |
93 | 92 | adantl 277 |
. . . . . . . . . . . . . . 15
    
 
                                    
     |
94 | 78, 93 | sylibd 149 |
. . . . . . . . . . . . . 14
    
 
                                        |
95 | | simpllr 534 |
. . . . . . . . . . . . . . . . . . . 20
                    
         
     |
96 | 95 | adantl 277 |
. . . . . . . . . . . . . . . . . . 19
    
 
                                       |
97 | | simpl2 1001 |
. . . . . . . . . . . . . . . . . . 19
    
 
                                      |
98 | 96, 97 | eqeltrrd 2255 |
. . . . . . . . . . . . . . . . . 18
    
 
                                    
    |
99 | | opelxp 4656 |
. . . . . . . . . . . . . . . . . 18
          |
100 | 98, 99 | sylib 122 |
. . . . . . . . . . . . . . . . 17
    
 
                                  
   |
101 | 100 | simprd 114 |
. . . . . . . . . . . . . . . 16
    
 
                                    |
102 | | pinn 7307 |
. . . . . . . . . . . . . . . 16
   |
103 | 101, 102 | syl 14 |
. . . . . . . . . . . . . . 15
    
 
                                    |
104 | 71 | simpld 112 |
. . . . . . . . . . . . . . 15
    
 
                                    |
105 | | nnm00 6530 |
. . . . . . . . . . . . . . 15
 
         |
106 | 103, 104,
105 | syl2anc 411 |
. . . . . . . . . . . . . 14
    
 
                                    
     |
107 | 94, 106 | sylibd 149 |
. . . . . . . . . . . . 13
    
 
                                        |
108 | | elni2 7312 |
. . . . . . . . . . . . . . . 16

    |
109 | 108 | simprbi 275 |
. . . . . . . . . . . . . . 15
   |
110 | 101, 109 | syl 14 |
. . . . . . . . . . . . . 14
    
 
                                    |
111 | | n0i 3428 |
. . . . . . . . . . . . . 14

  |
112 | | biorf 744 |
. . . . . . . . . . . . . 14
 
     |
113 | 110, 111,
112 | 3syl 17 |
. . . . . . . . . . . . 13
    
 
                                  
     |
114 | 107, 113 | sylibrd 169 |
. . . . . . . . . . . 12
    
 
                                      |
115 | 62 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
    
 
                                       |
116 | | simpl1 1000 |
. . . . . . . . . . . . . . . . . 18
    
 
                                      |
117 | 115, 116 | eqeltrrd 2255 |
. . . . . . . . . . . . . . . . 17
    
 
                                    
    |
118 | | opelxp 4656 |
. . . . . . . . . . . . . . . . 17
          |
119 | 117, 118 | sylib 122 |
. . . . . . . . . . . . . . . 16
    
 
                                  
   |
120 | 119 | simprd 114 |
. . . . . . . . . . . . . . 15
    
 
                                    |
121 | | pinn 7307 |
. . . . . . . . . . . . . . 15
   |
122 | 120, 121 | syl 14 |
. . . . . . . . . . . . . 14
    
 
                                    |
123 | | nnm0 6475 |
. . . . . . . . . . . . . 14
     |
124 | 122, 123 | syl 14 |
. . . . . . . . . . . . 13
    
 
                                      |
125 | | oveq2 5882 |
. . . . . . . . . . . . . 14

      |
126 | 125 | eqeq1d 2186 |
. . . . . . . . . . . . 13

  
     |
127 | 124, 126 | syl5ibrcom 157 |
. . . . . . . . . . . 12
    
 
                                        |
128 | 114, 127 | syld 45 |
. . . . . . . . . . 11
    
 
                                        |
129 | | oveq2 5882 |
. . . . . . . . . . . . . . . 16

      |
130 | 124 | eqeq2d 2189 |
. . . . . . . . . . . . . . . 16
    
 
                                      
     |
131 | 129, 130 | imbitrid 154 |
. . . . . . . . . . . . . . 15
    
 
                                        |
132 | | simprlr 538 |
. . . . . . . . . . . . . . . 16
    
 
                                        |
133 | 132 | eqeq1d 2186 |
. . . . . . . . . . . . . . 15
    
 
                                    
     |
134 | 131, 133 | sylibrd 169 |
. . . . . . . . . . . . . 14
    
 
                                        |
135 | 119 | simpld 112 |
. . . . . . . . . . . . . . 15
    
 
                                    |
136 | | nnm00 6530 |
. . . . . . . . . . . . . . 15
 
         |
137 | 135, 103,
136 | syl2anc 411 |
. . . . . . . . . . . . . 14
    
 
                                    
     |
138 | 134, 137 | sylibd 149 |
. . . . . . . . . . . . 13
    
 
                                        |
139 | | biorf 744 |
. . . . . . . . . . . . . . 15
 
     |
140 | | orcom 728 |
. . . . . . . . . . . . . . 15
  
    |
141 | 139, 140 | bitrdi 196 |
. . . . . . . . . . . . . 14
 
     |
142 | 110, 111,
141 | 3syl 17 |
. . . . . . . . . . . . 13
    
 
                                  
     |
143 | 138, 142 | sylibrd 169 |
. . . . . . . . . . . 12
    
 
                                      |
144 | | oveq1 5881 |
. . . . . . . . . . . . . 14

  
   |
145 | 144 | eqeq1d 2186 |
. . . . . . . . . . . . 13

  
     |
146 | 76, 145 | syl5ibrcom 157 |
. . . . . . . . . . . 12
    
 
                                        |
147 | 143, 146 | syld 45 |
. . . . . . . . . . 11
    
 
                                        |
148 | 128, 147 | jcad 307 |
. . . . . . . . . 10
    
 
                                            |
149 | | eqtr3 2197 |
. . . . . . . . . . 11
             |
150 | 149 | eqcomd 2183 |
. . . . . . . . . 10
             |
151 | 148, 150 | syl6 33 |
. . . . . . . . 9
    
 
                                          |
152 | | simplr 528 |
. . . . . . . . . . . . . . . . 17
                    
         
      |
153 | 91, 152 | oveq12d 5892 |
. . . . . . . . . . . . . . . 16
                    
         
              |
154 | 153 | adantl 277 |
. . . . . . . . . . . . . . 15
    
 
                                                |
155 | 100 | simpld 112 |
. . . . . . . . . . . . . . . . 17
    
 
                                    |
156 | | nnmcl 6481 |
. . . . . . . . . . . . . . . . 17
 
     |
157 | 155, 74, 156 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
    
 
                                      |
158 | | nnmcom 6489 |
. . . . . . . . . . . . . . . . 17
 
       |
159 | 158 | adantl 277 |
. . . . . . . . . . . . . . . 16
       
        
                 
                |
160 | | nnmass 6487 |
. . . . . . . . . . . . . . . . 17
 
           |
161 | 160 | adantl 277 |
. . . . . . . . . . . . . . . 16
       
        
                 
                    |
162 | 157, 135,
103, 159, 161 | caov13d 6057 |
. . . . . . . . . . . . . . 15
    
 
                                                |
163 | | nnmcl 6481 |
. . . . . . . . . . . . . . . . 17
 
     |
164 | 122, 155,
163 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
    
 
                                      |
165 | 161, 103,
104, 164 | caovassd 6033 |
. . . . . . . . . . . . . . 15
    
 
                                                |
166 | 154, 162,
165 | 3eqtr3d 2218 |
. . . . . . . . . . . . . 14
    
 
                                                |
167 | | nnmcl 6481 |
. . . . . . . . . . . . . . . 16
           |
168 | 135, 157,
167 | syl2anc 411 |
. . . . . . . . . . . . . . 15
    
 
                                        |
169 | | nnmcl 6481 |
. . . . . . . . . . . . . . . 16
  
        |
170 | 104, 164,
169 | syl2anc 411 |
. . . . . . . . . . . . . . 15
    
 
                                        |
171 | | nnmcan 6519 |
. . . . . . . . . . . . . . 15
                                     |
172 | 103, 168,
170, 110, 171 | syl31anc 1241 |
. . . . . . . . . . . . . 14
    
 
                                              
           |
173 | 166, 172 | mpbid 147 |
. . . . . . . . . . . . 13
    
 
                                            |
174 | 135, 155,
74, 159, 161 | caov12d 6055 |
. . . . . . . . . . . . 13
    
 
                                            |
175 | 104, 122,
155, 159, 161 | caov13d 6057 |
. . . . . . . . . . . . 13
    
 
                                            |
176 | 173, 174,
175 | 3eqtr3d 2218 |
. . . . . . . . . . . 12
    
 
                                            |
177 | 176 | adantr 276 |
. . . . . . . . . . 11
       
        
                 
       
          |
178 | | nnmcl 6481 |
. . . . . . . . . . . . . 14
 
     |
179 | 135, 74, 178 | syl2anc 411 |
. . . . . . . . . . . . 13
    
 
                                      |
180 | | nnmcl 6481 |
. . . . . . . . . . . . . 14
 
     |
181 | 122, 104,
180 | syl2anc 411 |
. . . . . . . . . . . . 13
    
 
                                      |
182 | 155, 179,
181 | 3jca 1177 |
. . . . . . . . . . . 12
    
 
                                     
    |
183 | | nnmcan 6519 |
. . . . . . . . . . . 12
     
                   |
184 | 182, 183 | sylan 283 |
. . . . . . . . . . 11
       
        
                 
       
        
       |
185 | 177, 184 | mpbid 147 |
. . . . . . . . . 10
       
        
                 
       
      |
186 | 185 | ex 115 |
. . . . . . . . 9
    
 
                                          |
187 | | 0elnn 4618 |
. . . . . . . . . 10
     |
188 | 155, 187 | syl 14 |
. . . . . . . . 9
    
 
                                      |
189 | 151, 186,
188 | mpjaod 718 |
. . . . . . . 8
    
 
                                        |
190 | 61, 65, 189 | jca32 310 |
. . . . . . 7
    
 
                                     
                    |
191 | 190 | 2eximi 1601 |
. . . . . 6
        
 
                                         
           
        |
192 | 191 | exlimivv 1896 |
. . . . 5
            
 
                                         
           
        |
193 | 192 | exlimivv 1896 |
. . . 4
                
    
                       
      
       
           
        |
194 | 193 | 2eximi 1601 |
. . 3
                    
    
                       
      
           
           
        |
195 | 59, 194 | syl 14 |
. 2
  ~Q0
~Q0             
           
        |
196 | | 19.42vvvv 1913 |
. . 3
                        
            
                         |
197 | 5 | anbi1d 465 |
. . . . . . 7
         
           |
198 | 197 | anbi1d 465 |
. . . . . 6
                                 |
199 | 198 | 4exbidv 1870 |
. . . . 5
              
   
    
                         |
200 | 4, 199 | anbi12d 473 |
. . . 4
        
                          
                             |
201 | 27 | anbi2d 464 |
. . . . 5
    
     
      |
202 | 29 | anbi2d 464 |
. . . . . . 7
         
           |
203 | 202 | anbi1d 465 |
. . . . . 6
                                 |
204 | 203 | 4exbidv 1870 |
. . . . 5
              
   
    
                         |
205 | 201, 204 | anbi12d 473 |
. . . 4
        
                          
                             |
206 | | df-enq0 7422 |
. . . 4
~Q0        
                            |
207 | 1, 19, 200, 205, 206 | brab 4272 |
. . 3
 ~Q0    
                            |
208 | 196, 207 | bitr4i 187 |
. 2
                        
      ~Q0   |
209 | 195, 208 | sylib 122 |
1
  ~Q0
~Q0  ~Q0   |