Step | Hyp | Ref
| Expression |
1 | | wemapwe.u |
. . . . . . . . 9
   finSupp
  |
2 | | eqid 2462 |
. . . . . . . . 9
   finSupp       
  finSupp        |
3 | | eqid 2462 |
. . . . . . . . 9
           |
4 | | simprr 771 |
. . . . . . . . . . 11
 
  
  |
5 | | wemapwe.2 |
. . . . . . . . . . . 12
   |
6 | 5 | adantr 471 |
. . . . . . . . . . 11
 
  
  |
7 | | wemapwe.5 |
. . . . . . . . . . . 12
OrdIso    |
8 | 7 | oiiso 8083 |
. . . . . . . . . . 11
 

     |
9 | 4, 6, 8 | syl2anc 671 |
. . . . . . . . . 10
 
        |
10 | | isof1o 6246 |
. . . . . . . . . 10

  
      |
11 | 9, 10 | syl 17 |
. . . . . . . . 9
 
         |
12 | | simprl 769 |
. . . . . . . . . . 11
 
  
  |
13 | | wemapwe.3 |
. . . . . . . . . . . 12
   |
14 | 13 | adantr 471 |
. . . . . . . . . . 11
 
  
  |
15 | | wemapwe.6 |
. . . . . . . . . . . 12
OrdIso    |
16 | 15 | oiiso 8083 |
. . . . . . . . . . 11
 

     |
17 | 12, 14, 16 | syl2anc 671 |
. . . . . . . . . 10
 
        |
18 | | isof1o 6246 |
. . . . . . . . . 10

  
      |
19 | | f1ocnv 5853 |
. . . . . . . . . 10
            |
20 | 17, 18, 19 | 3syl 18 |
. . . . . . . . 9
 
          |
21 | 7 | oiexg 8081 |
. . . . . . . . . . 11
   |
22 | 21 | ad2antll 740 |
. . . . . . . . . 10
 
  
  |
23 | | dmexg 6756 |
. . . . . . . . . 10
   |
24 | 22, 23 | syl 17 |
. . . . . . . . 9
 
     |
25 | 15 | oiexg 8081 |
. . . . . . . . . . 11
   |
26 | 25 | ad2antrl 739 |
. . . . . . . . . 10
 
  
  |
27 | | dmexg 6756 |
. . . . . . . . . 10
   |
28 | 26, 27 | syl 17 |
. . . . . . . . 9
 
     |
29 | | wemapwe.7 |
. . . . . . . . . 10
     |
30 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . 15
 
         |
31 | | f1ofo 5848 |
. . . . . . . . . . . . . . 15
           |
32 | | forn 5823 |
. . . . . . . . . . . . . . 15
       |
33 | 30, 31, 32 | 3syl 18 |
. . . . . . . . . . . . . 14
 
     |
34 | | wemapwe.4 |
. . . . . . . . . . . . . . 15
   |
35 | 34 | adantr 471 |
. . . . . . . . . . . . . 14
 
     |
36 | 33, 35 | eqnetrd 2703 |
. . . . . . . . . . . . 13
 
     |
37 | | dm0rn0 5073 |
. . . . . . . . . . . . . 14

  |
38 | 37 | necon3bii 2688 |
. . . . . . . . . . . . 13

  |
39 | 36, 38 | sylibr 217 |
. . . . . . . . . . . 12
 
     |
40 | 15 | oicl 8075 |
. . . . . . . . . . . . 13
 |
41 | | ord0eln0 5500 |
. . . . . . . . . . . . 13


   |
42 | 40, 41 | ax-mp 5 |
. . . . . . . . . . . 12

  |
43 | 39, 42 | sylibr 217 |
. . . . . . . . . . 11
 
  
  |
44 | 15 | oif 8076 |
. . . . . . . . . . . 12
     |
45 | 44 | ffvelrni 6049 |
. . . . . . . . . . 11
       |
46 | 43, 45 | syl 17 |
. . . . . . . . . 10
 
         |
47 | 29, 46 | syl5eqel 2544 |
. . . . . . . . 9
 
  
  |
48 | 1, 2, 3, 11, 20, 4, 12, 24, 28, 47 | mapfien 7952 |
. . . . . . . 8
 
                 finSupp         |
49 | | eqid 2462 |
. . . . . . . . . . 11
   finSupp     finSupp   |
50 | 15 | oion 8082 |
. . . . . . . . . . . 12
   |
51 | 50 | ad2antrl 739 |
. . . . . . . . . . 11
 
     |
52 | 7 | oion 8082 |
. . . . . . . . . . . 12
   |
53 | 52 | ad2antll 740 |
. . . . . . . . . . 11
 
     |
54 | 49, 51, 53 | cantnfdm 8200 |
. . . . . . . . . 10
 
    CNF     finSupp    |
55 | 29 | fveq2i 5895 |
. . . . . . . . . . . . 13
               |
56 | | f1ocnvfv1 6205 |
. . . . . . . . . . . . . 14
      
           |
57 | 30, 43, 56 | syl2anc 671 |
. . . . . . . . . . . . 13
 
              |
58 | 55, 57 | syl5eq 2508 |
. . . . . . . . . . . 12
 
          |
59 | 58 | breq2d 4430 |
. . . . . . . . . . 11
 
    finSupp
     finSupp    |
60 | 59 | rabbidv 3048 |
. . . . . . . . . 10
 
   
  finSupp          finSupp    |
61 | 54, 60 | eqtr4d 2499 |
. . . . . . . . 9
 
    CNF     finSupp         |
62 | | f1oeq3 5834 |
. . . . . . . . 9
  CNF     finSupp                    CNF 

             finSupp          |
63 | 61, 62 | syl 17 |
. . . . . . . 8
 
                CNF 

             finSupp          |
64 | 48, 63 | mpbird 240 |
. . . . . . 7
 
               CNF    |
65 | | eqid 2462 |
. . . . . . . . 9
 CNF
  CNF   |
66 | | eqid 2462 |
. . . . . . . . 9
    
                           
           
              |
67 | 65, 51, 53, 66 | oemapwe 8230 |
. . . . . . . 8
 
        
                         CNF  OrdIso                                CNF
  
    |
68 | 67 | simpld 465 |
. . . . . . 7
 
      
           
              CNF    |
69 | | eqid 2462 |
. . . . . . . 8
                    
                                       
   
            
                                     |
70 | 69 | f1owe 6274 |
. . . . . . 7
   
         CNF 
                               CNF
    
   
            
                                       |
71 | 64, 68, 70 | sylc 62 |
. . . . . 6
 
      
   
            
                                      |
72 | | weinxp 4924 |
. . . . . 6
                    
           
                
            
   
            
                                    
    |
73 | 71, 72 | sylib 201 |
. . . . 5
 
                        
                                    
    |
74 | 11 | adantr 471 |
. . . . . . . . . . . 12
   
  
        |
75 | | f1ofn 5842 |
. . . . . . . . . . . 12
    
  |
76 | | fveq2 5892 |
. . . . . . . . . . . . . . 15
                   |
77 | | fveq2 5892 |
. . . . . . . . . . . . . . 15
                   |
78 | 76, 77 | breq12d 4431 |
. . . . . . . . . . . . . 14
               
                     |
79 | | breq1 4421 |
. . . . . . . . . . . . . . . 16
       
         |
80 | 79 | imbi1d 323 |
. . . . . . . . . . . . . . 15
                        
            |
81 | 80 | ralbidv 2839 |
. . . . . . . . . . . . . 14
      
                                |
82 | 78, 81 | anbi12d 722 |
. . . . . . . . . . . . 13
                    
         
                  

      
             |
83 | 82 | rexrn 6052 |
. . . . . . . . . . . 12
               
                                                       |
84 | 74, 75, 83 | 3syl 18 |
. . . . . . . . . . 11
   
  
   
               
         
                     
      
             |
85 | | f1ofo 5848 |
. . . . . . . . . . . . 13
           |
86 | | forn 5823 |
. . . . . . . . . . . . 13
       |
87 | 74, 85, 86 | 3syl 18 |
. . . . . . . . . . . 12
   
  
    |
88 | 87 | rexeqdv 3006 |
. . . . . . . . . . 11
   
  
   
               
         

           
                |
89 | 26 | adantr 471 |
. . . . . . . . . . . . . . 15
   
  
    |
90 | | cnvexg 6771 |
. . . . . . . . . . . . . . 15
 
  |
91 | 89, 90 | syl 17 |
. . . . . . . . . . . . . 14
   
  
  
  |
92 | | vex 3060 |
. . . . . . . . . . . . . . 15
 |
93 | 22 | adantr 471 |
. . . . . . . . . . . . . . 15
   
  
    |
94 | | coexg 6776 |
. . . . . . . . . . . . . . 15
 
     |
95 | 92, 93, 94 | sylancr 674 |
. . . . . . . . . . . . . 14
   
  
      |
96 | | coexg 6776 |
. . . . . . . . . . . . . 14
  
     
    |
97 | 91, 95, 96 | syl2anc 671 |
. . . . . . . . . . . . 13
   
  
   
     |
98 | | vex 3060 |
. . . . . . . . . . . . . . 15
 |
99 | | coexg 6776 |
. . . . . . . . . . . . . . 15
 
     |
100 | 98, 93, 99 | sylancr 674 |
. . . . . . . . . . . . . 14
   
  
      |
101 | | coexg 6776 |
. . . . . . . . . . . . . 14
  
          |
102 | 91, 100, 101 | syl2anc 671 |
. . . . . . . . . . . . 13
   
  
   
     |
103 | | fveq1 5891 |
. . . . . . . . . . . . . . . . 17
                     |
104 | | fveq1 5891 |
. . . . . . . . . . . . . . . . 17
                     |
105 | | eleq12 2530 |
. . . . . . . . . . . . . . . . 17
        
                            
  
                  |
106 | 103, 104,
105 | syl2an 484 |
. . . . . . . . . . . . . . . 16
        
            
  
                  |
107 | | fveq1 5891 |
. . . . . . . . . . . . . . . . . . 19
                     |
108 | | fveq1 5891 |
. . . . . . . . . . . . . . . . . . 19
                     |
109 | 107, 108 | eqeqan12d 2478 |
. . . . . . . . . . . . . . . . . 18
        
            
  
                  |
110 | 109 | imbi2d 322 |
. . . . . . . . . . . . . . . . 17
        
               
  
                   |
111 | 110 | ralbidv 2839 |
. . . . . . . . . . . . . . . 16
        
     
                                    |
112 | 106, 111 | anbi12d 722 |
. . . . . . . . . . . . . . 15
        
                                             
      
       
           |
113 | 112 | rexbidv 2913 |
. . . . . . . . . . . . . 14
        
     
                       
                   
      
       
           |
114 | 113, 66 | brabga 4732 |
. . . . . . . . . . . . 13
    
                  
           
                  
                   
      
       
           |
115 | 97, 102, 114 | syl2anc 671 |
. . . . . . . . . . . 12
   
  
     
       
                         
                       
      
       
           |
116 | | simprl 769 |
. . . . . . . . . . . . . 14
   
  
    |
117 | | coeq1 5014 |
. . . . . . . . . . . . . . . 16
       |
118 | 117 | coeq2d 5019 |
. . . . . . . . . . . . . . 15
  
          |
119 | | eqid 2462 |
. . . . . . . . . . . . . . 15
               |
120 | 118, 119 | fvmptg 5974 |
. . . . . . . . . . . . . 14
   
                
     |
121 | 116, 97, 120 | syl2anc 671 |
. . . . . . . . . . . . 13
   
  
              
     |
122 | | simprr 771 |
. . . . . . . . . . . . . 14
   
  
    |
123 | | coeq1 5014 |
. . . . . . . . . . . . . . . 16
       |
124 | 123 | coeq2d 5019 |
. . . . . . . . . . . . . . 15
  
          |
125 | 124, 119 | fvmptg 5974 |
. . . . . . . . . . . . . 14
   
                
     |
126 | 122, 102,
125 | syl2anc 671 |
. . . . . . . . . . . . 13
   
  
              
     |
127 | 121, 126 | breq12d 4431 |
. . . . . . . . . . . 12
   
  
                   
                                  
 
                                         |
128 | 17 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . 18
    
 

 
      |
129 | | isocnv 6251 |
. . . . . . . . . . . . . . . . . 18

  
   
   |
130 | 128, 129 | syl 17 |
. . . . . . . . . . . . . . . . 17
    
 

 
        |
131 | | ssrab2 3526 |
. . . . . . . . . . . . . . . . . . . . 21
   finSupp     |
132 | 1, 131 | eqsstri 3474 |
. . . . . . . . . . . . . . . . . . . 20

  |
133 | 132, 116 | sseldi 3442 |
. . . . . . . . . . . . . . . . . . 19
   
  
      |
134 | | elmapi 7524 |
. . . . . . . . . . . . . . . . . . 19
         |
135 | 133, 134 | syl 17 |
. . . . . . . . . . . . . . . . . 18
   
  
        |
136 | 7 | oif 8076 |
. . . . . . . . . . . . . . . . . . 19
     |
137 | 136 | ffvelrni 6049 |
. . . . . . . . . . . . . . . . . 18
       |
138 | | ffvelrn 6048 |
. . . . . . . . . . . . . . . . . 18
                     |
139 | 135, 137,
138 | syl2an 484 |
. . . . . . . . . . . . . . . . 17
    
 

 
           |
140 | 132, 122 | sseldi 3442 |
. . . . . . . . . . . . . . . . . . 19
   
  
      |
141 | | elmapi 7524 |
. . . . . . . . . . . . . . . . . . 19
         |
142 | 140, 141 | syl 17 |
. . . . . . . . . . . . . . . . . 18
   
  
        |
143 | | ffvelrn 6048 |
. . . . . . . . . . . . . . . . . 18
                     |
144 | 142, 137,
143 | syl2an 484 |
. . . . . . . . . . . . . . . . 17
    
 

 
           |
145 | | isorel 6247 |
. . . . . . . . . . . . . . . . 17
  
                                         
                             |
146 | 130, 139,
144, 145 | syl12anc 1274 |
. . . . . . . . . . . . . . . 16
    
 

 
                                                 |
147 | | fvex 5902 |
. . . . . . . . . . . . . . . . 17
              |
148 | 147 | epelc 4769 |
. . . . . . . . . . . . . . . 16
                          
                            |
149 | 146, 148 | syl6bb 269 |
. . . . . . . . . . . . . . 15
    
 

 
                                                 |
150 | 135 | adantr 471 |
. . . . . . . . . . . . . . . . . . 19
    
 

 
       |
151 | | fco 5766 |
. . . . . . . . . . . . . . . . . . 19
                   |
152 | 150, 136,
151 | sylancl 673 |
. . . . . . . . . . . . . . . . . 18
    
 

 
         |
153 | | fvco3 5970 |
. . . . . . . . . . . . . . . . . 18
        
  
                   |
154 | 152, 153 | sylancom 678 |
. . . . . . . . . . . . . . . . 17
    
 

 
                       |
155 | | simpr 467 |
. . . . . . . . . . . . . . . . . . 19
    
 

 
   |
156 | | fvco3 5970 |
. . . . . . . . . . . . . . . . . . 19
      
                |
157 | 136, 155,
156 | sylancr 674 |
. . . . . . . . . . . . . . . . . 18
    
 

 
                 |
158 | 157 | fveq2d 5896 |
. . . . . . . . . . . . . . . . 17
    
 

 
                           |
159 | 154, 158 | eqtrd 2496 |
. . . . . . . . . . . . . . . 16
    
 

 
                         |
160 | 142 | adantr 471 |
. . . . . . . . . . . . . . . . . . 19
    
 

 
       |
161 | | fco 5766 |
. . . . . . . . . . . . . . . . . . 19
                   |
162 | 160, 136,
161 | sylancl 673 |
. . . . . . . . . . . . . . . . . 18
    
 

 
         |
163 | | fvco3 5970 |
. . . . . . . . . . . . . . . . . 18
        
  
                   |
164 | 162, 163 | sylancom 678 |
. . . . . . . . . . . . . . . . 17
    
 

 
                       |
165 | | fvco3 5970 |
. . . . . . . . . . . . . . . . . . 19
      
                |
166 | 136, 155,
165 | sylancr 674 |
. . . . . . . . . . . . . . . . . 18
    
 

 
                 |
167 | 166 | fveq2d 5896 |
. . . . . . . . . . . . . . . . 17
    
 

 
                           |
168 | 164, 167 | eqtrd 2496 |
. . . . . . . . . . . . . . . 16
    
 

 
                         |
169 | 159, 168 | eleq12d 2534 |
. . . . . . . . . . . . . . 15
    
 

 
    
              
                             |
170 | 149, 169 | bitr4d 264 |
. . . . . . . . . . . . . 14
    
 

 
                                         |
171 | 87 | raleqdv 3005 |
. . . . . . . . . . . . . . . . 17
   
  
   
                                     |
172 | | breq2 4422 |
. . . . . . . . . . . . . . . . . . . 20
           
             |
173 | | fveq2 5892 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
174 | | fveq2 5892 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
175 | 173, 174 | eqeq12d 2477 |
. . . . . . . . . . . . . . . . . . . 20
             
                   |
176 | 172, 175 | imbi12d 326 |
. . . . . . . . . . . . . . . . . . 19
                                
                    |
177 | 176 | ralrn 6053 |
. . . . . . . . . . . . . . . . . 18
                   
                                 |
178 | 74, 75, 177 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
   
  
   
                                                  |
179 | 171, 178 | bitr3d 263 |
. . . . . . . . . . . . . . . 16
   
  
   
                                                 |
180 | 179 | adantr 471 |
. . . . . . . . . . . . . . 15
    
 

 
  
      
        
                                 |
181 | | epel 4770 |
. . . . . . . . . . . . . . . . . . 19

  |
182 | 9 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . 20
    
 

          |
183 | | isorel 6247 |
. . . . . . . . . . . . . . . . . . . 20
 
  
                 |
184 | 182, 183 | sylancom 678 |
. . . . . . . . . . . . . . . . . . 19
    
 

     
             |
185 | 181, 184 | syl5bbr 267 |
. . . . . . . . . . . . . . . . . 18
    
 

     
             |
186 | 152 | adantrr 728 |
. . . . . . . . . . . . . . . . . . . . 21
    
 

             |
187 | | simprr 771 |
. . . . . . . . . . . . . . . . . . . . 21
    
 

       |
188 | | fvco3 5970 |
. . . . . . . . . . . . . . . . . . . . 21
        
  
                   |
189 | 186, 187,
188 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . 20
    
 

        
                  |
190 | 162 | adantrr 728 |
. . . . . . . . . . . . . . . . . . . . 21
    
 

             |
191 | | fvco3 5970 |
. . . . . . . . . . . . . . . . . . . . 21
        
  
                   |
192 | 190, 187,
191 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . 20
    
 

                           |
193 | 189, 192 | eqeq12d 2477 |
. . . . . . . . . . . . . . . . . . 19
    
 

                 
                               |
194 | 30 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . 21
    
 

           |
195 | | f1of1 5840 |
. . . . . . . . . . . . . . . . . . . . 21
             |
196 | 194, 19, 195 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
    
 

            |
197 | 186, 187 | ffvelrnd 6051 |
. . . . . . . . . . . . . . . . . . . 20
    
 

             |
198 | 190, 187 | ffvelrnd 6051 |
. . . . . . . . . . . . . . . . . . . 20
    
 

             |
199 | | f1fveq 6193 |
. . . . . . . . . . . . . . . . . . . 20
                                                            |
200 | 196, 197,
198, 199 | syl12anc 1274 |
. . . . . . . . . . . . . . . . . . 19
    
 

                                           |
201 | | fvco3 5970 |
. . . . . . . . . . . . . . . . . . . . 21
      
                |
202 | 136, 187,
201 | sylancr 674 |
. . . . . . . . . . . . . . . . . . . 20
    
 

                     |
203 | | fvco3 5970 |
. . . . . . . . . . . . . . . . . . . . 21
      
                |
204 | 136, 187,
203 | sylancr 674 |
. . . . . . . . . . . . . . . . . . . 20
    
 

                     |
205 | 202, 204 | eqeq12d 2477 |
. . . . . . . . . . . . . . . . . . 19
    
 

                 
                   |
206 | 193, 200,
205 | 3bitrd 287 |
. . . . . . . . . . . . . . . . . 18
    
 

                 
                         |
207 | 185, 206 | imbi12d 326 |
. . . . . . . . . . . . . . . . 17
    
 

                         
                               |
208 | 207 | anassrs 658 |
. . . . . . . . . . . . . . . 16
       

 
 
             
                 
                    |
209 | 208 | ralbidva 2836 |
. . . . . . . . . . . . . . 15
    
 

 
        
       
                                        |
210 | 180, 209 | bitr4d 264 |
. . . . . . . . . . . . . 14
    
 

 
  
      
        
      
       
          |
211 | 170, 210 | anbi12d 722 |
. . . . . . . . . . . . 13
    
 

 
                     
      
         
    
       
            
       
           |
212 | 211 | rexbidva 2910 |
. . . . . . . . . . . 12
   
  
   
                                                          
      
       
           |
213 | 115, 127,
212 | 3bitr4rd 294 |
. . . . . . . . . . 11
   
  
   
                                                     
           
                
          |
214 | 84, 88, 213 | 3bitr3d 291 |
. . . . . . . . . 10
   
  
   
              
         
   
            
                                      |
215 | 214 | ex 440 |
. . . . . . . . 9
 
       
              
         
   
            
                                       |
216 | 215 | pm5.32rd 650 |
. . . . . . . 8
 
     
           
               
                 
                                   
     |
217 | 216 | opabbidv 4482 |
. . . . . . 7
 
      
 
                                                  
                                   
     |
218 | | wemapwe.t |
. . . . . . . . 9
   

           
               |
219 | | df-xp 4862 |
. . . . . . . . 9
     

   |
220 | 218, 219 | ineq12i 3644 |
. . . . . . . 8
         
                                   |
221 | | inopab 4987 |
. . . . . . . 8
                    
                                       
          
    |
222 | 220, 221 | eqtri 2484 |
. . . . . . 7
       
 
                              |
223 | 219 | ineq2i 3643 |
. . . . . . . 8
                    
           
                
                                
                                             |
224 | | inopab 4987 |
. . . . . . . 8
                    
           
                
                                     
                                   
    |
225 | 223, 224 | eqtri 2484 |
. . . . . . 7
                    
           
                
                                
                                   
    |
226 | 217, 222,
225 | 3eqtr4g 2521 |
. . . . . 6
 
                            
                                    
    |
227 | | weeq1 4844 |
. . . . . 6
                          
                                    
      
                    
           
                
              |
228 | 226, 227 | syl 17 |
. . . . 5
 
     
      
   
            
                                    
     |
229 | 73, 228 | mpbird 240 |
. . . 4
 
         |
230 | | weinxp 4924 |
. . . 4

      |
231 | 229, 230 | sylibr 217 |
. . 3
 
  
  |
232 | 231 | ex 440 |
. 2
  

   |
233 | | we0 4851 |
. . 3
 |
234 | | elmapex 7523 |
. . . . . . . . 9
   
   |
235 | 234 | con3i 142 |
. . . . . . . 8
       |
236 | 235 | pm2.21d 110 |
. . . . . . 7
     
finSupp    |
237 | 236 | ralrimiv 2812 |
. . . . . 6
      finSupp
  |
238 | | rabeq0 3766 |
. . . . . 6
    finSupp  
  finSupp   |
239 | 237, 238 | sylibr 217 |
. . . . 5
      finSupp
   |
240 | 1, 239 | syl5eq 2508 |
. . . 4
     |
241 | | weeq2 4845 |
. . . 4


   |
242 | 240, 241 | syl 17 |
. . 3
       |
243 | 233, 242 | mpbiri 241 |
. 2
     |
244 | 232, 243 | pm2.61d1 164 |
1
   |