Metamath Proof Explorer


Theorem wrdl2exs2

Description: A word of length two is a doubleton word. (Contributed by AV, 25-Jan-2021)

Ref Expression
Assertion wrdl2exs2 ( ( 𝑊 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑊 ) = 2 ) → ∃ 𝑠𝑆𝑡𝑆 𝑊 = ⟨“ 𝑠 𝑡 ”⟩ )

Proof

Step Hyp Ref Expression
1 1le2 1 ≤ 2
2 breq2 ( ( ♯ ‘ 𝑊 ) = 2 → ( 1 ≤ ( ♯ ‘ 𝑊 ) ↔ 1 ≤ 2 ) )
3 1 2 mpbiri ( ( ♯ ‘ 𝑊 ) = 2 → 1 ≤ ( ♯ ‘ 𝑊 ) )
4 wrdsymb1 ( ( 𝑊 ∈ Word 𝑆 ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ‘ 0 ) ∈ 𝑆 )
5 3 4 sylan2 ( ( 𝑊 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑊 ) = 2 ) → ( 𝑊 ‘ 0 ) ∈ 𝑆 )
6 lsw ( 𝑊 ∈ Word 𝑆 → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
7 oveq1 ( ( ♯ ‘ 𝑊 ) = 2 → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( 2 − 1 ) )
8 2m1e1 ( 2 − 1 ) = 1
9 7 8 eqtrdi ( ( ♯ ‘ 𝑊 ) = 2 → ( ( ♯ ‘ 𝑊 ) − 1 ) = 1 )
10 9 fveq2d ( ( ♯ ‘ 𝑊 ) = 2 → ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) = ( 𝑊 ‘ 1 ) )
11 6 10 sylan9eq ( ( 𝑊 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑊 ) = 2 ) → ( lastS ‘ 𝑊 ) = ( 𝑊 ‘ 1 ) )
12 2nn 2 ∈ ℕ
13 lswlgt0cl ( ( 2 ∈ ℕ ∧ ( 𝑊 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑊 ) = 2 ) ) → ( lastS ‘ 𝑊 ) ∈ 𝑆 )
14 12 13 mpan ( ( 𝑊 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑊 ) = 2 ) → ( lastS ‘ 𝑊 ) ∈ 𝑆 )
15 11 14 eqeltrrd ( ( 𝑊 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑊 ) = 2 ) → ( 𝑊 ‘ 1 ) ∈ 𝑆 )
16 wrdlen2s2 ( ( 𝑊 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑊 ) = 2 ) → 𝑊 = ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ )
17 id ( 𝑠 = ( 𝑊 ‘ 0 ) → 𝑠 = ( 𝑊 ‘ 0 ) )
18 eqidd ( 𝑠 = ( 𝑊 ‘ 0 ) → 𝑡 = 𝑡 )
19 17 18 s2eqd ( 𝑠 = ( 𝑊 ‘ 0 ) → ⟨“ 𝑠 𝑡 ”⟩ = ⟨“ ( 𝑊 ‘ 0 ) 𝑡 ”⟩ )
20 19 eqeq2d ( 𝑠 = ( 𝑊 ‘ 0 ) → ( 𝑊 = ⟨“ 𝑠 𝑡 ”⟩ ↔ 𝑊 = ⟨“ ( 𝑊 ‘ 0 ) 𝑡 ”⟩ ) )
21 eqidd ( 𝑡 = ( 𝑊 ‘ 1 ) → ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ 0 ) )
22 id ( 𝑡 = ( 𝑊 ‘ 1 ) → 𝑡 = ( 𝑊 ‘ 1 ) )
23 21 22 s2eqd ( 𝑡 = ( 𝑊 ‘ 1 ) → ⟨“ ( 𝑊 ‘ 0 ) 𝑡 ”⟩ = ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ )
24 23 eqeq2d ( 𝑡 = ( 𝑊 ‘ 1 ) → ( 𝑊 = ⟨“ ( 𝑊 ‘ 0 ) 𝑡 ”⟩ ↔ 𝑊 = ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ) )
25 20 24 rspc2ev ( ( ( 𝑊 ‘ 0 ) ∈ 𝑆 ∧ ( 𝑊 ‘ 1 ) ∈ 𝑆𝑊 = ⟨“ ( 𝑊 ‘ 0 ) ( 𝑊 ‘ 1 ) ”⟩ ) → ∃ 𝑠𝑆𝑡𝑆 𝑊 = ⟨“ 𝑠 𝑡 ”⟩ )
26 5 15 16 25 syl3anc ( ( 𝑊 ∈ Word 𝑆 ∧ ( ♯ ‘ 𝑊 ) = 2 ) → ∃ 𝑠𝑆𝑡𝑆 𝑊 = ⟨“ 𝑠 𝑡 ”⟩ )