This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) → ∃ 𝑠 ∈ 𝑆 ∃ 𝑡 ∈ 𝑆 𝑊 = ⟨“ 𝑠 𝑡 ”⟩ )