Metamath Proof Explorer

Theorem s6len

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

Ref Expression
Assertion s6len 
|- ( # ` <" A B C D E F "> ) = 6

Proof

Step Hyp Ref Expression
1 df-s6 
 |-  <" A B C D E F "> = ( <" A B C D E "> ++ <" F "> )
2 s5cli 
 |-  <" A B C D E "> e. Word _V
3 s5len 
 |-  ( # ` <" A B C D E "> ) = 5
4 5p1e6 
 |-  ( 5 + 1 ) = 6
5 1 2 3 4 cats1len 
 |-  ( # ` <" A B C D E F "> ) = 6