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 ⊢ W ∈ Word S ∧ W = 2 → ∃ s ∈ S ∃ t ∈ S W = ⟨“ st ”⟩

Proof

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