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 × V )

Proof

Step	Hyp	Ref	Expression
1		df-concat	⊢ ++ = ( 𝑠 ∈ V , 𝑡 ∈ V ↦ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑠 ) + ( ♯ ‘ 𝑡 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑠 ) ) , ( 𝑠 ‘ 𝑥 ) , ( 𝑡 ‘ ( 𝑥 − ( ♯ ‘ 𝑠 ) ) ) ) ) )
2		ovex	⊢ ( 0 ..^ ( ( ♯ ‘ 𝑠 ) + ( ♯ ‘ 𝑡 ) ) ) ∈ V
3	2	mptex	⊢ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑠 ) + ( ♯ ‘ 𝑡 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑠 ) ) , ( 𝑠 ‘ 𝑥 ) , ( 𝑡 ‘ ( 𝑥 − ( ♯ ‘ 𝑠 ) ) ) ) ) ∈ V
4	1 3	fnmpoi	⊢ ++ Fn ( V × V )