Metamath Proof Explorer

Theorem wrdlen2i

Description: Implications of a word of length two. (Contributed by AV, 27-Jul-2018) (Proof shortened by AV, 14-Oct-2018)

Ref Expression
Assertion wrdlen2i 
|- ( ( 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 c0ex 
 |-  0 e. _V
2 1ex 
 |-  1 e. _V
3 1 2 pm3.2i 
 |-  ( 0 e. _V /\ 1 e. _V )
4 simpl 
 |-  ( ( ( S e. V /\ T e. V ) /\ W = { <. 0 , S >. , <. 1 , T >. } ) -> ( S e. V /\ T e. V ) )
5 0ne1 
 |-  0 =/= 1
6 5 a1i 
 |-  ( ( ( S e. V /\ T e. V ) /\ W = { <. 0 , S >. , <. 1 , T >. } ) -> 0 =/= 1 )
7 fprg 
 |-  ( ( ( 0 e. _V /\ 1 e. _V ) /\ ( S e. V /\ T e. V ) /\ 0 =/= 1 ) -> { <. 0 , S >. , <. 1 , T >. } : { 0 , 1 } --> { S , T } )
8 3 4 6 7 mp3an2i 
 |-  ( ( ( S e. V /\ T e. V ) /\ W = { <. 0 , S >. , <. 1 , T >. } ) -> { <. 0 , S >. , <. 1 , T >. } : { 0 , 1 } --> { S , T } )
9 fzo0to2pr 
 |-  ( 0 ..^ 2 ) = { 0 , 1 }
10 9 eqcomi 
 |-  { 0 , 1 } = ( 0 ..^ 2 )
11 10 a1i 
 |-  ( ( S e. V /\ T e. V ) -> { 0 , 1 } = ( 0 ..^ 2 ) )
12 11 feq2d 
 |-  ( ( S e. V /\ T e. V ) -> ( { <. 0 , S >. , <. 1 , T >. } : { 0 , 1 } --> { S , T } <-> { <. 0 , S >. , <. 1 , T >. } : ( 0 ..^ 2 ) --> { S , T } ) )
13 12 biimpa 
 |-  ( ( ( S e. V /\ T e. V ) /\ { <. 0 , S >. , <. 1 , T >. } : { 0 , 1 } --> { S , T } ) -> { <. 0 , S >. , <. 1 , T >. } : ( 0 ..^ 2 ) --> { S , T } )
14 prssi 
 |-  ( ( S e. V /\ T e. V ) -> { S , T } C_ V )
15 14 adantr 
 |-  ( ( ( S e. V /\ T e. V ) /\ { <. 0 , S >. , <. 1 , T >. } : { 0 , 1 } --> { S , T } ) -> { S , T } C_ V )
16 13 15 fssd 
 |-  ( ( ( S e. V /\ T e. V ) /\ { <. 0 , S >. , <. 1 , T >. } : { 0 , 1 } --> { S , T } ) -> { <. 0 , S >. , <. 1 , T >. } : ( 0 ..^ 2 ) --> V )
17 16 ex 
 |-  ( ( S e. V /\ T e. V ) -> ( { <. 0 , S >. , <. 1 , T >. } : { 0 , 1 } --> { S , T } -> { <. 0 , S >. , <. 1 , T >. } : ( 0 ..^ 2 ) --> V ) )
18 17 adantr 
 |-  ( ( ( S e. V /\ T e. V ) /\ W = { <. 0 , S >. , <. 1 , T >. } ) -> ( { <. 0 , S >. , <. 1 , T >. } : { 0 , 1 } --> { S , T } -> { <. 0 , S >. , <. 1 , T >. } : ( 0 ..^ 2 ) --> V ) )
19 18 impcom 
 |-  ( ( { <. 0 , S >. , <. 1 , T >. } : { 0 , 1 } --> { S , T } /\ ( ( S e. V /\ T e. V ) /\ W = { <. 0 , S >. , <. 1 , T >. } ) ) -> { <. 0 , S >. , <. 1 , T >. } : ( 0 ..^ 2 ) --> V )
20 feq1 
 |-  ( W = { <. 0 , S >. , <. 1 , T >. } -> ( W : ( 0 ..^ 2 ) --> V <-> { <. 0 , S >. , <. 1 , T >. } : ( 0 ..^ 2 ) --> V ) )
21 20 adantl 
 |-  ( ( ( S e. V /\ T e. V ) /\ W = { <. 0 , S >. , <. 1 , T >. } ) -> ( W : ( 0 ..^ 2 ) --> V <-> { <. 0 , S >. , <. 1 , T >. } : ( 0 ..^ 2 ) --> V ) )
22 21 adantl 
 |-  ( ( { <. 0 , S >. , <. 1 , T >. } : { 0 , 1 } --> { S , T } /\ ( ( S e. V /\ T e. V ) /\ W = { <. 0 , S >. , <. 1 , T >. } ) ) -> ( W : ( 0 ..^ 2 ) --> V <-> { <. 0 , S >. , <. 1 , T >. } : ( 0 ..^ 2 ) --> V ) )
23 19 22 mpbird 
 |-  ( ( { <. 0 , S >. , <. 1 , T >. } : { 0 , 1 } --> { S , T } /\ ( ( S e. V /\ T e. V ) /\ W = { <. 0 , S >. , <. 1 , T >. } ) ) -> W : ( 0 ..^ 2 ) --> V )
24 8 23 mpancom 
 |-  ( ( ( S e. V /\ T e. V ) /\ W = { <. 0 , S >. , <. 1 , T >. } ) -> W : ( 0 ..^ 2 ) --> V )
25 iswrdi 
 |-  ( W : ( 0 ..^ 2 ) --> V -> W e. Word V )
26 24 25 syl 
 |-  ( ( ( S e. V /\ T e. V ) /\ W = { <. 0 , S >. , <. 1 , T >. } ) -> W e. Word V )
27 fveq2 
 |-  ( W = { <. 0 , S >. , <. 1 , T >. } -> ( # ` W ) = ( # ` { <. 0 , S >. , <. 1 , T >. } ) )
28 5 neii 
 |-  -. 0 = 1
29 simpl 
 |-  ( ( S e. V /\ T e. V ) -> S e. V )
30 opth1g 
 |-  ( ( 0 e. _V /\ S e. V ) -> ( <. 0 , S >. = <. 1 , T >. -> 0 = 1 ) )
31 1 29 30 sylancr 
 |-  ( ( S e. V /\ T e. V ) -> ( <. 0 , S >. = <. 1 , T >. -> 0 = 1 ) )
32 28 31 mtoi 
 |-  ( ( S e. V /\ T e. V ) -> -. <. 0 , S >. = <. 1 , T >. )
33 32 neqned 
 |-  ( ( S e. V /\ T e. V ) -> <. 0 , S >. =/= <. 1 , T >. )
34 opex 
 |-  <. 0 , S >. e. _V
35 opex 
 |-  <. 1 , T >. e. _V
36 34 35 pm3.2i 
 |-  ( <. 0 , S >. e. _V /\ <. 1 , T >. e. _V )
37 hashprg 
 |-  ( ( <. 0 , S >. e. _V /\ <. 1 , T >. e. _V ) -> ( <. 0 , S >. =/= <. 1 , T >. <-> ( # ` { <. 0 , S >. , <. 1 , T >. } ) = 2 ) )
38 36 37 mp1i 
 |-  ( ( S e. V /\ T e. V ) -> ( <. 0 , S >. =/= <. 1 , T >. <-> ( # ` { <. 0 , S >. , <. 1 , T >. } ) = 2 ) )
39 33 38 mpbid 
 |-  ( ( S e. V /\ T e. V ) -> ( # ` { <. 0 , S >. , <. 1 , T >. } ) = 2 )
40 27 39 sylan9eqr 
 |-  ( ( ( S e. V /\ T e. V ) /\ W = { <. 0 , S >. , <. 1 , T >. } ) -> ( # ` W ) = 2 )
41 5 a1i 
 |-  ( ( S e. V /\ T e. V ) -> 0 =/= 1 )
42 fvpr1g 
 |-  ( ( 0 e. _V /\ S e. V /\ 0 =/= 1 ) -> ( { <. 0 , S >. , <. 1 , T >. } ` 0 ) = S )
43 1 29 41 42 mp3an2i 
 |-  ( ( S e. V /\ T e. V ) -> ( { <. 0 , S >. , <. 1 , T >. } ` 0 ) = S )
44 simpr 
 |-  ( ( S e. V /\ T e. V ) -> T e. V )
45 fvpr2g 
 |-  ( ( 1 e. _V /\ T e. V /\ 0 =/= 1 ) -> ( { <. 0 , S >. , <. 1 , T >. } ` 1 ) = T )
46 2 44 41 45 mp3an2i 
 |-  ( ( S e. V /\ T e. V ) -> ( { <. 0 , S >. , <. 1 , T >. } ` 1 ) = T )
47 43 46 jca 
 |-  ( ( S e. V /\ T e. V ) -> ( ( { <. 0 , S >. , <. 1 , T >. } ` 0 ) = S /\ ( { <. 0 , S >. , <. 1 , T >. } ` 1 ) = T ) )
48 47 adantr 
 |-  ( ( ( S e. V /\ T e. V ) /\ W = { <. 0 , S >. , <. 1 , T >. } ) -> ( ( { <. 0 , S >. , <. 1 , T >. } ` 0 ) = S /\ ( { <. 0 , S >. , <. 1 , T >. } ` 1 ) = T ) )
49 fveq1 
 |-  ( W = { <. 0 , S >. , <. 1 , T >. } -> ( W ` 0 ) = ( { <. 0 , S >. , <. 1 , T >. } ` 0 ) )
50 49 eqeq1d 
 |-  ( W = { <. 0 , S >. , <. 1 , T >. } -> ( ( W ` 0 ) = S <-> ( { <. 0 , S >. , <. 1 , T >. } ` 0 ) = S ) )
51 fveq1 
 |-  ( W = { <. 0 , S >. , <. 1 , T >. } -> ( W ` 1 ) = ( { <. 0 , S >. , <. 1 , T >. } ` 1 ) )
52 51 eqeq1d 
 |-  ( W = { <. 0 , S >. , <. 1 , T >. } -> ( ( W ` 1 ) = T <-> ( { <. 0 , S >. , <. 1 , T >. } ` 1 ) = T ) )
53 50 52 anbi12d 
 |-  ( W = { <. 0 , S >. , <. 1 , T >. } -> ( ( ( W ` 0 ) = S /\ ( W ` 1 ) = T ) <-> ( ( { <. 0 , S >. , <. 1 , T >. } ` 0 ) = S /\ ( { <. 0 , S >. , <. 1 , T >. } ` 1 ) = T ) ) )
54 53 adantl 
 |-  ( ( ( S e. V /\ T e. V ) /\ W = { <. 0 , S >. , <. 1 , T >. } ) -> ( ( ( W ` 0 ) = S /\ ( W ` 1 ) = T ) <-> ( ( { <. 0 , S >. , <. 1 , T >. } ` 0 ) = S /\ ( { <. 0 , S >. , <. 1 , T >. } ` 1 ) = T ) ) )
55 48 54 mpbird 
 |-  ( ( ( S e. V /\ T e. V ) /\ W = { <. 0 , S >. , <. 1 , T >. } ) -> ( ( W ` 0 ) = S /\ ( W ` 1 ) = T ) )
56 26 40 55 jca31 
 |-  ( ( ( S e. V /\ T e. V ) /\ W = { <. 0 , S >. , <. 1 , T >. } ) -> ( ( W e. Word V /\ ( # ` W ) = 2 ) /\ ( ( W ` 0 ) = S /\ ( W ` 1 ) = T ) ) )
57 56 ex 
 |-  ( ( S e. V /\ T e. V ) -> ( W = { <. 0 , S >. , <. 1 , T >. } -> ( ( W e. Word V /\ ( # ` W ) = 2 ) /\ ( ( W ` 0 ) = S /\ ( W ` 1 ) = T ) ) ) )