Step | Hyp | Ref
| Expression |
1 | | eqid 2471 |
. 2
             |
2 | | mapfien.g |
. . . . . . 7
       |
3 | | f1of 5828 |
. . . . . . 7
    
      |
4 | 2, 3 | syl 17 |
. . . . . 6
       |
5 | 4 | adantr 472 |
. . . . 5
 
       |
6 | | breq1 4398 |
. . . . . . . . . 10
  finSupp
finSupp    |
7 | | mapfien.s |
. . . . . . . . . 10
   finSupp
  |
8 | 6, 7 | elrab2 3186 |
. . . . . . . . 9

  
finSupp    |
9 | 8 | simplbi 467 |
. . . . . . . 8
     |
10 | 9 | adantl 473 |
. . . . . . 7
 
     |
11 | | elmapi 7511 |
. . . . . . 7
         |
12 | 10, 11 | syl 17 |
. . . . . 6
 
       |
13 | | mapfien.f |
. . . . . . . 8
       |
14 | | f1of 5828 |
. . . . . . . 8
    
      |
15 | 13, 14 | syl 17 |
. . . . . . 7
       |
16 | 15 | adantr 472 |
. . . . . 6
 
       |
17 | | fco 5751 |
. . . . . 6
                   |
18 | 12, 16, 17 | syl2anc 673 |
. . . . 5
 
         |
19 | | fco 5751 |
. . . . 5
                       |
20 | 5, 18, 19 | syl2anc 673 |
. . . 4
 
 
         |
21 | | mapfien.d |
. . . . . 6
   |
22 | | mapfien.c |
. . . . . 6
   |
23 | 21, 22 | elmapd 7504 |
. . . . 5
                   |
24 | 23 | adantr 472 |
. . . 4
 
       
           |
25 | 20, 24 | mpbird 240 |
. . 3
 
 
       |
26 | | mapfien.t |
. . . 4
   finSupp
  |
27 | | mapfien.w |
. . . 4
     |
28 | | mapfien.a |
. . . 4
   |
29 | | mapfien.b |
. . . 4
   |
30 | | mapfien.z |
. . . 4
   |
31 | 7, 26, 27, 13, 2, 28, 29, 22, 21, 30 | mapfienlem1 7936 |
. . 3
 
 
   finSupp   |
32 | | breq1 4398 |
. . . 4
      finSupp
    finSupp
   |
33 | 32, 26 | elrab2 3186 |
. . 3
    
 
    
    finSupp
   |
34 | 25, 31, 33 | sylanbrc 677 |
. 2
 
 
     |
35 | 7, 26, 27, 13, 2, 28, 29, 22, 21, 30 | mapfienlem3 7938 |
. 2
 
         |
36 | | coass 5361 |
. . . . . 6
          
      |
37 | 13 | adantr 472 |
. . . . . . . . 9
 

        |
38 | | f1ococnv1 5856 |
. . . . . . . . 9
    
 

   |
39 | 37, 38 | syl 17 |
. . . . . . . 8
 

    
   |
40 | 39 | coeq2d 5002 |
. . . . . . 7
 

       
          |
41 | | f1ocnv 5840 |
. . . . . . . . . . . 12
    
       |
42 | | f1of 5828 |
. . . . . . . . . . . 12
             |
43 | 2, 41, 42 | 3syl 18 |
. . . . . . . . . . 11
        |
44 | 43 | adantr 472 |
. . . . . . . . . 10
 
        |
45 | | simpr 468 |
. . . . . . . . . . . . 13
 
   |
46 | | breq1 4398 |
. . . . . . . . . . . . . 14
  finSupp
finSupp    |
47 | 46, 26 | elrab2 3186 |
. . . . . . . . . . . . 13

  
finSupp    |
48 | 45, 47 | sylib 201 |
. . . . . . . . . . . 12
 
    finSupp    |
49 | 48 | simpld 466 |
. . . . . . . . . . 11
 
     |
50 | | elmapi 7511 |
. . . . . . . . . . 11
         |
51 | 49, 50 | syl 17 |
. . . . . . . . . 10
 
       |
52 | | fco 5751 |
. . . . . . . . . 10
                     |
53 | 44, 51, 52 | syl2anc 673 |
. . . . . . . . 9
 
  
       |
54 | 53 | adantrl 730 |
. . . . . . . 8
 

           |
55 | | fcoi1 5769 |
. . . . . . . 8
  
                |
56 | 54, 55 | syl 17 |
. . . . . . 7
 

             |
57 | 40, 56 | eqtrd 2505 |
. . . . . 6
 

       
   
   |
58 | 36, 57 | syl5eq 2517 |
. . . . 5
 

               |
59 | 58 | eqeq2d 2481 |
. . . 4
 

                
    |
60 | | coass 5361 |
. . . . . . 7
  
            |
61 | 2 | adantr 472 |
. . . . . . . . . 10
 

        |
62 | | f1ococnv1 5856 |
. . . . . . . . . 10
    
 

   |
63 | 61, 62 | syl 17 |
. . . . . . . . 9
 

    
   |
64 | 63 | coeq1d 5001 |
. . . . . . . 8
 

         
      |
65 | 18 | adantrr 731 |
. . . . . . . . 9
 

          |
66 | | fcoi2 5770 |
. . . . . . . . 9
                |
67 | 65, 66 | syl 17 |
. . . . . . . 8
 

           |
68 | 64, 67 | eqtrd 2505 |
. . . . . . 7
 

             |
69 | 60, 68 | syl5eqr 2519 |
. . . . . 6
 

    
        |
70 | 69 | eqeq2d 2481 |
. . . . 5
 

       

            |
71 | | eqcom 2478 |
. . . . 5
  
  
   
   |
72 | 70, 71 | syl6bb 269 |
. . . 4
 

       

            |
73 | 59, 72 | bitr4d 264 |
. . 3
 

                 

       |
74 | | f1ofo 5835 |
. . . . 5
    
      |
75 | 37, 74 | syl 17 |
. . . 4
 

        |
76 | | ffn 5739 |
. . . . . 6
       |
77 | 10, 11, 76 | 3syl 18 |
. . . . 5
 
   |
78 | 77 | adantrr 731 |
. . . 4
 

    |
79 | | f1ocnv 5840 |
. . . . . . . . 9
    
       |
80 | | f1of 5828 |
. . . . . . . . 9
             |
81 | 13, 79, 80 | 3syl 18 |
. . . . . . . 8
        |
82 | 81 | adantr 472 |
. . . . . . 7
 
        |
83 | | fco 5751 |
. . . . . . 7
                           |
84 | 53, 82, 83 | syl2anc 673 |
. . . . . 6
 
             |
85 | | ffn 5739 |
. . . . . 6
                   |
86 | 84, 85 | syl 17 |
. . . . 5
 
         |
87 | 86 | adantrl 730 |
. . . 4
 

          |
88 | | cocan2 6208 |
. . . 4
     
      
      
      
      |
89 | 75, 78, 87, 88 | syl3anc 1292 |
. . 3
 

                      |
90 | 2, 41 | syl 17 |
. . . . . 6
        |
91 | 90 | adantr 472 |
. . . . 5
 

         |
92 | | f1of1 5827 |
. . . . 5
             |
93 | 91, 92 | syl 17 |
. . . 4
 

         |
94 | 51 | adantrl 730 |
. . . 4
 

        |
95 | 20 | adantrr 731 |
. . . 4
 

            |
96 | | cocan1 6207 |
. . . 4
           
                  

      |
97 | 93, 94, 95, 96 | syl3anc 1292 |
. . 3
 

       

           |
98 | 73, 89, 97 | 3bitr3d 291 |
. 2
 

        

      |
99 | 1, 34, 35, 98 | f1o2d 6540 |
1
             |