Metamath Proof Explorer


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 ++FnV×V

Proof

Step Hyp Ref Expression
1 df-concat ++=sV,tVx0..^s+tifx0..^ssxtxs
2 ovex 0..^s+tV
3 2 mptex x0..^s+tifx0..^ssxtxsV
4 1 3 fnmpoi ++FnV×V