Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . 3
   |
2 | | iftrue 3878 |
. . . . . . . . 9
  
      
      |
3 | 2 | adantl 473 |
. . . . . . . 8
 
  
      
      |
4 | | isomenndlem.f |
. . . . . . . . . . 11
       |
5 | | f1of 5828 |
. . . . . . . . . . 11
    
      |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
       |
7 | | ssun1 3588 |
. . . . . . . . . . 11

    |
8 | 7 | a1i 11 |
. . . . . . . . . 10

      |
9 | 6, 8 | fssd 5750 |
. . . . . . . . 9
           |
10 | 9 | ffvelrnda 6037 |
. . . . . . . 8
 
           |
11 | 3, 10 | eqeltrd 2549 |
. . . . . . 7
 
  
      
      |
12 | 11 | adantlr 729 |
. . . . . 6
      
      
      |
13 | | iffalse 3881 |
. . . . . . . . 9
         
  |
14 | 13 | adantl 473 |
. . . . . . . 8
 
  
      
  |
15 | | 0ex 4528 |
. . . . . . . . . . 11
 |
16 | 15 | snid 3988 |
. . . . . . . . . 10
   |
17 | | elun2 3593 |
. . . . . . . . . 10
         |
18 | 16, 17 | ax-mp 5 |
. . . . . . . . 9
     |
19 | 18 | a1i 11 |
. . . . . . . 8
 
       |
20 | 14, 19 | eqeltrd 2549 |
. . . . . . 7
 
  
      
      |
21 | 20 | adantlr 729 |
. . . . . 6
   
         

     |
22 | 12, 21 | pm2.61dan 808 |
. . . . 5
 

               |
23 | | isomenndlem.a |
. . . . 5
            |
24 | 22, 23 | fmptd 6061 |
. . . 4
           |
25 | | isomenndlem.y |
. . . . 5

   |
26 | | 0elpw 4570 |
. . . . . . 7
  |
27 | | snssi 4107 |
. . . . . . 7
       |
28 | 26, 27 | ax-mp 5 |
. . . . . 6
    |
29 | 28 | a1i 11 |
. . . . 5
      |
30 | 25, 29 | unssd 3601 |
. . . 4
        |
31 | 24, 30 | fssd 5750 |
. . 3
        |
32 | | nnex 10637 |
. . . . . 6
 |
33 | 32 | mptex 6152 |
. . . . 5
            |
34 | 23, 33 | eqeltri 2545 |
. . . 4
 |
35 | | feq1 5720 |
. . . . . 6
               |
36 | 35 | anbi2d 718 |
. . . . 5
  
      
         |
37 | | fveq1 5878 |
. . . . . . . 8
           |
38 | 37 | iuneq2d 4296 |
. . . . . . 7
      
      |
39 | 38 | fveq2d 5883 |
. . . . . 6
                     |
40 | | simpl 464 |
. . . . . . . . . 10
 
   |
41 | 40 | fveq1d 5881 |
. . . . . . . . 9
 
           |
42 | 41 | fveq2d 5883 |
. . . . . . . 8
 
                   |
43 | 42 | mpteq2dva 4482 |
. . . . . . 7
                       |
44 | 43 | fveq2d 5883 |
. . . . . 6
 Σ^            Σ^              |
45 | 39, 44 | breq12d 4408 |
. . . . 5
           Σ^           
        
Σ^               |
46 | 36, 45 | imbi12d 327 |
. . . 4
         
         Σ^            
                 Σ^                |
47 | | isomenndlem.subadd |
. . . 4
 
               Σ^              |
48 | 34, 46, 47 | vtocl 3086 |
. . 3
 
               Σ^              |
49 | 1, 31, 48 | syl2anc 673 |
. 2
          Σ^              |
50 | 6 | ad2antrr 740 |
. . . . . . . . . . 11
           |
51 | | simpr 468 |
. . . . . . . . . . . . 13
 
   |
52 | | id 22 |
. . . . . . . . . . . . . . 15
   |
53 | 52 | eqcomd 2477 |
. . . . . . . . . . . . . 14
   |
54 | 53 | adantr 472 |
. . . . . . . . . . . . 13
 
   |
55 | 51, 54 | eleqtrd 2551 |
. . . . . . . . . . . 12
 
   |
56 | 55 | adantll 728 |
. . . . . . . . . . 11
       |
57 | 50, 56 | ffvelrnd 6038 |
. . . . . . . . . 10
           |
58 | | eqid 2471 |
. . . . . . . . . 10
             |
59 | 57, 58 | fmptd 6061 |
. . . . . . . . 9
 

            |
60 | 23 | a1i 11 |
. . . . . . . . . . . 12
              |
61 | 55 | iftrued 3880 |
. . . . . . . . . . . . 13
 
         
      |
62 | 61 | mpteq2dva 4482 |
. . . . . . . . . . . 12
                    |
63 | 60, 62 | eqtrd 2505 |
. . . . . . . . . . 11
         |
64 | 63 | feq1d 5724 |
. . . . . . . . . 10
     
             |
65 | 64 | adantl 473 |
. . . . . . . . 9
 

    
             |
66 | 59, 65 | mpbird 240 |
. . . . . . . 8
 

      |
67 | | f1ofo 5835 |
. . . . . . . . . . . . . . . 16
    
      |
68 | 4, 67 | syl 17 |
. . . . . . . . . . . . . . 15
       |
69 | | dffo3 6052 |
. . . . . . . . . . . . . . 15
    
     

       |
70 | 68, 69 | sylib 201 |
. . . . . . . . . . . . . 14
               |
71 | 70 | simprd 470 |
. . . . . . . . . . . . 13
  
      |
72 | 71 | adantr 472 |
. . . . . . . . . . . 12
 
 

      |
73 | | simpr 468 |
. . . . . . . . . . . 12
 
   |
74 | | rspa 2774 |
. . . . . . . . . . . 12
   
     
      |
75 | 72, 73, 74 | syl2anc 673 |
. . . . . . . . . . 11
 
 
      |
76 | 75 | adantlr 729 |
. . . . . . . . . 10
     
      |
77 | | nfv 1769 |
. . . . . . . . . . . 12
  
  |
78 | | nfre1 2846 |
. . . . . . . . . . . 12
  
     |
79 | | simpr 468 |
. . . . . . . . . . . . . . . . 17
 
   |
80 | | simpl 464 |
. . . . . . . . . . . . . . . . 17
 
   |
81 | 79, 80 | eleqtrd 2551 |
. . . . . . . . . . . . . . . 16
 
   |
82 | 81 | adantll 728 |
. . . . . . . . . . . . . . 15
       |
83 | 82 | 3adant3 1050 |
. . . . . . . . . . . . . 14
   
    
  |
84 | 60 | fveq1d 5881 |
. . . . . . . . . . . . . . . . 17
                      |
85 | 84 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . 16
 
                          |
86 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . . . 21
     |
87 | 86, 15 | ifex 3940 |
. . . . . . . . . . . . . . . . . . . 20
          |
88 | 87 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
 
         
  |
89 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . 20
                       |
90 | 89 | fvmpt2 5972 |
. . . . . . . . . . . . . . . . . . 19
          
                           |
91 | 81, 88, 90 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
 
                           |
92 | 2 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
 
         
      |
93 | 91, 92 | eqtrd 2505 |
. . . . . . . . . . . . . . . . 17
 
                      |
94 | 93 | 3adant3 1050 |
. . . . . . . . . . . . . . . 16
 
                          |
95 | | id 22 |
. . . . . . . . . . . . . . . . . 18
           |
96 | 95 | eqcomd 2477 |
. . . . . . . . . . . . . . . . 17
           |
97 | 96 | 3ad2ant3 1053 |
. . . . . . . . . . . . . . . 16
 
           |
98 | 85, 94, 97 | 3eqtrrd 2510 |
. . . . . . . . . . . . . . 15
 
           |
99 | 98 | 3adant1l 1284 |
. . . . . . . . . . . . . 14
   
           |
100 | | rspe 2844 |
. . . . . . . . . . . . . 14
 
     
      |
101 | 83, 99, 100 | syl2anc 673 |
. . . . . . . . . . . . 13
   
     
      |
102 | 101 | 3exp 1230 |
. . . . . . . . . . . 12
 

      
        |
103 | 77, 78, 102 | rexlimd 2866 |
. . . . . . . . . . 11
 

              |
104 | 103 | adantr 472 |
. . . . . . . . . 10
      
            |
105 | 76, 104 | mpd 15 |
. . . . . . . . 9
            |
106 | 105 | ralrimiva 2809 |
. . . . . . . 8
 


       |
107 | 66, 106 | jca 541 |
. . . . . . 7
 

      
       |
108 | | dffo3 6052 |
. . . . . . 7
    
     

       |
109 | 107, 108 | sylibr 217 |
. . . . . 6
 

      |
110 | | founiiun 37517 |
. . . . . 6
     

      |
111 | 109, 110 | syl 17 |
. . . . 5
 

        |
112 | | uniun 4209 |
. . . . . . . 8
 
          |
113 | 15 | unisn 4205 |
. . . . . . . . 9
    |
114 | 113 | uneq2i 3576 |
. . . . . . . 8
 
     
  |
115 | | un0 3762 |
. . . . . . . 8
 
   |
116 | 112, 114,
115 | 3eqtrri 2498 |
. . . . . . 7
       |
117 | 116 | a1i 11 |
. . . . . 6
 
         |
118 | 24 | adantr 472 |
. . . . . . . . 9
 
           |
119 | | isomenndlem.b |
. . . . . . . . . . . . . . . . . 18

  |
120 | 119 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 
   |
121 | 52 | necon3bi 2669 |
. . . . . . . . . . . . . . . . . 18
   |
122 | 121 | adantl 473 |
. . . . . . . . . . . . . . . . 17
 
   |
123 | 120, 122 | jca 541 |
. . . . . . . . . . . . . . . 16
 
     |
124 | | df-pss 3406 |
. . . . . . . . . . . . . . . 16

    |
125 | 123, 124 | sylibr 217 |
. . . . . . . . . . . . . . 15
 
   |
126 | | pssnel 3829 |
. . . . . . . . . . . . . . 15

      |
127 | 125, 126 | syl 17 |
. . . . . . . . . . . . . 14
 
       |
128 | 127 | adantr 472 |
. . . . . . . . . . . . 13
  

       |
129 | | nfv 1769 |
. . . . . . . . . . . . . 14
   
   |
130 | | simprl 772 |
. . . . . . . . . . . . . . . . 17
    
    |
131 | | simprl 772 |
. . . . . . . . . . . . . . . . . . . 20
 
  
  |
132 | 87 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
 
           
  |
133 | 23 | fvmpt2 5972 |
. . . . . . . . . . . . . . . . . . . 20
          
                |
134 | 131, 132,
133 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . 19
 
                  |
135 | 134 | adantlr 729 |
. . . . . . . . . . . . . . . . . 18
    
                 |
136 | 13 | ad2antll 743 |
. . . . . . . . . . . . . . . . . 18
    
   
      
  |
137 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20

  |
138 | 137 | eqcomd 2477 |
. . . . . . . . . . . . . . . . . . 19

  |
139 | 138 | ad2antlr 741 |
. . . . . . . . . . . . . . . . . 18
    
    |
140 | 135, 136,
139 | 3eqtrrd 2510 |
. . . . . . . . . . . . . . . . 17
    
        |
141 | 130, 140,
100 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
    
         |
142 | 141 | ex 441 |
. . . . . . . . . . . . . . 15
 

 

        |
143 | 142 | adantlr 729 |
. . . . . . . . . . . . . 14
  

            |
144 | 129, 78, 143 | exlimd 2017 |
. . . . . . . . . . . . 13
  

    

        |
145 | 128, 144 | mpd 15 |
. . . . . . . . . . . 12
  

 
      |
146 | 145 | adantlr 729 |
. . . . . . . . . . 11
   
              |
147 | | simplll 776 |
. . . . . . . . . . . 12
   
     
   |
148 | | simpl 464 |
. . . . . . . . . . . . . 14
      
      |
149 | | elsni 3985 |
. . . . . . . . . . . . . . . 16
     |
150 | 149 | con3i 142 |
. . . . . . . . . . . . . . 15

    |
151 | 150 | adantl 473 |
. . . . . . . . . . . . . 14
      
    |
152 | | elunnel2 37423 |
. . . . . . . . . . . . . 14
           |
153 | 148, 151,
152 | syl2anc 673 |
. . . . . . . . . . . . 13
      
  |
154 | 153 | adantll 728 |
. . . . . . . . . . . 12
   
     
   |
155 | 68 | adantr 472 |
. . . . . . . . . . . . . 14
 
       |
156 | | foelrni 5927 |
. . . . . . . . . . . . . 14
     


      |
157 | 155, 73, 156 | syl2anc 673 |
. . . . . . . . . . . . 13
 
 
      |
158 | | nfv 1769 |
. . . . . . . . . . . . . 14
  
  |
159 | 119 | sselda 3418 |
. . . . . . . . . . . . . . . . . 18
 
   |
160 | 159 | 3adant3 1050 |
. . . . . . . . . . . . . . . . 17
 
    
  |
161 | 159, 87, 133 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . 20
 
                |
162 | 161, 3 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . 19
 
           |
163 | 162 | 3adant3 1050 |
. . . . . . . . . . . . . . . . . 18
 
    
          |
164 | | simp3 1032 |
. . . . . . . . . . . . . . . . . 18
 
    
      |
165 | 163, 164 | eqtr2d 2506 |
. . . . . . . . . . . . . . . . 17
 
    
      |
166 | 160, 165,
100 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
 
    
       |
167 | 166 | 3exp 1230 |
. . . . . . . . . . . . . . 15
       
        |
168 | 167 | adantr 472 |
. . . . . . . . . . . . . 14
 
       
        |
169 | 158, 78, 168 | rexlimd 2866 |
. . . . . . . . . . . . 13
 
  
            |
170 | 157, 169 | mpd 15 |
. . . . . . . . . . . 12
 
        |
171 | 147, 154,
170 | syl2anc 673 |
. . . . . . . . . . 11
   
     
 
      |
172 | 146, 171 | pm2.61dan 808 |
. . . . . . . . . 10
  


   
       |
173 | 172 | ralrimiva 2809 |
. . . . . . . . 9
 
              |
174 | 118, 173 | jca 541 |
. . . . . . . 8
 
                        |
175 | | dffo3 6052 |
. . . . . . . 8
              
                 |
176 | 174, 175 | sylibr 217 |
. . . . . . 7
 
           |
177 | | founiiun 37517 |
. . . . . . 7
              
      |
178 | 176, 177 | syl 17 |
. . . . . 6
 
  
          |
179 | 117, 178 | eqtrd 2505 |
. . . . 5
 
         |
180 | 111, 179 | pm2.61dan 808 |
. . . 4
  
      |
181 | 180 | fveq2d 5883 |
. . 3
                 |
182 | | uncom 3569 |
. . . . . . . . 9
         |
183 | 182 | a1i 11 |
. . . . . . . 8
           |
184 | | undif 3839 |
. . . . . . . . 9

 
    |
185 | 119, 184 | sylib 201 |
. . . . . . . 8
       |
186 | 183, 185 | eqtrd 2505 |
. . . . . . 7
       |
187 | 186 | eqcomd 2477 |
. . . . . 6
       |
188 | 187 | mpteq1d 4477 |
. . . . 5
                           |
189 | 188 | fveq2d 5883 |
. . . 4
 Σ^            Σ^                  |
190 | | nfv 1769 |
. . . . 5
   |
191 | | difexg 4545 |
. . . . . . 7
     |
192 | 32, 191 | ax-mp 5 |
. . . . . 6
   |
193 | 192 | a1i 11 |
. . . . 5
     |
194 | 32 | a1i 11 |
. . . . . 6
   |
195 | 194, 119 | ssexd 4543 |
. . . . 5
   |
196 | | incom 3616 |
. . . . . . 7
         |
197 | | disjdif 3830 |
. . . . . . 7
     |
198 | 196, 197 | eqtri 2493 |
. . . . . 6
     |
199 | 198 | a1i 11 |
. . . . 5
       |
200 | | simpl 464 |
. . . . . 6
 

 
  |
201 | | eldifi 3544 |
. . . . . . 7
     |
202 | 201 | adantl 473 |
. . . . . 6
 

 
  |
203 | | isomenndlem.o |
. . . . . . . 8
           |
204 | 203 | adantr 472 |
. . . . . . 7
 

          |
205 | 31 | ffvelrnda 6037 |
. . . . . . 7
 

       |
206 | 204, 205 | ffvelrnd 6038 |
. . . . . 6
 

             |
207 | 200, 202,
206 | syl2anc 673 |
. . . . 5
 

 
             |
208 | 159, 206 | syldan 478 |
. . . . 5
 
              |
209 | 190, 193,
195, 199, 207, 208 | sge0splitmpt 38367 |
. . . 4
 Σ^                 Σ^                 Σ^               |
210 | | eqid 2471 |
. . . . . . . 8
                     |
211 | 208, 210 | fmptd 6061 |
. . . . . . 7
                    |
212 | 195, 211 | sge0xrcl 38341 |
. . . . . 6
 Σ^              |
213 | 212 | xaddid2d 37629 |
. . . . 5
     Σ^             Σ^              |
214 | 87 | a1i 11 |
. . . . . . . . . . . . 13
 

 
           |
215 | 202, 214,
133 | syl2anc 673 |
. . . . . . . . . . . 12
 

 
               |
216 | | eldifn 3545 |
. . . . . . . . . . . . . 14
  
  |
217 | 216 | adantl 473 |
. . . . . . . . . . . . 13
 

 
  |
218 | 217 | iffalsed 3883 |
. . . . . . . . . . . 12
 

 
           |
219 | 215, 218 | eqtrd 2505 |
. . . . . . . . . . 11
 

 
      |
220 | 219 | fveq2d 5883 |
. . . . . . . . . 10
 

 
              |
221 | | isomenndlem.o0 |
. . . . . . . . . . 11
       |
222 | 200, 221 | syl 17 |
. . . . . . . . . 10
 

 
      |
223 | 220, 222 | eqtrd 2505 |
. . . . . . . . 9
 

 
          |
224 | 223 | mpteq2dva 4482 |
. . . . . . . 8
                   |
225 | 224 | fveq2d 5883 |
. . . . . . 7
 Σ^              Σ^        |
226 | 190, 193 | sge0z 38331 |
. . . . . . 7
 Σ^        |
227 | 225, 226 | eqtrd 2505 |
. . . . . 6
 Σ^                |
228 | 227 | oveq1d 6323 |
. . . . 5
  Σ^                 Σ^                 Σ^               |
229 | 203, 25 | feqresmpt 5933 |
. . . . . . 7
           |
230 | 229 | fveq2d 5883 |
. . . . . 6
 Σ^    Σ^          |
231 | | nfv 1769 |
. . . . . . 7
   |
232 | | fveq2 5879 |
. . . . . . 7
                   |
233 | 162 | eqcomd 2477 |
. . . . . . 7
 
           |
234 | 203 | adantr 472 |
. . . . . . . 8
 
           |
235 | 25 | sselda 3418 |
. . . . . . . 8
 
    |
236 | 234, 235 | ffvelrnd 6038 |
. . . . . . 7
 
          |
237 | 231, 190,
232, 195, 4, 233, 236 | sge0f1o 38338 |
. . . . . 6
 Σ^        Σ^              |
238 | | eqidd 2472 |
. . . . . 6
 Σ^            Σ^              |
239 | 230, 237,
238 | 3eqtrd 2509 |
. . . . 5
 Σ^    Σ^              |
240 | 213, 228,
239 | 3eqtr4d 2515 |
. . . 4
  Σ^                 Σ^             Σ^      |
241 | 189, 209,
240 | 3eqtrrd 2510 |
. . 3
 Σ^    Σ^              |
242 | 181, 241 | breq12d 4408 |
. 2
       Σ^             Σ^               |
243 | 49, 242 | mpbird 240 |
1
      Σ^      |