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	|- <" I J K "> e. ( `' # " { 3 } )

Proof

Step	Hyp	Ref	Expression
1		s3cli	|- <" I J K "> e. Word _V
2	1	elexi	|- <" I J K "> e. _V
3		s3len	|- ( # ` <" I J K "> ) = 3
4		hashf	|- # : _V --> ( NN0 u. { +oo } )
5		ffn	|- ( # : _V --> ( NN0 u. { +oo } ) -> # Fn _V )
6		fniniseg	|- ( # Fn _V -> ( <" I J K "> e. ( `' # " { 3 } ) <-> ( <" I J K "> e. _V /\ ( # ` <" I J K "> ) = 3 ) ) )
7	4 5 6	mp2b	|- ( <" I J K "> e. ( `' # " { 3 } ) <-> ( <" I J K "> e. _V /\ ( # ` <" I J K "> ) = 3 ) )
8	2 3 7	mpbir2an	|- <" I J K "> e. ( `' # " { 3 } )