Step |
Hyp |
Ref |
Expression |
1 |
|
s1cl |
⊢ ( 𝑆 ∈ 𝑉 → 〈“ 𝑆 ”〉 ∈ Word 𝑉 ) |
2 |
|
s1len |
⊢ ( ♯ ‘ 〈“ 𝑆 ”〉 ) = 1 |
3 |
2
|
a1i |
⊢ ( 𝑆 ∈ 𝑉 → ( ♯ ‘ 〈“ 𝑆 ”〉 ) = 1 ) |
4 |
|
s1fv |
⊢ ( 𝑆 ∈ 𝑉 → ( 〈“ 𝑆 ”〉 ‘ 0 ) = 𝑆 ) |
5 |
1 3 4
|
3jca |
⊢ ( 𝑆 ∈ 𝑉 → ( 〈“ 𝑆 ”〉 ∈ Word 𝑉 ∧ ( ♯ ‘ 〈“ 𝑆 ”〉 ) = 1 ∧ ( 〈“ 𝑆 ”〉 ‘ 0 ) = 𝑆 ) ) |
6 |
|
eleq1 |
⊢ ( 𝑊 = 〈“ 𝑆 ”〉 → ( 𝑊 ∈ Word 𝑉 ↔ 〈“ 𝑆 ”〉 ∈ Word 𝑉 ) ) |
7 |
|
fveqeq2 |
⊢ ( 𝑊 = 〈“ 𝑆 ”〉 → ( ( ♯ ‘ 𝑊 ) = 1 ↔ ( ♯ ‘ 〈“ 𝑆 ”〉 ) = 1 ) ) |
8 |
|
fveq1 |
⊢ ( 𝑊 = 〈“ 𝑆 ”〉 → ( 𝑊 ‘ 0 ) = ( 〈“ 𝑆 ”〉 ‘ 0 ) ) |
9 |
8
|
eqeq1d |
⊢ ( 𝑊 = 〈“ 𝑆 ”〉 → ( ( 𝑊 ‘ 0 ) = 𝑆 ↔ ( 〈“ 𝑆 ”〉 ‘ 0 ) = 𝑆 ) ) |
10 |
6 7 9
|
3anbi123d |
⊢ ( 𝑊 = 〈“ 𝑆 ”〉 → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ∧ ( 𝑊 ‘ 0 ) = 𝑆 ) ↔ ( 〈“ 𝑆 ”〉 ∈ Word 𝑉 ∧ ( ♯ ‘ 〈“ 𝑆 ”〉 ) = 1 ∧ ( 〈“ 𝑆 ”〉 ‘ 0 ) = 𝑆 ) ) ) |
11 |
5 10
|
syl5ibrcom |
⊢ ( 𝑆 ∈ 𝑉 → ( 𝑊 = 〈“ 𝑆 ”〉 → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ∧ ( 𝑊 ‘ 0 ) = 𝑆 ) ) ) |
12 |
|
eqs1 |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ) → 𝑊 = 〈“ ( 𝑊 ‘ 0 ) ”〉 ) |
13 |
|
s1eq |
⊢ ( ( 𝑊 ‘ 0 ) = 𝑆 → 〈“ ( 𝑊 ‘ 0 ) ”〉 = 〈“ 𝑆 ”〉 ) |
14 |
13
|
eqeq2d |
⊢ ( ( 𝑊 ‘ 0 ) = 𝑆 → ( 𝑊 = 〈“ ( 𝑊 ‘ 0 ) ”〉 ↔ 𝑊 = 〈“ 𝑆 ”〉 ) ) |
15 |
12 14
|
syl5ibcom |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( ( 𝑊 ‘ 0 ) = 𝑆 → 𝑊 = 〈“ 𝑆 ”〉 ) ) |
16 |
15
|
3impia |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ∧ ( 𝑊 ‘ 0 ) = 𝑆 ) → 𝑊 = 〈“ 𝑆 ”〉 ) |
17 |
11 16
|
impbid1 |
⊢ ( 𝑆 ∈ 𝑉 → ( 𝑊 = 〈“ 𝑆 ”〉 ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 1 ∧ ( 𝑊 ‘ 0 ) = 𝑆 ) ) ) |