Theorem rev0

Description: The empty word is its own reverse. (Contributed by Stefan O'Rear, 26-Aug-2015)

	Ref	Expression
Assertion	rev0	$$⊢\mathrm{reverse}\left(\varnothing \right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		wrd0	$$⊢\varnothing \in \mathrm{Word}\mathrm{V}$$
2		revlen	$$⊢\varnothing \in \mathrm{Word}\mathrm{V}\to \left|\mathrm{reverse}\left(\varnothing \right)\right|=\left|\varnothing \right|$$
3	1 2	ax-mp	$$⊢\left|\mathrm{reverse}\left(\varnothing \right)\right|=\left|\varnothing \right|$$
4		hash0	$$⊢\left|\varnothing \right|=0$$
5	3 4	eqtri	$$⊢\left|\mathrm{reverse}\left(\varnothing \right)\right|=0$$
6		fvex	$$⊢\mathrm{reverse}\left(\varnothing \right)\in \mathrm{V}$$
7		hasheq0	$$⊢\mathrm{reverse}\left(\varnothing \right)\in \mathrm{V}\to \left(\left|\mathrm{reverse}\left(\varnothing \right)\right|=0\leftrightarrow \mathrm{reverse}\left(\varnothing \right)=\varnothing \right)$$
8	6 7	ax-mp	$$⊢\left|\mathrm{reverse}\left(\varnothing \right)\right|=0\leftrightarrow \mathrm{reverse}\left(\varnothing \right)=\varnothing$$
9	5 8	mpbi	$$⊢\mathrm{reverse}\left(\varnothing \right)=\varnothing$$