Metamath Proof Explorer


Theorem s4cld

Description: A length 4 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypotheses s2cld.1 ( 𝜑𝐴𝑋 )
s2cld.2 ( 𝜑𝐵𝑋 )
s3cld.3 ( 𝜑𝐶𝑋 )
s4cld.4 ( 𝜑𝐷𝑋 )
Assertion s4cld ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ∈ Word 𝑋 )

Proof

Step Hyp Ref Expression
1 s2cld.1 ( 𝜑𝐴𝑋 )
2 s2cld.2 ( 𝜑𝐵𝑋 )
3 s3cld.3 ( 𝜑𝐶𝑋 )
4 s4cld.4 ( 𝜑𝐷𝑋 )
5 df-s4 ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ++ ⟨“ 𝐷 ”⟩ )
6 1 2 3 s3cld ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑋 )
7 5 6 4 cats1cld ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ∈ Word 𝑋 )