| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cats1cld.1 |
|- T = ( S ++ <" X "> ) |
| 2 |
|
cats1cli.2 |
|- S e. Word _V |
| 3 |
|
cats1fvn.3 |
|- ( # ` S ) = M |
| 4 |
|
cats1len.4 |
|- ( M + 1 ) = N |
| 5 |
1
|
fveq2i |
|- ( # ` T ) = ( # ` ( S ++ <" X "> ) ) |
| 6 |
|
s1cli |
|- <" X "> e. Word _V |
| 7 |
|
ccatlen |
|- ( ( S e. Word _V /\ <" X "> e. Word _V ) -> ( # ` ( S ++ <" X "> ) ) = ( ( # ` S ) + ( # ` <" X "> ) ) ) |
| 8 |
2 6 7
|
mp2an |
|- ( # ` ( S ++ <" X "> ) ) = ( ( # ` S ) + ( # ` <" X "> ) ) |
| 9 |
|
s1len |
|- ( # ` <" X "> ) = 1 |
| 10 |
3 9
|
oveq12i |
|- ( ( # ` S ) + ( # ` <" X "> ) ) = ( M + 1 ) |
| 11 |
8 10
|
eqtri |
|- ( # ` ( S ++ <" X "> ) ) = ( M + 1 ) |
| 12 |
11 4
|
eqtri |
|- ( # ` ( S ++ <" X "> ) ) = N |
| 13 |
5 12
|
eqtri |
|- ( # ` T ) = N |