Theorem s3rn

Description: Range of a length 3 string. (Contributed by Thierry Arnoux, 19-Sep-2023)

	Ref	Expression
Hypotheses	s3rn.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
	s3rn.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
	s3rn.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐷 )
Assertion	s3rn	⊢ ( 𝜑 → ran ⟨“ 𝐼 𝐽 𝐾 ”⟩ = { 𝐼 , 𝐽 , 𝐾 } )

Proof

Step	Hyp	Ref	Expression
1		s3rn.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
2		s3rn.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
3		s3rn.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐷 )
4		imadmrn	⊢ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ “ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) = ran ⟨“ 𝐼 𝐽 𝐾 ”⟩
5	1 2 3	s3cld	⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 𝐾 ”⟩ ∈ Word 𝐷 )
6		wrdfn	⊢ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ∈ Word 𝐷 → ⟨“ 𝐼 𝐽 𝐾 ”⟩ Fn ( 0 ..^ ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ) )
7		s3len	⊢ ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) = 3
8	7	oveq2i	⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ) = ( 0 ..^ 3 )
9		fzo0to3tp	⊢ ( 0 ..^ 3 ) = { 0 , 1 , 2 }
10	8 9	eqtri	⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ) = { 0 , 1 , 2 }
11	10	fneq2i	⊢ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ Fn ( 0 ..^ ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ) ↔ ⟨“ 𝐼 𝐽 𝐾 ”⟩ Fn { 0 , 1 , 2 } )
12	11	biimpi	⊢ ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ Fn ( 0 ..^ ( ♯ ‘ ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) ) → ⟨“ 𝐼 𝐽 𝐾 ”⟩ Fn { 0 , 1 , 2 } )
13	5 6 12	3syl	⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 𝐾 ”⟩ Fn { 0 , 1 , 2 } )
14	13	fndmd	⊢ ( 𝜑 → dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ = { 0 , 1 , 2 } )
15	14	imaeq2d	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ “ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) = ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ “ { 0 , 1 , 2 } ) )
16		c0ex	⊢ 0 ∈ V
17	16	tpid1	⊢ 0 ∈ { 0 , 1 , 2 }
18	17	a1i	⊢ ( 𝜑 → 0 ∈ { 0 , 1 , 2 } )
19		1ex	⊢ 1 ∈ V
20	19	tpid2	⊢ 1 ∈ { 0 , 1 , 2 }
21	20	a1i	⊢ ( 𝜑 → 1 ∈ { 0 , 1 , 2 } )
22		2ex	⊢ 2 ∈ V
23	22	tpid3	⊢ 2 ∈ { 0 , 1 , 2 }
24	23	a1i	⊢ ( 𝜑 → 2 ∈ { 0 , 1 , 2 } )
25	13 18 21 24	fnimatp	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ “ { 0 , 1 , 2 } ) = { ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 0 ) , ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 1 ) , ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 2 ) } )
26		s3fv0	⊢ ( 𝐼 ∈ 𝐷 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 0 ) = 𝐼 )
27	1 26	syl	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 0 ) = 𝐼 )
28		s3fv1	⊢ ( 𝐽 ∈ 𝐷 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 1 ) = 𝐽 )
29	2 28	syl	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 1 ) = 𝐽 )
30		s3fv2	⊢ ( 𝐾 ∈ 𝐷 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 2 ) = 𝐾 )
31	3 30	syl	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 2 ) = 𝐾 )
32	27 29 31	tpeq123d	⊢ ( 𝜑 → { ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 0 ) , ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 1 ) , ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ ‘ 2 ) } = { 𝐼 , 𝐽 , 𝐾 } )
33	15 25 32	3eqtrd	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 𝐾 ”⟩ “ dom ⟨“ 𝐼 𝐽 𝐾 ”⟩ ) = { 𝐼 , 𝐽 , 𝐾 } )
34	4 33	eqtr3id	⊢ ( 𝜑 → ran ⟨“ 𝐼 𝐽 𝐾 ”⟩ = { 𝐼 , 𝐽 , 𝐾 } )