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	⊢ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ∈ ( ◡ ♯ “ { 3 } )

Proof

Step	Hyp	Ref	Expression
1		s3cli	⊢ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ∈ Word V
2	1	elexi	⊢ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ∈ V
3		s3len	⊢ ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) = 3
4		hashf	⊢ ♯ : V ⟶ ( ℕ0 ∪ { +∞ } )
5		ffn	⊢ ( ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) → ♯ Fn V )
6		fniniseg	⊢ ( ♯ Fn V → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ∈ ( ◡ ♯ “ { 3 } ) ↔ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ∈ V ∧ ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) = 3 ) ) )
7	4 5 6	mp2b	⊢ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ∈ ( ◡ ♯ “ { 3 } ) ↔ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ∈ V ∧ ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) = 3 ) )
8	2 3 7	mpbir2an	⊢ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ∈ ( ◡ ♯ “ { 3 } )