Step | Hyp | Ref
| Expression |
1 | | tsmsid.2 |
. . . . . . 7
   |
2 | | tsmsid.b |
. . . . . . . 8
     |
3 | | tsmsgsum.j |
. . . . . . . 8
     |
4 | 2, 3 | istps 20000 |
. . . . . . 7
 TopOn    |
5 | 1, 4 | sylib 201 |
. . . . . 6
 TopOn    |
6 | | toponuni 19991 |
. . . . . 6
 TopOn 
   |
7 | 5, 6 | syl 17 |
. . . . 5
    |
8 | 7 | eleq2d 2525 |
. . . 4
      |
9 | | elfpw 7902 |
. . . . . . . . . . . . . . 15
   
    |
10 | 9 | simplbi 466 |
. . . . . . . . . . . . . 14
      |
11 | 10 | adantl 472 |
. . . . . . . . . . . . 13
          |
12 | | suppssdm 6954 |
. . . . . . . . . . . . . . 15
 supp  |
13 | | tsmsid.f |
. . . . . . . . . . . . . . . 16
       |
14 | | fdm 5756 |
. . . . . . . . . . . . . . . 16
       |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . 15
   |
16 | 12, 15 | syl5sseq 3492 |
. . . . . . . . . . . . . 14
  supp   |
17 | 16 | ad2antrr 737 |
. . . . . . . . . . . . 13
         supp   |
18 | 11, 17 | unssd 3622 |
. . . . . . . . . . . 12
          supp    |
19 | 9 | simprbi 470 |
. . . . . . . . . . . . . 14
      |
20 | 19 | adantl 472 |
. . . . . . . . . . . . 13
          |
21 | | tsmsid.w |
. . . . . . . . . . . . . . 15
 finSupp
 |
22 | 21 | ad2antrr 737 |
. . . . . . . . . . . . . 14
        finSupp  |
23 | 22 | fsuppimpd 7916 |
. . . . . . . . . . . . 13
         supp   |
24 | | unfi 7864 |
. . . . . . . . . . . . 13
  
supp    supp    |
25 | 20, 23, 24 | syl2anc 671 |
. . . . . . . . . . . 12
          supp    |
26 | | elfpw 7902 |
. . . . . . . . . . . 12
   supp        supp    supp     |
27 | 18, 25, 26 | sylanbrc 675 |
. . . . . . . . . . 11
          supp       |
28 | | ssun1 3609 |
. . . . . . . . . . . . . . 15
  supp   |
29 | | id 22 |
. . . . . . . . . . . . . . 15
   supp 
  supp    |
30 | 28, 29 | syl5sseqr 3493 |
. . . . . . . . . . . . . 14
   supp 
  |
31 | | pm5.5 342 |
. . . . . . . . . . . . . 14
    g      g       |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . 13
   supp 
 
 g      g       |
33 | | reseq2 5119 |
. . . . . . . . . . . . . . 15
   supp 
  
  supp     |
34 | 33 | oveq2d 6331 |
. . . . . . . . . . . . . 14
   supp 
 g 
   g 
  supp      |
35 | 34 | eleq1d 2524 |
. . . . . . . . . . . . 13
   supp 
  g     g    supp       |
36 | 32, 35 | bitrd 261 |
. . . . . . . . . . . 12
   supp 
 
 g      g    supp       |
37 | 36 | rspcv 3158 |
. . . . . . . . . . 11
   supp    
 
    
 g    
 g 
  supp       |
38 | 27, 37 | syl 17 |
. . . . . . . . . 10
         
 
    g    
 g 
  supp       |
39 | | tsmsid.z |
. . . . . . . . . . . 12
     |
40 | | tsmsid.1 |
. . . . . . . . . . . . 13
 CMnd |
41 | 40 | ad2antrr 737 |
. . . . . . . . . . . 12
        CMnd |
42 | | tsmsid.a |
. . . . . . . . . . . . 13
   |
43 | 42 | ad2antrr 737 |
. . . . . . . . . . . 12
          |
44 | 13 | ad2antrr 737 |
. . . . . . . . . . . 12
              |
45 | | ssun2 3610 |
. . . . . . . . . . . . 13
 supp   supp   |
46 | 45 | a1i 11 |
. . . . . . . . . . . 12
         supp   supp    |
47 | 2, 39, 41, 43, 44, 46, 22 | gsumres 17596 |
. . . . . . . . . . 11
         g    supp     g    |
48 | 47 | eleq1d 2524 |
. . . . . . . . . 10
          g    supp   
 g     |
49 | 38, 48 | sylibd 222 |
. . . . . . . . 9
         
 
    g    
 g     |
50 | 49 | rexlimdva 2891 |
. . . . . . . 8
 
  
 
  
 
    g    
 g     |
51 | 21 | fsuppimpd 7916 |
. . . . . . . . . . . 12
  supp   |
52 | | elfpw 7902 |
. . . . . . . . . . . 12
  supp
     supp  supp    |
53 | 16, 51, 52 | sylanbrc 675 |
. . . . . . . . . . 11
  supp      |
54 | 53 | adantr 471 |
. . . . . . . . . 10
 

 g     supp      |
55 | 40 | ad2antrr 737 |
. . . . . . . . . . . . . 14
    
g         supp  
CMnd |
56 | 42 | ad2antrr 737 |
. . . . . . . . . . . . . 14
    
g         supp  
  |
57 | 13 | ad2antrr 737 |
. . . . . . . . . . . . . 14
    
g         supp         |
58 | | simprr 771 |
. . . . . . . . . . . . . 14
    
g         supp    supp
  |
59 | 21 | ad2antrr 737 |
. . . . . . . . . . . . . 14
    
g         supp   finSupp  |
60 | 2, 39, 55, 56, 57, 58, 59 | gsumres 17596 |
. . . . . . . . . . . . 13
    
g         supp    g     g    |
61 | | simplrr 776 |
. . . . . . . . . . . . 13
    
g         supp    g    |
62 | 60, 61 | eqeltrd 2540 |
. . . . . . . . . . . 12
    
g         supp    g      |
63 | 62 | expr 624 |
. . . . . . . . . . 11
    
g          supp
 g 
     |
64 | 63 | ralrimiva 2814 |
. . . . . . . . . 10
 

 g           supp  g       |
65 | | sseq1 3465 |
. . . . . . . . . . . . 13
  supp   supp    |
66 | 65 | imbi1d 323 |
. . . . . . . . . . . 12
  supp    g       supp  g        |
67 | 66 | ralbidv 2839 |
. . . . . . . . . . 11
  supp         g    
       supp  g        |
68 | 67 | rspcev 3162 |
. . . . . . . . . 10
   supp           supp  g                  g       |
69 | 54, 64, 68 | syl2anc 671 |
. . . . . . . . 9
 

 g                g       |
70 | 69 | expr 624 |
. . . . . . . 8
 
   g              g        |
71 | 50, 70 | impbid 195 |
. . . . . . 7
 
  
 
  
 
    g      g     |
72 | | disjsn 4044 |
. . . . . . . 8
    g   
 g    |
73 | 72 | necon2abii 2686 |
. . . . . . 7
  g     g      |
74 | 71, 73 | syl6bb 269 |
. . . . . 6
 
  
 
  
 
    g        g       |
75 | 74 | imbi2d 322 |
. . . . 5
 
               g     

   g        |
76 | 75 | ralbidva 2836 |
. . . 4
   
            g     


   g        |
77 | 8, 76 | anbi12d 722 |
. . 3
   

            g          
   g         |
78 | | eqid 2462 |
. . . 4
       |
79 | 2, 3, 78, 40, 1, 42, 13 | eltsms 21196 |
. . 3
   tsums 



            g          |
80 | | topontop 19990 |
. . . . 5
 TopOn 
  |
81 | 5, 80 | syl 17 |
. . . 4
   |
82 | 2, 39, 40, 42, 13, 21 | gsumcl 17598 |
. . . . . 6
  g    |
83 | 82 | snssd 4130 |
. . . . 5
   g  
  |
84 | 83, 7 | sseqtrd 3480 |
. . . 4
   g  
   |
85 | | eqid 2462 |
. . . . 5
   |
86 | 85 | elcls2 20139 |
. . . 4
    g               g       
   g         |
87 | 81, 84, 86 | syl2anc 671 |
. . 3
           g       
   g         |
88 | 77, 79, 87 | 3bitr4d 293 |
. 2
   tsums 
         g       |
89 | 88 | eqrdv 2460 |
1
  tsums           g      |