Theorem revval

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

	Ref	Expression
Assertion	revval	⊢ ( 𝑊 ∈ 𝑉 → ( reverse ‘ 𝑊 ) = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝑊 ∈ 𝑉 → 𝑊 ∈ V )
2		fveq2	⊢ ( 𝑤 = 𝑊 → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑊 ) )
3	2	oveq2d	⊢ ( 𝑤 = 𝑊 → ( 0 ..^ ( ♯ ‘ 𝑤 ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
4		id	⊢ ( 𝑤 = 𝑊 → 𝑤 = 𝑊 )
5	2	oveq1d	⊢ ( 𝑤 = 𝑊 → ( ( ♯ ‘ 𝑤 ) − 1 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
6	5	oveq1d	⊢ ( 𝑤 = 𝑊 → ( ( ( ♯ ‘ 𝑤 ) − 1 ) − 𝑥 ) = ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) )
7	4 6	fveq12d	⊢ ( 𝑤 = 𝑊 → ( 𝑤 ‘ ( ( ( ♯ ‘ 𝑤 ) − 1 ) − 𝑥 ) ) = ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) )
8	3 7	mpteq12dv	⊢ ( 𝑤 = 𝑊 → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( 𝑤 ‘ ( ( ( ♯ ‘ 𝑤 ) − 1 ) − 𝑥 ) ) ) = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) )
9		df-reverse	⊢ reverse = ( 𝑤 ∈ V ↦ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ↦ ( 𝑤 ‘ ( ( ( ♯ ‘ 𝑤 ) − 1 ) − 𝑥 ) ) ) )
10		ovex	⊢ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∈ V
11	10	mptex	⊢ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) ∈ V
12	8 9 11	fvmpt	⊢ ( 𝑊 ∈ V → ( reverse ‘ 𝑊 ) = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) )
13	1 12	syl	⊢ ( 𝑊 ∈ 𝑉 → ( reverse ‘ 𝑊 ) = ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ↦ ( 𝑊 ‘ ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝑥 ) ) ) )