This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ++ Fn V × V

Proof

Step Hyp Ref Expression
1 df-concat ⊢ ++ = s ∈ V , t ∈ V ⟼ x ∈ 0 ..^ s + t ⟼ if x ∈ 0 ..^ s s ⁡ x t ⁡ x − s
2 ovex ⊢ 0 ..^ s + t ∈ V
3 2 mptex ⊢ x ∈ 0 ..^ s + t ⟼ if x ∈ 0 ..^ s s ⁡ x t ⁡ x − s ∈ V
4 1 3 fnmpoi ⊢ ++ Fn V × V