Proof of Theorem hasheuni
Step | Hyp | Ref
| Expression |
1 | | nfdisj1 4379 |
. . . . . . . 8
 Disj  |
2 | | nfv 1769 |
. . . . . . . 8

 |
3 | | nfv 1769 |
. . . . . . . 8
  |
4 | 1, 2, 3 | nf3an 2033 |
. . . . . . 7
  Disj
  |
5 | | simp2 1031 |
. . . . . . 7
 Disj
   |
6 | | simp3 1032 |
. . . . . . 7
 Disj

  |
7 | | simp1 1030 |
. . . . . . 7
 Disj
 Disj
  |
8 | 4, 5, 6, 7 | hashunif 28454 |
. . . . . 6
 Disj
             |
9 | | simpl 464 |
. . . . . . . 8
  
  |
10 | | dfss3 3408 |
. . . . . . . . . . 11


  |
11 | | hashcl 12576 |
. . . . . . . . . . . . 13
       |
12 | | nn0re 10902 |
. . . . . . . . . . . . . 14
    
      |
13 | | nn0ge0 10919 |
. . . . . . . . . . . . . 14
    
      |
14 | | elrege0 11764 |
. . . . . . . . . . . . . 14
                    |
15 | 12, 13, 14 | sylanbrc 677 |
. . . . . . . . . . . . 13
    
         |
16 | 11, 15 | syl 17 |
. . . . . . . . . . . 12
          |
17 | 16 | ralimi 2796 |
. . . . . . . . . . 11
 

         |
18 | 10, 17 | sylbi 200 |
. . . . . . . . . 10


         |
19 | 18 | r19.21bi 2776 |
. . . . . . . . 9
 
          |
20 | 19 | adantll 728 |
. . . . . . . 8
  


         |
21 | 9, 20 | esumpfinval 28970 |
. . . . . . 7
   Σ*      
      |
22 | 21 | 3adant1 1048 |
. . . . . 6
 Disj
 Σ*             |
23 | 8, 22 | eqtr4d 2508 |
. . . . 5
 Disj
      Σ*        |
24 | 23 | 3adant1l 1284 |
. . . 4
   Disj 
      Σ*        |
25 | 24 | 3expa 1231 |
. . 3
   
Disj         Σ*        |
26 | | uniexg 6607 |
. . . . . . . 8
    |
27 | 10 | notbii 303 |
. . . . . . . . . 10


  |
28 | | rexnal 2836 |
. . . . . . . . . 10
 

  |
29 | 27, 28 | bitr4i 260 |
. . . . . . . . 9


  |
30 | | elssuni 4219 |
. . . . . . . . . . 11
    |
31 | | ssfi 7810 |
. . . . . . . . . . . . 13
  
    |
32 | 31 | expcom 442 |
. . . . . . . . . . . 12
   
   |
33 | 32 | con3d 140 |
. . . . . . . . . . 11
  
    |
34 | 30, 33 | syl 17 |
. . . . . . . . . 10
 
    |
35 | 34 | rexlimiv 2867 |
. . . . . . . . 9
 
   |
36 | 29, 35 | sylbi 200 |
. . . . . . . 8

   |
37 | | hashinf 12558 |
. . . . . . . 8
            |
38 | 26, 36, 37 | syl2an 485 |
. . . . . . 7
 
        |
39 | | vex 3034 |
. . . . . . . . . . 11
 |
40 | | hashinf 12558 |
. . . . . . . . . . 11
 
       |
41 | 39, 40 | mpan 684 |
. . . . . . . . . 10
       |
42 | 41 | reximi 2852 |
. . . . . . . . 9
 

      |
43 | 29, 42 | sylbi 200 |
. . . . . . . 8


      |
44 | | nfv 1769 |
. . . . . . . . . 10

 |
45 | | nfre1 2846 |
. . . . . . . . . 10
  
     |
46 | 44, 45 | nfan 2031 |
. . . . . . . . 9
          |
47 | | simpl 464 |
. . . . . . . . 9
          |
48 | | hashf2 28979 |
. . . . . . . . . . 11
        |
49 | | ffvelrn 6035 |
. . . . . . . . . . 11
        
          |
50 | 48, 39, 49 | mp2an 686 |
. . . . . . . . . 10
        |
51 | 50 | a1i 11 |
. . . . . . . . 9
        
          |
52 | | simpr 468 |
. . . . . . . . 9
        
      |
53 | 46, 47, 51, 52 | esumpinfval 28968 |
. . . . . . . 8
       
Σ*
       |
54 | 43, 53 | sylan2 482 |
. . . . . . 7
 
 Σ*        |
55 | 38, 54 | eqtr4d 2508 |
. . . . . 6
 
      Σ*        |
56 | 55 | 3adant2 1049 |
. . . . 5
 
     
Σ*
       |
57 | 56 | 3adant1r 1285 |
. . . 4
   Disj 
      Σ*        |
58 | 57 | 3expa 1231 |
. . 3
   
Disj        
Σ*
       |
59 | 25, 58 | pm2.61dan 808 |
. 2
   Disj        Σ*        |
60 | | pwfi 7887 |
. . . . . . 7
 
    |
61 | | pwuni 4631 |
. . . . . . . 8
   |
62 | | ssfi 7810 |
. . . . . . . 8
   
     |
63 | 61, 62 | mpan2 685 |
. . . . . . 7
     |
64 | 60, 63 | sylbi 200 |
. . . . . 6
 
  |
65 | 64 | con3i 142 |
. . . . 5
    |
66 | 26, 65, 37 | syl2an 485 |
. . . 4
 
        |
67 | | nftru 1685 |
. . . . . . . . 9
  |
68 | | unrab 3705 |
. . . . . . . . . . 11
              
            |
69 | | exmid 422 |
. . . . . . . . . . . . 13
           |
70 | 69 | rgenw 2768 |
. . . . . . . . . . . 12

           |
71 | | rabid2 2954 |
. . . . . . . . . . . 12
             
            |
72 | 70, 71 | mpbir 214 |
. . . . . . . . . . 11
             |
73 | 68, 72 | eqtr4i 2496 |
. . . . . . . . . 10
               |
74 | 73 | a1i 11 |
. . . . . . . . 9
       
        |
75 | 67, 74 | esumeq1d 28930 |
. . . . . . . 8
Σ*
                  
Σ*
       |
76 | 75 | trud 1461 |
. . . . . . 7
Σ*
 
                 Σ*
      |
77 | | nfrab1 2957 |
. . . . . . . 8
  
      |
78 | | nfrab1 2957 |
. . . . . . . 8
  
      |
79 | | rabexg 4549 |
. . . . . . . 8
 
       |
80 | | rabexg 4549 |
. . . . . . . 8
 
       |
81 | | rabnc 3759 |
. . . . . . . . 9
               |
82 | 81 | a1i 11 |
. . . . . . . 8
  
              |
83 | 50 | a1i 11 |
. . . . . . . 8
 

               |
84 | 50 | a1i 11 |
. . . . . . . 8
 

               |
85 | 44, 77, 78, 79, 80, 82, 83, 84 | esumsplit 28948 |
. . . . . . 7

Σ*
 
                 Σ* 
           Σ*              |
86 | 76, 85 | syl5eqr 2519 |
. . . . . 6

Σ*
     Σ* 
           Σ*              |
87 | 86 | adantr 472 |
. . . . 5
 
 Σ*      Σ* 
           Σ*              |
88 | | nfv 1769 |
. . . . . . 7
     |
89 | 80 | adantr 472 |
. . . . . . 7
 
         |
90 | | simpr 468 |
. . . . . . . . 9
 

  |
91 | | dfrab3 3709 |
. . . . . . . . . . . 12

              |
92 | | hasheq0 12582 |
. . . . . . . . . . . . . . . 16
     
   |
93 | 39, 92 | ax-mp 5 |
. . . . . . . . . . . . . . 15
    
  |
94 | 93 | abbii 2587 |
. . . . . . . . . . . . . 14
         |
95 | | df-sn 3960 |
. . . . . . . . . . . . . 14
     |
96 | 94, 95 | eqtr4i 2496 |
. . . . . . . . . . . . 13
         |
97 | 96 | ineq2i 3622 |
. . . . . . . . . . . 12
             |
98 | 91, 97 | eqtri 2493 |
. . . . . . . . . . 11

          |
99 | | snfi 7668 |
. . . . . . . . . . . 12
   |
100 | | inss2 3644 |
. . . . . . . . . . . 12
       |
101 | | ssfi 7810 |
. . . . . . . . . . . 12
          
      |
102 | 99, 100, 101 | mp2an 686 |
. . . . . . . . . . 11
     |
103 | 98, 102 | eqeltri 2545 |
. . . . . . . . . 10

      |
104 | 103 | a1i 11 |
. . . . . . . . 9
 
         |
105 | | difinf 7859 |
. . . . . . . . 9
                   |
106 | 90, 104, 105 | syl2anc 673 |
. . . . . . . 8
 

          |
107 | | notrab 3711 |
. . . . . . . . 9
               |
108 | 107 | eleq1i 2540 |
. . . . . . . 8
  
              |
109 | 106, 108 | sylnib 311 |
. . . . . . 7
 


       |
110 | 50 | a1i 11 |
. . . . . . 7
          
         |
111 | 39 | a1i 11 |
. . . . . . . 8
          
  |
112 | | simpr 468 |
. . . . . . . . . . 11
          
        |
113 | | rabid 2953 |
. . . . . . . . . . 11
      

       |
114 | 112, 113 | sylib 201 |
. . . . . . . . . 10
          

       |
115 | 114 | simprd 470 |
. . . . . . . . 9
          
      |
116 | 93 | biimpri 211 |
. . . . . . . . . 10

      |
117 | 116 | necon3bi 2669 |
. . . . . . . . 9
       |
118 | 115, 117 | syl 17 |
. . . . . . . 8
          
  |
119 | | hashge1 12606 |
. . . . . . . 8
         |
120 | 111, 118,
119 | syl2anc 673 |
. . . . . . 7
          
      |
121 | | 1re 9660 |
. . . . . . . . 9
 |
122 | 121 | rexri 9711 |
. . . . . . . 8
 |
123 | 122 | a1i 11 |
. . . . . . 7
 
   |
124 | | 0lt1 10157 |
. . . . . . . 8
 |
125 | 124 | a1i 11 |
. . . . . . 7
 
   |
126 | 88, 78, 89, 109, 110, 120, 123, 125 | esumpinfsum 28972 |
. . . . . 6
 
 Σ* 
           |
127 | 126 | oveq2d 6324 |
. . . . 5
 
 Σ* 
           Σ*            Σ*                |
128 | | iccssxr 11742 |
. . . . . . 7
    |
129 | 79 | adantr 472 |
. . . . . . . 8
 
         |
130 | 50 | a1i 11 |
. . . . . . . . 9
                    |
131 | 130 | ralrimiva 2809 |
. . . . . . . 8
 
                 |
132 | 77 | esumcl 28925 |
. . . . . . . 8
        

            
Σ*

              |
133 | 129, 131,
132 | syl2anc 673 |
. . . . . . 7
 
 Σ* 
              |
134 | 128, 133 | sseldi 3416 |
. . . . . 6
 
 Σ* 
           |
135 | | xrge0neqmnf 11762 |
. . . . . . 7
Σ*              Σ*             |
136 | 133, 135 | syl 17 |
. . . . . 6
 
 Σ* 
           |
137 | | xaddpnf1 11542 |
. . . . . 6
 Σ*          
Σ*

          Σ* 
           
  |
138 | 134, 136,
137 | syl2anc 673 |
. . . . 5
 
 Σ* 
           
  |
139 | 87, 127, 138 | 3eqtrd 2509 |
. . . 4
 
 Σ*        |
140 | 66, 139 | eqtr4d 2508 |
. . 3
 
      Σ*        |
141 | 140 | adantlr 729 |
. 2
   Disj        Σ*        |
142 | 59, 141 | pm2.61dan 808 |
1
  Disj       Σ*        |