Theorem ccatfn

Description: The concatenation operator is a two-argument function. (Contributed by Mario Carneiro, 27-Sep-2015) (Proof shortened by AV, 29-Apr-2020)

	Ref	Expression
Assertion	ccatfn	|- ++ Fn ( _V X. _V )

Proof

Step	Hyp	Ref	Expression
1		df-concat	|- ++ = ( s e. _V , t e. _V |-> ( x e. ( 0 ..^ ( ( # ` s ) + ( # ` t ) ) ) |-> if ( x e. ( 0 ..^ ( # ` s ) ) , ( s ` x ) , ( t ` ( x - ( # ` s ) ) ) ) ) )
2		ovex	|- ( 0 ..^ ( ( # ` s ) + ( # ` t ) ) ) e. _V
3	2	mptex	|- ( x e. ( 0 ..^ ( ( # ` s ) + ( # ` t ) ) ) |-> if ( x e. ( 0 ..^ ( # ` s ) ) , ( s ` x ) , ( t ` ( x - ( # ` s ) ) ) ) ) e. _V
4	1 3	fnmpoi	|- ++ Fn ( _V X. _V )