Metamath Proof Explorer

Theorem ccatvalfn

Description: The concatenation of two words is a function over the half-open integer range having the sum of the lengths of the word as length. (Contributed by Alexander van der Vekens, 30-Mar-2018)

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

Proof

Step Hyp Ref Expression
1 ccatfval 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( A ++ B ) = ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) )
2 fvex 
 |-  ( A ` x ) e. _V
3 fvex 
 |-  ( B ` ( x - ( # ` A ) ) ) e. _V
4 2 3 ifex 
 |-  if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) e. _V
5 eqid 
 |-  ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) = ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) )
6 4 5 fnmpti 
 |-  ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) Fn ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) )
7 fneq1 
 |-  ( ( A ++ B ) = ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) -> ( ( A ++ B ) Fn ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) <-> ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) Fn ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) ) )
8 6 7 mpbiri 
 |-  ( ( A ++ B ) = ( x e. ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) |-> if ( x e. ( 0 ..^ ( # ` A ) ) , ( A ` x ) , ( B ` ( x - ( # ` A ) ) ) ) ) -> ( A ++ B ) Fn ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) )
9 1 8 syl 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( A ++ B ) Fn ( 0 ..^ ( ( # ` A ) + ( # ` B ) ) ) )