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

Metamath Proof Explorer

Theorem revcl

Description: The reverse of a word is a word. (Contributed by Stefan O'Rear, 26-Aug-2015)

Ref Expression
Assertion revcl 
|- ( W e. Word A -> ( reverse ` W ) e. Word A )

Proof

Step Hyp Ref Expression
1 revval 
 |-  ( W e. Word A -> ( reverse ` W ) = ( x e. ( 0 ..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) )
2 wrdf 
 |-  ( W e. Word A -> W : ( 0 ..^ ( # ` W ) ) --> A )
3 2 adantr 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> W : ( 0 ..^ ( # ` W ) ) --> A )
4 simpr 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> x e. ( 0 ..^ ( # ` W ) ) )
5 lencl 
 |-  ( W e. Word A -> ( # ` W ) e. NN0 )
6 5 adantr 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( # ` W ) e. NN0 )
7 6 nn0zd 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( # ` W ) e. ZZ )
8 fzoval 
 |-  ( ( # ` W ) e. ZZ -> ( 0 ..^ ( # ` W ) ) = ( 0 ... ( ( # ` W ) - 1 ) ) )
9 7 8 syl 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( 0 ..^ ( # ` W ) ) = ( 0 ... ( ( # ` W ) - 1 ) ) )
10 4 9 eleqtrd 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> x e. ( 0 ... ( ( # ` W ) - 1 ) ) )
11 fznn0sub2 
 |-  ( x e. ( 0 ... ( ( # ` W ) - 1 ) ) -> ( ( ( # ` W ) - 1 ) - x ) e. ( 0 ... ( ( # ` W ) - 1 ) ) )
12 10 11 syl 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( # ` W ) - 1 ) - x ) e. ( 0 ... ( ( # ` W ) - 1 ) ) )
13 12 9 eleqtrrd 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( # ` W ) - 1 ) - x ) e. ( 0 ..^ ( # ` W ) ) )
14 3 13 ffvelcdmd 
 |-  ( ( W e. Word A /\ x e. ( 0 ..^ ( # ` W ) ) ) -> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) e. A )
15 14 fmpttd 
 |-  ( W e. Word A -> ( x e. ( 0 ..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) : ( 0 ..^ ( # ` W ) ) --> A )
16 iswrdi 
 |-  ( ( x e. ( 0 ..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) : ( 0 ..^ ( # ` W ) ) --> A -> ( x e. ( 0 ..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) e. Word A )
17 15 16 syl 
 |-  ( W e. Word A -> ( x e. ( 0 ..^ ( # ` W ) ) |-> ( W ` ( ( ( # ` W ) - 1 ) - x ) ) ) e. Word A )
18 1 17 eqeltrd 
 |-  ( W e. Word A -> ( reverse ` W ) e. Word A )