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	$$⊢\mathrm{++}Fn\left(\mathrm{V}\times \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-concat	$$⊢\mathrm{++}=\left(s\in \mathrm{V},t\in \mathrm{V}⟼\left(x\in \left(0..^\left|s\right|+\left|t\right|\right)⟼if\left(x\in \left(0..^\left|s\right|\right),s\left(x\right),t\left(x-\left|s\right|\right)\right)\right)\right)$$
2		ovex	$$⊢\left(0..^\left|s\right|+\left|t\right|\right)\in \mathrm{V}$$
3	2	mptex	$$⊢\left(x\in \left(0..^\left|s\right|+\left|t\right|\right)⟼if\left(x\in \left(0..^\left|s\right|\right),s\left(x\right),t\left(x-\left|s\right|\right)\right)\right)\in \mathrm{V}$$
4	1 3	fnmpoi	$$⊢\mathrm{++}Fn\left(\mathrm{V}\times \mathrm{V}\right)$$