Theorem wrdlen1

Description: A word of length 1 starts with a symbol. (Contributed by AV, 20-Jul-2018) (Proof shortened by AV, 19-Oct-2018)

	Ref	Expression
Assertion	wrdlen1	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ∃ 𝑣 ∈ 𝑉 ( 𝑊 ‘ 0 ) = 𝑣 )

Proof

Step	Hyp	Ref	Expression
1		1le1	⊢ 1 ≤ 1
2		breq2	⊢ ( ( ♯ ‘ 𝑊 ) = 1 → ( 1 ≤ ( ♯ ‘ 𝑊 ) ↔ 1 ≤ 1 ) )
3	1 2	mpbiri	⊢ ( ( ♯ ‘ 𝑊 ) = 1 → 1 ≤ ( ♯ ‘ 𝑊 ) )
4		wrdsymb1	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 )
5	3 4	sylan2	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( 𝑊 ‘ 0 ) ∈ 𝑉 )
6		clel5	⊢ ( ( 𝑊 ‘ 0 ) ∈ 𝑉 ↔ ∃ 𝑣 ∈ 𝑉 ( 𝑊 ‘ 0 ) = 𝑣 )
7	5 6	sylib	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ∃ 𝑣 ∈ 𝑉 ( 𝑊 ‘ 0 ) = 𝑣 )