Step |
Hyp |
Ref |
Expression |
1 |
|
wrdfn |
⊢ ( 𝑊 ∈ Word 𝑉 → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) |
2 |
1
|
adantr |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) |
3 |
|
oveq2 |
⊢ ( ( ♯ ‘ 𝑊 ) = 3 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ 3 ) ) |
4 |
|
fzo0to3tp |
⊢ ( 0 ..^ 3 ) = { 0 , 1 , 2 } |
5 |
3 4
|
eqtr2di |
⊢ ( ( ♯ ‘ 𝑊 ) = 3 → { 0 , 1 , 2 } = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) |
6 |
5
|
adantl |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) → { 0 , 1 , 2 } = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) |
7 |
6
|
fneq2d |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) → ( 𝑊 Fn { 0 , 1 , 2 } ↔ 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) ) |
8 |
2 7
|
mpbird |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) → 𝑊 Fn { 0 , 1 , 2 } ) |
9 |
|
c0ex |
⊢ 0 ∈ V |
10 |
|
1ex |
⊢ 1 ∈ V |
11 |
|
2ex |
⊢ 2 ∈ V |
12 |
9 10 11
|
fntpb |
⊢ ( 𝑊 Fn { 0 , 1 , 2 } ↔ 𝑊 = { 〈 0 , ( 𝑊 ‘ 0 ) 〉 , 〈 1 , ( 𝑊 ‘ 1 ) 〉 , 〈 2 , ( 𝑊 ‘ 2 ) 〉 } ) |
13 |
8 12
|
sylib |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 3 ) → 𝑊 = { 〈 0 , ( 𝑊 ‘ 0 ) 〉 , 〈 1 , ( 𝑊 ‘ 1 ) 〉 , 〈 2 , ( 𝑊 ‘ 2 ) 〉 } ) |