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