Step | Hyp | Ref
| Expression |
1 | | funfn 5630 |
. . 3

  |
2 | | hashfn 12586 |
. . 3
           |
3 | 1, 2 | sylbi 200 |
. 2

          |
4 | | dmfi 7880 |
. . . . . . . . . . 11
   |
5 | | hashcl 12570 |
. . . . . . . . . . 11
       |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
   
   |
7 | 6 | nn0red 10955 |
. . . . . . . . 9
   
   |
8 | 7 | adantr 471 |
. . . . . . . 8
         |
9 | | df-rel 4860 |
. . . . . . . . . . . . 13

    |
10 | | dfss3 3434 |
. . . . . . . . . . . . 13
  

    |
11 | 9, 10 | bitri 257 |
. . . . . . . . . . . 12
 
    |
12 | 11 | notbii 302 |
. . . . . . . . . . 11



   |
13 | | rexnal 2848 |
. . . . . . . . . . 11
 
 


   |
14 | 12, 13 | bitr4i 260 |
. . . . . . . . . 10


    |
15 | | dmun 5060 |
. . . . . . . . . . . . . . . 16
                 |
16 | 15 | fveq2i 5891 |
. . . . . . . . . . . . . . 15
                         |
17 | | dmsnn0 5320 |
. . . . . . . . . . . . . . . . . . . . 21
  
    |
18 | 17 | biimpri 211 |
. . . . . . . . . . . . . . . . . . . 20
  
    |
19 | 18 | necon1bi 2664 |
. . . . . . . . . . . . . . . . . . 19
       |
20 | 19 | 3ad2ant3 1037 |
. . . . . . . . . . . . . . . . . 18
 
  
 
  |
21 | 20 | uneq2d 3600 |
. . . . . . . . . . . . . . . . 17
 
                   |
22 | | un0 3771 |
. . . . . . . . . . . . . . . . 17
     

    |
23 | 21, 22 | syl6eq 2512 |
. . . . . . . . . . . . . . . 16
 
                 |
24 | 23 | fveq2d 5892 |
. . . . . . . . . . . . . . 15
 
                         |
25 | 16, 24 | syl5eq 2508 |
. . . . . . . . . . . . . 14
 
                         |
26 | | diffi 7829 |
. . . . . . . . . . . . . . . . . . 19
       |
27 | | dmfi 7880 |
. . . . . . . . . . . . . . . . . . 19
           |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 
     |
29 | | hashcl 12570 |
. . . . . . . . . . . . . . . . . 18
        
      |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . . . 17
   
       |
31 | 30 | nn0red 10955 |
. . . . . . . . . . . . . . . 16
   
       |
32 | | hashcl 12570 |
. . . . . . . . . . . . . . . . . 18
               |
33 | 26, 32 | syl 17 |
. . . . . . . . . . . . . . . . 17
           |
34 | 33 | nn0red 10955 |
. . . . . . . . . . . . . . . 16
           |
35 | | peano2re 9832 |
. . . . . . . . . . . . . . . . 17
                     |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . . . 16
             |
37 | | fidomdm 7879 |
. . . . . . . . . . . . . . . . . 18
               |
38 | 26, 37 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
         |
39 | | hashdom 12590 |
. . . . . . . . . . . . . . . . . 18
               
           
           |
40 | 28, 26, 39 | syl2anc 671 |
. . . . . . . . . . . . . . . . 17
                             |
41 | 38, 40 | mpbird 240 |
. . . . . . . . . . . . . . . 16
   
    
          |
42 | 34 | ltp1d 10565 |
. . . . . . . . . . . . . . . 16
                     |
43 | 31, 34, 36, 41, 42 | lelttrd 9819 |
. . . . . . . . . . . . . . 15
   
                 |
44 | 43 | 3ad2ant1 1035 |
. . . . . . . . . . . . . 14
 
      
                |
45 | 25, 44 | eqbrtrd 4437 |
. . . . . . . . . . . . 13
 
                           |
46 | | snfi 7676 |
. . . . . . . . . . . . . . . . 17
 
 |
47 | | incom 3637 |
. . . . . . . . . . . . . . . . . 18
                 |
48 | | disjdif 3851 |
. . . . . . . . . . . . . . . . . 18
         |
49 | 47, 48 | eqtri 2484 |
. . . . . . . . . . . . . . . . 17
         |
50 | | hashun 12593 |
. . . . . . . . . . . . . . . . 17
     
 
                                       |
51 | 46, 49, 50 | mp3an23 1365 |
. . . . . . . . . . . . . . . 16
                                   |
52 | 26, 51 | syl 17 |
. . . . . . . . . . . . . . 15
                               |
53 | | vex 3060 |
. . . . . . . . . . . . . . . . 17
 |
54 | | hashsng 12581 |
. . . . . . . . . . . . . . . . 17
         |
55 | 53, 54 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
       |
56 | 55 | oveq2i 6326 |
. . . . . . . . . . . . . . 15
                           |
57 | 52, 56 | syl6req 2513 |
. . . . . . . . . . . . . 14
                         |
58 | 57 | 3ad2ant1 1035 |
. . . . . . . . . . . . 13
 
                           |
59 | 45, 58 | breqtrd 4441 |
. . . . . . . . . . . 12
 
                             |
60 | | difsnid 4131 |
. . . . . . . . . . . . . . 15
           |
61 | 60 | dmeqd 5056 |
. . . . . . . . . . . . . 14
           |
62 | 61 | fveq2d 5892 |
. . . . . . . . . . . . 13
   
               |
63 | 62 | 3ad2ant2 1036 |
. . . . . . . . . . . 12
 
                     |
64 | 60 | fveq2d 5892 |
. . . . . . . . . . . . 13
                   |
65 | 64 | 3ad2ant2 1036 |
. . . . . . . . . . . 12
 
                     |
66 | 59, 63, 65 | 3brtr3d 4446 |
. . . . . . . . . . 11
 
             |
67 | 66 | rexlimdv3a 2893 |
. . . . . . . . . 10
  
     
       |
68 | 14, 67 | syl5bi 225 |
. . . . . . . . 9
    
        |
69 | 68 | imp 435 |
. . . . . . . 8
      
      |
70 | 8, 69 | gtned 9796 |
. . . . . . 7
             |
71 | 70 | ex 440 |
. . . . . 6
             |
72 | 71 | necon4bd 2656 |
. . . . 5
         
   |
73 | 72 | imp 435 |
. . . 4
             |
74 | | 2nalexn 1711 |
. . . . . . . 8
           
   

  
              |
75 | | df-ne 2635 |
. . . . . . . . . . . . 13

  |
76 | 75 | anbi2i 705 |
. . . . . . . . . . . 12
         

    
   
   |
77 | | annim 431 |
. . . . . . . . . . . 12
         

        
   |
78 | 76, 77 | bitri 257 |
. . . . . . . . . . 11
         

        
   |
79 | 78 | exbii 1729 |
. . . . . . . . . 10
       
   

             |
80 | | exnal 1710 |
. . . . . . . . . 10
      
   

              |
81 | 79, 80 | bitr2i 258 |
. . . . . . . . 9
       
   

              |
82 | 81 | 2exbii 1730 |
. . . . . . . 8
          
   

              
   |
83 | 74, 82 | bitri 257 |
. . . . . . 7
           
   

              
   |
84 | 7 | adantr 471 |
. . . . . . . . . . 11
                   |
85 | | 2re 10707 |
. . . . . . . . . . . . 13
 |
86 | | diffi 7829 |
. . . . . . . . . . . . . . . . 17
              |
87 | | dmfi 7880 |
. . . . . . . . . . . . . . . . 17
            
            |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . . . 16
 
            |
89 | | hashcl 12570 |
. . . . . . . . . . . . . . . 16
               
             |
90 | 88, 89 | syl 17 |
. . . . . . . . . . . . . . 15
   
     
        |
91 | 90 | nn0red 10955 |
. . . . . . . . . . . . . 14
   
     
        |
92 | 91 | adantr 471 |
. . . . . . . . . . . . 13
                
             |
93 | | readdcl 9648 |
. . . . . . . . . . . . 13
                      
              |
94 | 85, 92, 93 | sylancr 674 |
. . . . . . . . . . . 12
                 
              |
95 | | hashcl 12570 |
. . . . . . . . . . . . . 14
       |
96 | 95 | nn0red 10955 |
. . . . . . . . . . . . 13
       |
97 | 96 | adantr 471 |
. . . . . . . . . . . 12
                   |
98 | | 1re 9668 |
. . . . . . . . . . . . . . 15
 |
99 | | readdcl 9648 |
. . . . . . . . . . . . . . 15
                      
              |
100 | 98, 91, 99 | sylancr 674 |
. . . . . . . . . . . . . 14
          
         |
101 | 100 | adantr 471 |
. . . . . . . . . . . . 13
                 
              |
102 | 85, 91, 93 | sylancr 674 |
. . . . . . . . . . . . . 14
          
         |
103 | 102 | adantr 471 |
. . . . . . . . . . . . 13
                 
              |
104 | | dmun 5060 |
. . . . . . . . . . . . . . . . . 18
     
                     
    
            |
105 | | opex 4678 |
. . . . . . . . . . . . . . . . . . . . 21
    |
106 | | opex 4678 |
. . . . . . . . . . . . . . . . . . . . 21
    |
107 | 105, 106 | prss 4139 |
. . . . . . . . . . . . . . . . . . . 20
    
        
      |
108 | | undif 3860 |
. . . . . . . . . . . . . . . . . . . 20
         
                        |
109 | 107, 108 | sylbb 202 |
. . . . . . . . . . . . . . . . . . 19
    
   
                        |
110 | 109 | dmeqd 5056 |
. . . . . . . . . . . . . . . . . 18
    
   
                        |
111 | 104, 110 | syl5reqr 2511 |
. . . . . . . . . . . . . . . . 17
    
   
                        |
112 | | vex 3060 |
. . . . . . . . . . . . . . . . . . . 20
 |
113 | | vex 3060 |
. . . . . . . . . . . . . . . . . . . 20
 |
114 | 112, 113 | dmprop 5330 |
. . . . . . . . . . . . . . . . . . 19
             |
115 | | dfsn2 3993 |
. . . . . . . . . . . . . . . . . . 19
 
    |
116 | 114, 115 | eqtr4i 2487 |
. . . . . . . . . . . . . . . . . 18
            |
117 | 116 | uneq1i 3596 |
. . . . . . . . . . . . . . . . 17
     
    
              
            |
118 | 111, 117 | syl6eq 2512 |
. . . . . . . . . . . . . . . 16
    
   
        
        |
119 | 118 | fveq2d 5892 |
. . . . . . . . . . . . . . 15
    
   
               
         |
120 | 119 | ad2antrl 739 |
. . . . . . . . . . . . . 14
                            
         |
121 | | hashun2 12594 |
. . . . . . . . . . . . . . . . 17
                      
                                     |
122 | 46, 88, 121 | sylancr 674 |
. . . . . . . . . . . . . . . 16
      
                                      |
123 | 55 | oveq1i 6325 |
. . . . . . . . . . . . . . . 16
                                
        |
124 | 122, 123 | syl6breq 4456 |
. . . . . . . . . . . . . . 15
      
                      
         |
125 | 124 | adantr 471 |
. . . . . . . . . . . . . 14
                                    
              |
126 | 120, 125 | eqbrtrd 4437 |
. . . . . . . . . . . . 13
                
    
              |
127 | | 1lt2 10805 |
. . . . . . . . . . . . . . 15
 |
128 | | ltadd1 10109 |
. . . . . . . . . . . . . . . . 17
 
  
     
                 
           
               |
129 | 98, 85, 128 | mp3an12 1363 |
. . . . . . . . . . . . . . . 16
                          
           
               |
130 | 91, 129 | syl 17 |
. . . . . . . . . . . . . . 15
 
    
                     
          |
131 | 127, 130 | mpbii 216 |
. . . . . . . . . . . . . 14
          
           
              |
132 | 131 | adantr 471 |
. . . . . . . . . . . . 13
                 
                     
         |
133 | 84, 101, 103, 126, 132 | lelttrd 9819 |
. . . . . . . . . . . 12
                     
              |
134 | | fidomdm 7879 |
. . . . . . . . . . . . . . . . 17
            
                       |
135 | 86, 134 | syl 17 |
. . . . . . . . . . . . . . . 16
 
                       |
136 | | hashdom 12590 |
. . . . . . . . . . . . . . . . 17
       
    
     
                     
                    
                   |
137 | 88, 86, 136 | syl2anc 671 |
. . . . . . . . . . . . . . . 16
                
                    
                   |
138 | 135, 137 | mpbird 240 |
. . . . . . . . . . . . . . 15
   
     
                       |
139 | | hashcl 12570 |
. . . . . . . . . . . . . . . . . 18
                    
        |
140 | 86, 139 | syl 17 |
. . . . . . . . . . . . . . . . 17
         
        |
141 | 140 | nn0red 10955 |
. . . . . . . . . . . . . . . 16
         
        |
142 | | leadd2 10111 |
. . . . . . . . . . . . . . . . 17
     
                         
     
          
                   
                                |
143 | 85, 142 | mp3an3 1362 |
. . . . . . . . . . . . . . . 16
     
                                    
                         
                                |
144 | 91, 141, 143 | syl2anc 671 |
. . . . . . . . . . . . . . 15
                
                   
                                |
145 | 138, 144 | mpbid 215 |
. . . . . . . . . . . . . 14
          
      
                   |
146 | 145 | adantr 471 |
. . . . . . . . . . . . 13
                 
                               |
147 | | prfi 7872 |
. . . . . . . . . . . . . . . . 17
          |
148 | | disjdif 3851 |
. . . . . . . . . . . . . . . . 17
                       |
149 | | hashun 12593 |
. . . . . . . . . . . . . . . . 17
      
                         
                                                            
         |
150 | 147, 148,
149 | mp3an13 1364 |
. . . . . . . . . . . . . . . 16
                         
                                  
         |
151 | 86, 150 | syl 17 |
. . . . . . . . . . . . . . 15
              
                                  
         |
152 | 151 | adantr 471 |
. . . . . . . . . . . . . 14
                     
                                       
         |
153 | 109 | fveq2d 5892 |
. . . . . . . . . . . . . . 15
    
   
        
                       |
154 | 153 | ad2antrl 739 |
. . . . . . . . . . . . . 14
                     
                       |
155 | 53, 112 | opth 4690 |
. . . . . . . . . . . . . . . . . . 19
           |
156 | 155 | simprbi 470 |
. . . . . . . . . . . . . . . . . 18
         |
157 | 156 | necon3i 2668 |
. . . . . . . . . . . . . . . . 17
         |
158 | | hashprg 12604 |
. . . . . . . . . . . . . . . . . 18
               
                |
159 | 105, 106,
158 | mp2an 683 |
. . . . . . . . . . . . . . . . 17
                      |
160 | 157, 159 | sylib 201 |
. . . . . . . . . . . . . . . 16
                |
161 | 160 | oveq1d 6330 |
. . . . . . . . . . . . . . 15
                                                  |
162 | 161 | ad2antll 740 |
. . . . . . . . . . . . . 14
                     
                                        |
163 | 152, 154,
162 | 3eqtr3rd 2505 |
. . . . . . . . . . . . 13
                                    |
164 | 146, 163 | breqtrd 4441 |
. . . . . . . . . . . 12
                 
                  |
165 | 84, 94, 97, 133, 164 | ltletrd 9821 |
. . . . . . . . . . 11
                       |
166 | 84, 165 | gtned 9796 |
. . . . . . . . . 10
                       |
167 | 166 | ex 440 |
. . . . . . . . 9
                       |
168 | 167 | exlimdv 1790 |
. . . . . . . 8
        
   
            |
169 | 168 | exlimdvv 1791 |
. . . . . . 7
            
   
            |
170 | 83, 169 | syl5bi 225 |
. . . . . 6
            
   
            |
171 | 170 | necon4bd 2656 |
. . . . 5
         
              
    |
172 | 171 | imp 435 |
. . . 4
                         
   |
173 | | dffun4 5613 |
. . . 4
            
   
    |
174 | 73, 172, 173 | sylanbrc 675 |
. . 3
             |
175 | 174 | ex 440 |
. 2
         
   |
176 | 3, 175 | impbid2 209 |
1
             |