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 ⊢ W ∈ V → reverse ⁡ W = x ∈ 0 ..^ W ⟼ W ⁡ W - 1 - x

Proof

Step Hyp Ref Expression
1 elex ⊢ W ∈ V → W ∈ V
2 fveq2 ⊢ w = W → w = W
3 2 oveq2d ⊢ w = W → 0 ..^ w = 0 ..^ W
4 id ⊢ w = W → w = W
5 2 oveq1d ⊢ w = W → w − 1 = W − 1
6 5 oveq1d ⊢ w = W → w - 1 - x = W - 1 - x
7 4 6 fveq12d ⊢ w = W → w ⁡ w - 1 - x = W ⁡ W - 1 - x
8 3 7 mpteq12dv ⊢ w = W → x ∈ 0 ..^ w ⟼ w ⁡ w - 1 - x = x ∈ 0 ..^ W ⟼ W ⁡ W - 1 - x
9 df-reverse ⊢ reverse = w ∈ V ⟼ x ∈ 0 ..^ w ⟼ w ⁡ w - 1 - x
10 ovex ⊢ 0 ..^ W ∈ V
11 10 mptex ⊢ x ∈ 0 ..^ W ⟼ W ⁡ W - 1 - x ∈ V
12 8 9 11 fvmpt ⊢ W ∈ V → reverse ⁡ W = x ∈ 0 ..^ W ⟼ W ⁡ W - 1 - x
13 1 12 syl ⊢ W ∈ V → reverse ⁡ W = x ∈ 0 ..^ W ⟼ W ⁡ W - 1 - x