Theorem wrdl1s1

Description: A word of length 1 is a singleton word consisting of the first symbol of the word. (Contributed by AV, 22-Jul-2018) (Proof shortened by AV, 14-Oct-2018)

	Ref	Expression
Assertion	wrdl1s1	⊢ ( 𝑆 ∈ 𝑉 → ( 𝑊 = ⟨“ 𝑆 ”⟩ ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ∧ ( 𝑊 ‘ 0 ) = 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		s1cl	⊢ ( 𝑆 ∈ 𝑉 → ⟨“ 𝑆 ”⟩ ∈ Word 𝑉 )
2		s1len	⊢ ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) = 1
3	2	a1i	⊢ ( 𝑆 ∈ 𝑉 → ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) = 1 )
4		s1fv	⊢ ( 𝑆 ∈ 𝑉 → ( ⟨“ 𝑆 ”⟩ ‘ 0 ) = 𝑆 )
5	1 3 4	3jca	⊢ ( 𝑆 ∈ 𝑉 → ( ⟨“ 𝑆 ”⟩ ∈ Word 𝑉 ∧ ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) = 1 ∧ ( ⟨“ 𝑆 ”⟩ ‘ 0 ) = 𝑆 ) )
6		eleq1	⊢ ( 𝑊 = ⟨“ 𝑆 ”⟩ → ( 𝑊 ∈ Word 𝑉 ↔ ⟨“ 𝑆 ”⟩ ∈ Word 𝑉 ) )
7		fveqeq2	⊢ ( 𝑊 = ⟨“ 𝑆 ”⟩ → ( ( ♯ ‘ 𝑊 ) = 1 ↔ ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) = 1 ) )
8		fveq1	⊢ ( 𝑊 = ⟨“ 𝑆 ”⟩ → ( 𝑊 ‘ 0 ) = ( ⟨“ 𝑆 ”⟩ ‘ 0 ) )
9	8	eqeq1d	⊢ ( 𝑊 = ⟨“ 𝑆 ”⟩ → ( ( 𝑊 ‘ 0 ) = 𝑆 ↔ ( ⟨“ 𝑆 ”⟩ ‘ 0 ) = 𝑆 ) )
10	6 7 9	3anbi123d	⊢ ( 𝑊 = ⟨“ 𝑆 ”⟩ → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ∧ ( 𝑊 ‘ 0 ) = 𝑆 ) ↔ ( ⟨“ 𝑆 ”⟩ ∈ Word 𝑉 ∧ ( ♯ ‘ ⟨“ 𝑆 ”⟩ ) = 1 ∧ ( ⟨“ 𝑆 ”⟩ ‘ 0 ) = 𝑆 ) ) )
11	5 10	syl5ibrcom	⊢ ( 𝑆 ∈ 𝑉 → ( 𝑊 = ⟨“ 𝑆 ”⟩ → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ∧ ( 𝑊 ‘ 0 ) = 𝑆 ) ) )
12		eqs1	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ) → 𝑊 = ⟨“ ( 𝑊 ‘ 0 ) ”⟩ )
13		s1eq	⊢ ( ( 𝑊 ‘ 0 ) = 𝑆 → ⟨“ ( 𝑊 ‘ 0 ) ”⟩ = ⟨“ 𝑆 ”⟩ )
14	13	eqeq2d	⊢ ( ( 𝑊 ‘ 0 ) = 𝑆 → ( 𝑊 = ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ↔ 𝑊 = ⟨“ 𝑆 ”⟩ ) )
15	12 14	syl5ibcom	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( ( 𝑊 ‘ 0 ) = 𝑆 → 𝑊 = ⟨“ 𝑆 ”⟩ ) )
16	15	3impia	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ∧ ( 𝑊 ‘ 0 ) = 𝑆 ) → 𝑊 = ⟨“ 𝑆 ”⟩ )
17	11 16	impbid1	⊢ ( 𝑆 ∈ 𝑉 → ( 𝑊 = ⟨“ 𝑆 ”⟩ ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ∧ ( 𝑊 ‘ 0 ) = 𝑆 ) ) )