Step | Hyp | Ref
| Expression |
1 | | hashbc.4 |
. . . . 5
   |
2 | | hashbc.3 |
. . . . 5
                     |
3 | | oveq2 6316 |
. . . . . . 7
               |
4 | | eqeq2 2482 |
. . . . . . . . 9
     
       |
5 | 4 | rabbidv 3022 |
. . . . . . . 8
        

       |
6 | 5 | fveq2d 5883 |
. . . . . . 7
                         |
7 | 3, 6 | eqeq12d 2486 |
. . . . . 6
                             
         |
8 | 7 | rspcv 3132 |
. . . . 5
  
                
                    |
9 | 1, 2, 8 | sylc 61 |
. . . 4
                    |
10 | | ssun1 3588 |
. . . . . . . . . . . . 13

    |
11 | | sspwb 4649 |
. . . . . . . . . . . . 13
    
        |
12 | 10, 11 | mpbi 213 |
. . . . . . . . . . . 12
       |
13 | 12 | sseli 3414 |
. . . . . . . . . . 11
 
 
     |
14 | 13 | adantl 473 |
. . . . . . . . . 10
 
         |
15 | | hashbc.2 |
. . . . . . . . . . 11
   |
16 | | elpwi 3951 |
. . . . . . . . . . . 12
    |
17 | 16 | ssneld 3420 |
. . . . . . . . . . 11
  
   |
18 | 15, 17 | mpan9 477 |
. . . . . . . . . 10
 
 
  |
19 | 14, 18 | jca 541 |
. . . . . . . . 9
 
    
  
   |
20 | | elpwi 3951 |
. . . . . . . . . . . . . 14
     

     |
21 | | uncom 3569 |
. . . . . . . . . . . . . 14
         |
22 | 20, 21 | syl6sseq 3464 |
. . . . . . . . . . . . 13
     
      |
23 | 22 | adantr 472 |
. . . . . . . . . . . 12
   
  

      |
24 | | simpr 468 |
. . . . . . . . . . . . . 14
   
  
   |
25 | | disjsn 4023 |
. . . . . . . . . . . . . 14
    
  |
26 | 24, 25 | sylibr 217 |
. . . . . . . . . . . . 13
   
  
       |
27 | | disjssun 3826 |
. . . . . . . . . . . . 13
         
   |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . 12
   
  
     
   |
29 | 23, 28 | mpbid 215 |
. . . . . . . . . . 11
   
  

  |
30 | | vex 3034 |
. . . . . . . . . . . 12
 |
31 | 30 | elpw 3948 |
. . . . . . . . . . 11
 
  |
32 | 29, 31 | sylibr 217 |
. . . . . . . . . 10
   
  
    |
33 | 32 | adantl 473 |
. . . . . . . . 9
 
     
     |
34 | 19, 33 | impbida 850 |
. . . . . . . 8
     
  
    |
35 | 34 | anbi1d 719 |
. . . . . . 7
        
   
  
         |
36 | | anass 661 |
. . . . . . 7
    
  
        
   
        |
37 | 35, 36 | syl6bb 269 |
. . . . . 6
        
      
         |
38 | 37 | rabbidva2 3020 |
. . . . 5
  
       
            |
39 | 38 | fveq2d 5883 |
. . . 4
                 
             |
40 | 9, 39 | eqtrd 2505 |
. . 3
            
             |
41 | | peano2zm 11004 |
. . . . . 6
 
   |
42 | 1, 41 | syl 17 |
. . . . 5
     |
43 | | oveq2 6316 |
. . . . . . 7
                   |
44 | | eqeq2 2482 |
. . . . . . . . 9
       
         |
45 | 44 | rabbidv 3022 |
. . . . . . . 8
          

         |
46 | 45 | fveq2d 5883 |
. . . . . . 7
                             |
47 | 43, 46 | eqeq12d 2486 |
. . . . . 6
                          
      
           |
48 | 47 | rspcv 3132 |
. . . . 5
    
                
                        |
49 | 42, 2, 48 | sylc 61 |
. . . 4
                        |
50 | | hashbc.1 |
. . . . . . . 8
   |
51 | | pwfi 7887 |
. . . . . . . 8

   |
52 | 50, 51 | sylib 201 |
. . . . . . 7
    |
53 | | rabexg 4549 |
. . . . . . 7
             |
54 | 52, 53 | syl 17 |
. . . . . 6
  
         |
55 | | snfi 7668 |
. . . . . . . . . 10
   |
56 | | unfi 7856 |
. . . . . . . . . 10
           |
57 | 50, 55, 56 | sylancl 675 |
. . . . . . . . 9
       |
58 | | pwfi 7887 |
. . . . . . . . 9
      
     |
59 | 57, 58 | sylib 201 |
. . . . . . . 8
        |
60 | | ssrab2 3500 |
. . . . . . . 8
            
 
    |
61 | | ssfi 7810 |
. . . . . . . 8
      
            
 
    
 
            |
62 | 59, 60, 61 | sylancl 675 |
. . . . . . 7
   
            |
63 | | elex 3040 |
. . . . . . 7
   
                         |
64 | 62, 63 | syl 17 |
. . . . . 6
   
            |
65 | | fveq2 5879 |
. . . . . . . . 9
           |
66 | 65 | eqeq1d 2473 |
. . . . . . . 8
       
         |
67 | 66 | elrab 3184 |
. . . . . . 7
         
           |
68 | | elpwi 3951 |
. . . . . . . . . . . 12
    |
69 | 68 | ad2antrl 742 |
. . . . . . . . . . 11
 
            |
70 | | unss1 3594 |
. . . . . . . . . . 11
     
     |
71 | 69, 70 | syl 17 |
. . . . . . . . . 10
 
              
     |
72 | | vex 3034 |
. . . . . . . . . . . 12
 |
73 | | snex 4641 |
. . . . . . . . . . . 12
   |
74 | 72, 73 | unex 6608 |
. . . . . . . . . . 11
     |
75 | 74 | elpw 3948 |
. . . . . . . . . 10
      
  
          |
76 | 71, 75 | sylibr 217 |
. . . . . . . . 9
 
                     |
77 | 50 | adantr 472 |
. . . . . . . . . . . . 13
 
         
  |
78 | | ssfi 7810 |
. . . . . . . . . . . . 13
  
  |
79 | 77, 69, 78 | syl2anc 673 |
. . . . . . . . . . . 12
 
         
  |
80 | 55 | a1i 11 |
. . . . . . . . . . . 12
 
              |
81 | 15 | adantr 472 |
. . . . . . . . . . . . . 14
 
         
  |
82 | 69, 81 | ssneldd 3421 |
. . . . . . . . . . . . 13
 
         
  |
83 | | disjsn 4023 |
. . . . . . . . . . . . 13
    
  |
84 | 82, 83 | sylibr 217 |
. . . . . . . . . . . 12
 
                |
85 | | hashun 12599 |
. . . . . . . . . . . 12
        
                      |
86 | 79, 80, 84, 85 | syl3anc 1292 |
. . . . . . . . . . 11
 
                                |
87 | | simprr 774 |
. . . . . . . . . . . 12
 
                  |
88 | | vex 3034 |
. . . . . . . . . . . . . 14
 |
89 | | hashsng 12587 |
. . . . . . . . . . . . . 14
         |
90 | 88, 89 | ax-mp 5 |
. . . . . . . . . . . . 13
       |
91 | 90 | a1i 11 |
. . . . . . . . . . . 12
 
                  |
92 | 87, 91 | oveq12d 6326 |
. . . . . . . . . . 11
 
                            |
93 | 1 | adantr 472 |
. . . . . . . . . . . . 13
 
         
  |
94 | 93 | zcnd 11064 |
. . . . . . . . . . . 12
 
         
  |
95 | | ax-1cn 9615 |
. . . . . . . . . . . 12
 |
96 | | npcan 9904 |
. . . . . . . . . . . 12
 
       |
97 | 94, 95, 96 | sylancl 675 |
. . . . . . . . . . 11
 
                |
98 | 86, 92, 97 | 3eqtrd 2509 |
. . . . . . . . . 10
 
                    |
99 | | ssun2 3589 |
. . . . . . . . . . 11
 
     |
100 | 88 | snss 4087 |
. . . . . . . . . . 11
       
     |
101 | 99, 100 | mpbir 214 |
. . . . . . . . . 10
     |
102 | 98, 101 | jctil 546 |
. . . . . . . . 9
 
                          |
103 | | eleq2 2538 |
. . . . . . . . . . 11
             |
104 | | fveq2 5879 |
. . . . . . . . . . . 12
                   |
105 | 104 | eqeq1d 2473 |
. . . . . . . . . . 11
                     |
106 | 103, 105 | anbi12d 725 |
. . . . . . . . . 10
           
                 |
107 | 106 | elrab 3184 |
. . . . . . . . 9
       
                                     |
108 | 76, 102, 107 | sylanbrc 677 |
. . . . . . . 8
 
                
            |
109 | 108 | ex 441 |
. . . . . . 7
                 
             |
110 | 67, 109 | syl5bi 225 |
. . . . . 6
                               |
111 | | eleq2 2538 |
. . . . . . . . 9
 
   |
112 | | fveq2 5879 |
. . . . . . . . . 10
           |
113 | 112 | eqeq1d 2473 |
. . . . . . . . 9
     
       |
114 | 111, 113 | anbi12d 725 |
. . . . . . . 8
                 |
115 | 114 | elrab 3184 |
. . . . . . 7
                             |
116 | | elpwi 3951 |
. . . . . . . . . . . . 13
     

     |
117 | 116 | ad2antrl 742 |
. . . . . . . . . . . 12
 
                    |
118 | 117, 21 | syl6sseq 3464 |
. . . . . . . . . . 11
 
                    |
119 | | ssundif 3842 |
. . . . . . . . . . 11
           |
120 | 118, 119 | sylib 201 |
. . . . . . . . . 10
 
              
     |
121 | | vex 3034 |
. . . . . . . . . . . 12
 |
122 | | difexg 4545 |
. . . . . . . . . . . 12
 
     |
123 | 121, 122 | ax-mp 5 |
. . . . . . . . . . 11
     |
124 | 123 | elpw 3948 |
. . . . . . . . . 10
            |
125 | 120, 124 | sylibr 217 |
. . . . . . . . 9
 
              
      |
126 | 50 | adantr 472 |
. . . . . . . . . . . . . 14
 
                |
127 | | ssfi 7810 |
. . . . . . . . . . . . . 14
       
     |
128 | 126, 120,
127 | syl2anc 673 |
. . . . . . . . . . . . 13
 
              
     |
129 | | hashcl 12576 |
. . . . . . . . . . . . 13
        
      |
130 | 128, 129 | syl 17 |
. . . . . . . . . . . 12
 
                        |
131 | 130 | nn0cnd 10951 |
. . . . . . . . . . 11
 
                        |
132 | | pncan 9901 |
. . . . . . . . . . 11
     
          
                |
133 | 131, 95, 132 | sylancl 675 |
. . . . . . . . . 10
 
                   
                |
134 | | undif1 3833 |
. . . . . . . . . . . . . 14
             |
135 | | simprrl 782 |
. . . . . . . . . . . . . . . 16
 
                |
136 | 135 | snssd 4108 |
. . . . . . . . . . . . . . 15
 
               
  |
137 | | ssequn2 3598 |
. . . . . . . . . . . . . . 15
         |
138 | 136, 137 | sylib 201 |
. . . . . . . . . . . . . 14
 
                    |
139 | 134, 138 | syl5eq 2517 |
. . . . . . . . . . . . 13
 
                        |
140 | 139 | fveq2d 5883 |
. . . . . . . . . . . 12
 
                                |
141 | 55 | a1i 11 |
. . . . . . . . . . . . . 14
 
                  |
142 | | incom 3616 |
. . . . . . . . . . . . . . . 16
                 |
143 | | disjdif 3830 |
. . . . . . . . . . . . . . . 16
   
     |
144 | 142, 143 | eqtri 2493 |
. . . . . . . . . . . . . . 15
         |
145 | 144 | a1i 11 |
. . . . . . . . . . . . . 14
 
                        |
146 | | hashun 12599 |
. . . . . . . . . . . . . 14
     
 
                         
             |
147 | 128, 141,
145, 146 | syl3anc 1292 |
. . . . . . . . . . . . 13
 
                              
             |
148 | 90 | oveq2i 6319 |
. . . . . . . . . . . . 13
                           |
149 | 147, 148 | syl6eq 2521 |
. . . . . . . . . . . 12
 
                              
       |
150 | | simprrr 783 |
. . . . . . . . . . . 12
 
                    |
151 | 140, 149,
150 | 3eqtr3d 2513 |
. . . . . . . . . . 11
 
                          |
152 | 151 | oveq1d 6323 |
. . . . . . . . . 10
 
                   
          |
153 | 133, 152 | eqtr3d 2507 |
. . . . . . . . 9
 
                          |
154 | | fveq2 5879 |
. . . . . . . . . . 11
                   |
155 | 154 | eqeq1d 2473 |
. . . . . . . . . 10
                         |
156 | 155 | elrab 3184 |
. . . . . . . . 9
                                 |
157 | 125, 153,
156 | sylanbrc 677 |
. . . . . . . 8
 
              
              |
158 | 157 | ex 441 |
. . . . . . 7
              
                |
159 | 115, 158 | syl5bi 225 |
. . . . . 6
    
                          |
160 | 67, 115 | anbi12i 711 |
. . . . . . 7
          
             
                          |
161 | | simp3rl 1103 |
. . . . . . . . . . . 12
 
           
          
  |
162 | 161 | snssd 4108 |
. . . . . . . . . . 11
 
           
          
    |
163 | | incom 3616 |
. . . . . . . . . . . 12
         |
164 | 84 | 3adant3 1050 |
. . . . . . . . . . . 12
 
           
          
      |
165 | 163, 164 | syl5eq 2517 |
. . . . . . . . . . 11
 
           
          
      |
166 | | uneqdifeq 3847 |
. . . . . . . . . . 11
                     |
167 | 162, 165,
166 | syl2anc 673 |
. . . . . . . . . 10
 
           
          
            |
168 | 167 | bicomd 206 |
. . . . . . . . 9
 
           
          
 
          |
169 | | eqcom 2478 |
. . . . . . . . 9
           |
170 | | eqcom 2478 |
. . . . . . . . . 10
           |
171 | | uncom 3569 |
. . . . . . . . . . 11
         |
172 | 171 | eqeq1i 2476 |
. . . . . . . . . 10
           |
173 | 170, 172 | bitri 257 |
. . . . . . . . 9
           |
174 | 168, 169,
173 | 3bitr4g 296 |
. . . . . . . 8
 
           
          
            |
175 | 174 | 3expib 1234 |
. . . . . . 7
              
          
             |
176 | 160, 175 | syl5bi 225 |
. . . . . 6
    
         
          
             |
177 | 54, 64, 110, 159, 176 | en3d 7624 |
. . . . 5
  
                      |
178 | | ssrab2 3500 |
. . . . . . 7
           |
179 | | ssfi 7810 |
. . . . . . 7
    
         

         |
180 | 52, 178, 179 | sylancl 675 |
. . . . . 6
  
         |
181 | | hashen 12568 |
. . . . . 6
   
         
                              
            
                       |
182 | 180, 62, 181 | syl2anc 673 |
. . . . 5
                    
            
                       |
183 | 177, 182 | mpbird 240 |
. . . 4
                   
             |
184 | 49, 183 | eqtrd 2505 |
. . 3
              
             |
185 | 40, 184 | oveq12d 6326 |
. 2
                       
                               |
186 | 55 | a1i 11 |
. . . . . 6
     |
187 | | disjsn 4023 |
. . . . . . 7
    
  |
188 | 15, 187 | sylibr 217 |
. . . . . 6
       |
189 | | hashun 12599 |
. . . . . 6
        
                      |
190 | 50, 186, 188, 189 | syl3anc 1292 |
. . . . 5
    
                  |
191 | 90 | oveq2i 6319 |
. . . . 5
                   |
192 | 190, 191 | syl6eq 2521 |
. . . 4
    
            |
193 | 192 | oveq1d 6323 |
. . 3
     
               |
194 | | hashcl 12576 |
. . . . 5
       |
195 | 50, 194 | syl 17 |
. . . 4
       |
196 | | bcpasc 12544 |
. . . 4
     
                           |
197 | 195, 1, 196 | syl2anc 673 |
. . 3
                           |
198 | 193, 197 | eqtr4d 2508 |
. 2
     
                 
     |
199 | | pm2.1 424 |
. . . . . . . . 9
   |
200 | 199 | biantrur 514 |
. . . . . . . 8
    
          |
201 | | andir 885 |
. . . . . . . 8
        
 
              |
202 | 200, 201 | bitri 257 |
. . . . . . 7
    
                |
203 | 202 | a1i 11 |
. . . . . 6
     
                      |
204 | 203 | rabbiia 3019 |
. . . . 5
             
                   |
205 | | unrab 3705 |
. . . . 5
   
                          
                   |
206 | 204, 205 | eqtr4i 2496 |
. . . 4
                           
            |
207 | 206 | fveq2i 5882 |
. . 3
     
             
 
                          |
208 | | ssrab2 3500 |
. . . . 5
              
    |
209 | | ssfi 7810 |
. . . . 5
      
              
    
 
            |
210 | 59, 208, 209 | sylancl 675 |
. . . 4
   
            |
211 | | inrab 3706 |
. . . . . 6
   
                          
                   |
212 | | simprl 772 |
. . . . . . . . 9
                 |
213 | | simpll 768 |
. . . . . . . . 9
              
  |
214 | 212, 213 | pm2.65i 178 |
. . . . . . . 8
               |
215 | 214 | rgenw 2768 |
. . . . . . 7
      
             |
216 | | rabeq0 3757 |
. . . . . . 7
   
                 
 
                   |
217 | 215, 216 | mpbir 214 |
. . . . . 6
       
              |
218 | 211, 217 | eqtri 2493 |
. . . . 5
   
                         |
219 | 218 | a1i 11 |
. . . 4
                 
             |
220 | | hashun 12599 |
. . . 4
    
            
           
 
                             
 
                               
                               |
221 | 210, 62, 219, 220 | syl3anc 1292 |
. . 3
     
 
                               
                               |
222 | 207, 221 | syl5eq 2517 |
. 2
      
               
                               |
223 | 185, 198,
222 | 3eqtr4d 2515 |
1
     
                      |