Step | Hyp | Ref
| Expression |
1 | | coafval.o |
. 2
compa   |
2 | | fveq2 5879 |
. . . . . 6
 Nat  Nat    |
3 | | coafval.a |
. . . . . 6
Nat   |
4 | 2, 3 | syl6eqr 2523 |
. . . . 5
 Nat    |
5 | 4 | rabeqdv 3025 |
. . . . 5
  Nat  coda        
coda          |
6 | | fveq2 5879 |
. . . . . . . . 9
 comp  comp    |
7 | | coafval.x |
. . . . . . . . 9
comp   |
8 | 6, 7 | syl6eqr 2523 |
. . . . . . . 8
 comp   |
9 | 8 | oveqd 6325 |
. . . . . . 7
                comp   coda                 coda     |
10 | 9 | oveqd 6325 |
. . . . . 6
                      comp   coda                             coda           |
11 | 10 | oteq3d 4172 |
. . . . 5
        coda                        comp   coda                 coda                       coda            |
12 | 4, 5, 11 | mpt2eq123dv 6372 |
. . . 4
  Nat    Nat  coda               coda                        comp   coda              coda               coda                       coda             |
13 | | df-coa 16029 |
. . . 4
compa   Nat  
 Nat  coda               coda                        comp   coda             |
14 | | fvex 5889 |
. . . . . 6
Nat   |
15 | 3, 14 | eqeltri 2545 |
. . . . 5
 |
16 | 15 | rabex 4550 |
. . . . 5

coda         |
17 | 15, 16 | mpt2ex 6889 |
. . . 4
   coda               coda                       coda            |
18 | 12, 13, 17 | fvmpt 5963 |
. . 3
 compa     coda               coda                       coda             |
19 | 13 | dmmptss 5338 |
. . . . . . 7
compa  |
20 | 19 | sseli 3414 |
. . . . . 6

compa   |
21 | 20 | con3i 142 |
. . . . 5

compa |
22 | | ndmfv 5903 |
. . . . 5

compa compa    |
23 | 21, 22 | syl 17 |
. . . 4
 compa    |
24 | 3 | arwrcl 16017 |
. . . . . . . 8
   |
25 | 24 | con3i 142 |
. . . . . . 7
   |
26 | 25 | eq0rdv 3773 |
. . . . . 6
   |
27 | | eqidd 2472 |
. . . . . 6
  coda         coda          |
28 | | eqidd 2472 |
. . . . . 6
        coda                       coda                 coda                       coda            |
29 | 26, 27, 28 | mpt2eq123dv 6372 |
. . . . 5
   
coda               coda                       coda              coda               coda                       coda             |
30 | | mpt20 6380 |
. . . . 5
   coda               coda                       coda            |
31 | 29, 30 | syl6eq 2521 |
. . . 4
   
coda               coda                       coda             |
32 | 23, 31 | eqtr4d 2508 |
. . 3
 compa    
coda               coda                       coda             |
33 | 18, 32 | pm2.61i 169 |
. 2
compa     coda               coda                       coda            |
34 | 1, 33 | eqtri 2493 |
1
 

coda               coda                       coda            |