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