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