This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wrdlen2

Description: A word of length two. (Contributed by AV, 20-Oct-2018)

Ref Expression
Assertion wrdlen2 ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) → ( 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ↔ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 2 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑆 ∧ ( 𝑊 ‘ 1 ) = 𝑇 ) ) ) )

Proof

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 ) = 𝑇 ) ) ) )