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 ‘ ⟨“ 𝑆 ”⟩ ) = ⟨“ 𝑆 ”⟩

Proof

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