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

Metamath Proof Explorer

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 ) − 𝑥 ) ) ) )