Metamath Proof Explorer


Theorem s7cld

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

Ref Expression
Hypotheses s2cld.1 φAX
s2cld.2 φBX
s3cld.3 φCX
s4cld.4 φDX
s5cld.5 φEX
s6cld.6 φFX
s7cld.7 φGX
Assertion s7cld φ⟨“ABCDEFG”⟩WordX

Proof

Step Hyp Ref Expression
1 s2cld.1 φAX
2 s2cld.2 φBX
3 s3cld.3 φCX
4 s4cld.4 φDX
5 s5cld.5 φEX
6 s6cld.6 φFX
7 s7cld.7 φGX
8 df-s7 ⟨“ABCDEFG”⟩=⟨“ABCDEF”⟩++⟨“G”⟩
9 1 2 3 4 5 6 s6cld φ⟨“ABCDEF”⟩WordX
10 8 9 7 cats1cld φ⟨“ABCDEFG”⟩WordX