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