Metamath Proof Explorer

Theorem wrdlen2

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

Ref Expression
Assertion wrdlen2 
|- ( ( S e. V /\ T e. V ) -> ( W = { <. 0 , S >. , <. 1 , T >. } <-> ( ( W e. Word V /\ ( # ` W ) = 2 ) /\ ( ( W ` 0 ) = S /\ ( W ` 1 ) = T ) ) ) )

Proof

Step Hyp Ref Expression
1 wrdlen2i 
 |-  ( ( S e. V /\ T e. V ) -> ( W = { <. 0 , S >. , <. 1 , T >. } -> ( ( W e. Word V /\ ( # ` W ) = 2 ) /\ ( ( W ` 0 ) = S /\ ( W ` 1 ) = T ) ) ) )
2 wrd2pr2op 
 |-  ( ( W e. Word V /\ ( # ` W ) = 2 ) -> W = { <. 0 , ( W ` 0 ) >. , <. 1 , ( W ` 1 ) >. } )
3 opeq2 
 |-  ( ( W ` 0 ) = S -> <. 0 , ( W ` 0 ) >. = <. 0 , S >. )
4 3 adantr 
 |-  ( ( ( W ` 0 ) = S /\ ( W ` 1 ) = T ) -> <. 0 , ( W ` 0 ) >. = <. 0 , S >. )
5 opeq2 
 |-  ( ( W ` 1 ) = T -> <. 1 , ( W ` 1 ) >. = <. 1 , T >. )
6 5 adantl 
 |-  ( ( ( W ` 0 ) = S /\ ( W ` 1 ) = T ) -> <. 1 , ( W ` 1 ) >. = <. 1 , T >. )
7 4 6 preq12d 
 |-  ( ( ( W ` 0 ) = S /\ ( W ` 1 ) = T ) -> { <. 0 , ( W ` 0 ) >. , <. 1 , ( W ` 1 ) >. } = { <. 0 , S >. , <. 1 , T >. } )
8 2 7 sylan9eq 
 |-  ( ( ( W e. Word V /\ ( # ` W ) = 2 ) /\ ( ( W ` 0 ) = S /\ ( W ` 1 ) = T ) ) -> W = { <. 0 , S >. , <. 1 , T >. } )
9 1 8 impbid1 
 |-  ( ( S e. V /\ T e. V ) -> ( W = { <. 0 , S >. , <. 1 , T >. } <-> ( ( W e. Word V /\ ( # ` W ) = 2 ) /\ ( ( W ` 0 ) = S /\ ( W ` 1 ) = T ) ) ) )