Metamath Proof Explorer

Theorem revs1

Description: Singleton words are their own reverses. (Contributed by Stefan O'Rear, 26-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion revs1 ⊢reverse⁡⟨“S”⟩=⟨“S”⟩

Proof

Step Hyp Ref Expression
1 s1cli ⊢⟨“S”⟩∈WordV
2 s1len ⊢⟨“S”⟩=1
3 1nn ⊢1∈ℕ
4 2 3 eqeltri ⊢⟨“S”⟩∈ℕ
5 lbfzo0 ⊢0∈0..^⟨“S”⟩↔⟨“S”⟩∈ℕ
6 4 5 mpbir ⊢0∈0..^⟨“S”⟩
7 revfv ⊢⟨“S”⟩∈WordV∧0∈0..^⟨“S”⟩→reverse⁡⟨“S”⟩⁡0=⟨“S”⟩⁡⟨“S”⟩-1-0
8 1 6 7 mp2an ⊢reverse⁡⟨“S”⟩⁡0=⟨“S”⟩⁡⟨“S”⟩-1-0
9 2 oveq1i ⊢⟨“S”⟩−1=1−1
10 1m1e0 ⊢1−1=0
11 9 10 eqtri ⊢⟨“S”⟩−1=0
12 11 oveq1i ⊢⟨“S”⟩-1-0=0−0
13 0m0e0 ⊢0−0=0
14 12 13 eqtri ⊢⟨“S”⟩-1-0=0
15 14 fveq2i ⊢⟨“S”⟩⁡⟨“S”⟩-1-0=⟨“S”⟩⁡0
16 ids1 ⊢⟨“S”⟩=⟨“I⁡S”⟩
17 16 fveq1i ⊢⟨“S”⟩⁡0=⟨“I⁡S”⟩⁡0
18 fvex ⊢I⁡S∈V
19 s1fv ⊢I⁡S∈V→⟨“I⁡S”⟩⁡0=I⁡S
20 18 19 ax-mp ⊢⟨“I⁡S”⟩⁡0=I⁡S
21 17 20 eqtri ⊢⟨“S”⟩⁡0=I⁡S
22 15 21 eqtri ⊢⟨“S”⟩⁡⟨“S”⟩-1-0=I⁡S
23 8 22 eqtri ⊢reverse⁡⟨“S”⟩⁡0=I⁡S
24 s1eq ⊢reverse⁡⟨“S”⟩⁡0=I⁡S→⟨“reverse⁡⟨“S”⟩⁡0”⟩=⟨“I⁡S”⟩
25 23 24 ax-mp ⊢⟨“reverse⁡⟨“S”⟩⁡0”⟩=⟨“I⁡S”⟩
26 revcl ⊢⟨“S”⟩∈WordV→reverse⁡⟨“S”⟩∈WordV
27 1 26 ax-mp ⊢reverse⁡⟨“S”⟩∈WordV
28 revlen ⊢⟨“S”⟩∈WordV→reverse⁡⟨“S”⟩=⟨“S”⟩
29 1 28 ax-mp ⊢reverse⁡⟨“S”⟩=⟨“S”⟩
30 29 2 eqtri ⊢reverse⁡⟨“S”⟩=1
31 eqs1 ⊢reverse⁡⟨“S”⟩∈WordV∧reverse⁡⟨“S”⟩=1→reverse⁡⟨“S”⟩=⟨“reverse⁡⟨“S”⟩⁡0”⟩
32 27 30 31 mp2an ⊢reverse⁡⟨“S”⟩=⟨“reverse⁡⟨“S”⟩⁡0”⟩
33 25 32 16 3eqtr4i ⊢reverse⁡⟨“S”⟩=⟨“S”⟩