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∈WordA→reverse⁡W∈WordA

Proof

Step Hyp Ref Expression
1 revval ⊢W∈WordA→reverse⁡W=x∈0..^W⟼W⁡W-1-x
2 wrdf ⊢W∈WordA→W:0..^W⟶A
3 2 adantr ⊢W∈WordA∧x∈0..^W→W:0..^W⟶A
4 simpr ⊢W∈WordA∧x∈0..^W→x∈0..^W
5 lencl ⊢W∈WordA→W∈ℕ0
6 5 adantr ⊢W∈WordA∧x∈0..^W→W∈ℕ0
7 6 nn0zd ⊢W∈WordA∧x∈0..^W→W∈ℤ
8 fzoval ⊢W∈ℤ→0..^W=0…W−1
9 7 8 syl ⊢W∈WordA∧x∈0..^W→0..^W=0…W−1
10 4 9 eleqtrd ⊢W∈WordA∧x∈0..^W→x∈0…W−1
11 fznn0sub2 ⊢x∈0…W−1→W-1-x∈0…W−1
12 10 11 syl ⊢W∈WordA∧x∈0..^W→W-1-x∈0…W−1
13 12 9 eleqtrrd ⊢W∈WordA∧x∈0..^W→W-1-x∈0..^W
14 3 13 ffvelcdmd ⊢W∈WordA∧x∈0..^W→W⁡W-1-x∈A
15 14 fmpttd ⊢W∈WordA→x∈0..^W⟼W⁡W-1-x:0..^W⟶A
16 iswrdi ⊢x∈0..^W⟼W⁡W-1-x:0..^W⟶A→x∈0..^W⟼W⁡W-1-x∈WordA
17 15 16 syl ⊢W∈WordA→x∈0..^W⟼W⁡W-1-x∈WordA
18 1 17 eqeltrd ⊢W∈WordA→reverse⁡W∈WordA