Metamath Proof Explorer

Theorem elfzelfzccat

Description: An element of a finite set of sequential integers up to the length of a word is an element of an extended finite set of sequential integers up to the length of a concatenation of this word with another word. (Contributed by Alexander van der Vekens, 28-Mar-2018)

Ref Expression
Assertion elfzelfzccat 
|- ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( 0 ... ( # ` A ) ) -> N e. ( 0 ... ( # ` ( A ++ B ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lencl 
 |-  ( A e. Word V -> ( # ` A ) e. NN0 )
2 lencl 
 |-  ( B e. Word V -> ( # ` B ) e. NN0 )
3 elfz0add 
 |-  ( ( ( # ` A ) e. NN0 /\ ( # ` B ) e. NN0 ) -> ( N e. ( 0 ... ( # ` A ) ) -> N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) )
4 1 2 3 syl2an 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( 0 ... ( # ` A ) ) -> N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) )
5 ccatlen 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( # ` ( A ++ B ) ) = ( ( # ` A ) + ( # ` B ) ) )
6 5 oveq2d 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( 0 ... ( # ` ( A ++ B ) ) ) = ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) )
7 6 eleq2d 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( 0 ... ( # ` ( A ++ B ) ) ) <-> N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) )
8 4 7 sylibrd 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( 0 ... ( # ` A ) ) -> N e. ( 0 ... ( # ` ( A ++ B ) ) ) ) )