Theorem s3clhash

Description: Closure of the words of length 3 in a preimage using the hash function. (Contributed by Thierry Arnoux, 27-Sep-2023)

	Ref	Expression
Assertion	s3clhash	$$⊢⟨“IJK”⟩\in {\left|.\right|}^{-1}\left[\left\{3\right\}\right]$$

Proof

Step	Hyp	Ref	Expression
1		s3cli	$$⊢⟨“IJK”⟩\in \mathrm{Word}\mathrm{V}$$
2	1	elexi	$$⊢⟨“IJK”⟩\in \mathrm{V}$$
3		s3len	$$⊢\left|⟨“IJK”⟩\right|=3$$
4		hashf	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$
5		ffn	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}\to \left|.\right|Fn\mathrm{V}$$
6		fniniseg	$$⊢\left|.\right|Fn\mathrm{V}\to \left(⟨“IJK”⟩\in {\left|.\right|}^{-1}\left[\left\{3\right\}\right]\leftrightarrow \left(⟨“IJK”⟩\in \mathrm{V}\wedge \left|⟨“IJK”⟩\right|=3\right)\right)$$
7	4 5 6	mp2b	$$⊢⟨“IJK”⟩\in {\left|.\right|}^{-1}\left[\left\{3\right\}\right]\leftrightarrow \left(⟨“IJK”⟩\in \mathrm{V}\wedge \left|⟨“IJK”⟩\right|=3\right)$$
8	2 3 7	mpbir2an	$$⊢⟨“IJK”⟩\in {\left|.\right|}^{-1}\left[\left\{3\right\}\right]$$