Metamath Proof Explorer

Theorem ccatvalfn

Description: The concatenation of two words is a function over the half-open integer range having the sum of the lengths of the word as length. (Contributed by Alexander van der Vekens, 30-Mar-2018)

Ref Expression
Assertion ccatvalfn ⊢ A ∈ Word V ∧ B ∈ Word V → A ++ B Fn 0 ..^ A + B

Proof

Step Hyp Ref Expression
1 ccatfval ⊢ A ∈ Word V ∧ B ∈ Word V → A ++ B = x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A
2 fvex ⊢ A ⁡ x ∈ V
3 fvex ⊢ B ⁡ x − A ∈ V
4 2 3 ifex ⊢ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A ∈ V
5 eqid ⊢ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A = x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A
6 4 5 fnmpti ⊢ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A Fn 0 ..^ A + B
7 fneq1 ⊢ A ++ B = x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A → A ++ B Fn 0 ..^ A + B ↔ x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A Fn 0 ..^ A + B
8 6 7 mpbiri ⊢ A ++ B = x ∈ 0 ..^ A + B ⟼ if x ∈ 0 ..^ A A ⁡ x B ⁡ x − A → A ++ B Fn 0 ..^ A + B
9 1 8 syl ⊢ A ∈ Word V ∧ B ∈ Word V → A ++ B Fn 0 ..^ A + B