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