Theorem revval

Description: Value of the word reversing function. (Contributed by Stefan O'Rear, 26-Aug-2015)

	Ref	Expression
Assertion	revval	$$⊢W\in V\to \mathrm{reverse}\left(W\right)=\left(x\in \left(0..^\left|W\right|\right)⟼W\left(\left|W\right|-1-x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢W\in V\to W\in \mathrm{V}$$
2		fveq2	$$⊢w=W\to \left|w\right|=\left|W\right|$$
3	2	oveq2d	$$⊢w=W\to \left(0..^\left|w\right|\right)=\left(0..^\left|W\right|\right)$$
4		id	$$⊢w=W\to w=W$$
5	2	oveq1d	$$⊢w=W\to \left|w\right|-1=\left|W\right|-1$$
6	5	oveq1d	$$⊢w=W\to \left|w\right|-1-x=\left|W\right|-1-x$$
7	4 6	fveq12d	$$⊢w=W\to w\left(\left|w\right|-1-x\right)=W\left(\left|W\right|-1-x\right)$$
8	3 7	mpteq12dv	$$⊢w=W\to \left(x\in \left(0..^\left|w\right|\right)⟼w\left(\left|w\right|-1-x\right)\right)=\left(x\in \left(0..^\left|W\right|\right)⟼W\left(\left|W\right|-1-x\right)\right)$$
9		df-reverse	$$⊢\mathrm{reverse}=\left(w\in \mathrm{V}⟼\left(x\in \left(0..^\left|w\right|\right)⟼w\left(\left|w\right|-1-x\right)\right)\right)$$
10		ovex	$$⊢\left(0..^\left|W\right|\right)\in \mathrm{V}$$
11	10	mptex	$$⊢\left(x\in \left(0..^\left|W\right|\right)⟼W\left(\left|W\right|-1-x\right)\right)\in \mathrm{V}$$
12	8 9 11	fvmpt	$$⊢W\in \mathrm{V}\to \mathrm{reverse}\left(W\right)=\left(x\in \left(0..^\left|W\right|\right)⟼W\left(\left|W\right|-1-x\right)\right)$$
13	1 12	syl	$$⊢W\in V\to \mathrm{reverse}\left(W\right)=\left(x\in \left(0..^\left|W\right|\right)⟼W\left(\left|W\right|-1-x\right)\right)$$