Step |
Hyp |
Ref |
Expression |
1 |
|
wrdlen2i |
⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) → ( 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 2 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑆 ∧ ( 𝑊 ‘ 1 ) = 𝑇 ) ) ) ) |
2 |
|
wrd2pr2op |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 2 ) → 𝑊 = { ⟨ 0 , ( 𝑊 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑊 ‘ 1 ) ⟩ } ) |
3 |
|
opeq2 |
⊢ ( ( 𝑊 ‘ 0 ) = 𝑆 → ⟨ 0 , ( 𝑊 ‘ 0 ) ⟩ = ⟨ 0 , 𝑆 ⟩ ) |
4 |
3
|
adantr |
⊢ ( ( ( 𝑊 ‘ 0 ) = 𝑆 ∧ ( 𝑊 ‘ 1 ) = 𝑇 ) → ⟨ 0 , ( 𝑊 ‘ 0 ) ⟩ = ⟨ 0 , 𝑆 ⟩ ) |
5 |
|
opeq2 |
⊢ ( ( 𝑊 ‘ 1 ) = 𝑇 → ⟨ 1 , ( 𝑊 ‘ 1 ) ⟩ = ⟨ 1 , 𝑇 ⟩ ) |
6 |
5
|
adantl |
⊢ ( ( ( 𝑊 ‘ 0 ) = 𝑆 ∧ ( 𝑊 ‘ 1 ) = 𝑇 ) → ⟨ 1 , ( 𝑊 ‘ 1 ) ⟩ = ⟨ 1 , 𝑇 ⟩ ) |
7 |
4 6
|
preq12d |
⊢ ( ( ( 𝑊 ‘ 0 ) = 𝑆 ∧ ( 𝑊 ‘ 1 ) = 𝑇 ) → { ⟨ 0 , ( 𝑊 ‘ 0 ) ⟩ , ⟨ 1 , ( 𝑊 ‘ 1 ) ⟩ } = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ) |
8 |
2 7
|
sylan9eq |
⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 2 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑆 ∧ ( 𝑊 ‘ 1 ) = 𝑇 ) ) → 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ) |
9 |
1 8
|
impbid1 |
⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) → ( 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 2 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑆 ∧ ( 𝑊 ‘ 1 ) = 𝑇 ) ) ) ) |