Theorem s7len

Description: The length of a length 7 string. (Contributed by Mario Carneiro, 26-Feb-2016)

	Ref	Expression
Assertion	s7len	⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ ) = 7

Proof

Step	Hyp	Ref	Expression
1		df-s7	⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 ”⟩ ++ ⟨“ 𝐺 ”⟩ )
2		s6cli	⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 ”⟩ ∈ Word V
3		s6len	⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 ”⟩ ) = 6
4		6p1e7	⊢ ( 6 + 1 ) = 7
5	1 2 3 4	cats1len	⊢ ( ♯ ‘ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ ) = 7