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 ++ = ( 𝑠 ∈ V , 𝑡 ∈ V ↦ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑠 ) + ( ♯ ‘ 𝑡 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑠 ) ) , ( 𝑠𝑥 ) , ( 𝑡 ‘ ( 𝑥 − ( ♯ ‘ 𝑠 ) ) ) ) ) )
2 ovex ( 0 ..^ ( ( ♯ ‘ 𝑠 ) + ( ♯ ‘ 𝑡 ) ) ) ∈ V
3 2 mptex ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑠 ) + ( ♯ ‘ 𝑡 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑠 ) ) , ( 𝑠𝑥 ) , ( 𝑡 ‘ ( 𝑥 − ( ♯ ‘ 𝑠 ) ) ) ) ) ∈ V
4 1 3 fnmpoi ++ Fn ( V × V )