Theorem s2rn

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

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

Proof

Step	Hyp	Ref	Expression
1		s2rn.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
2		s2rn.j	⊢ ( 𝜑 → 𝐽 ∈ 𝐷 )
3		imadmrn	⊢ ( ⟨“ 𝐼 𝐽 ”⟩ “ dom ⟨“ 𝐼 𝐽 ”⟩ ) = ran ⟨“ 𝐼 𝐽 ”⟩
4	1 2	s2cld	⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ ∈ Word 𝐷 )
5		wrdfn	⊢ ( ⟨“ 𝐼 𝐽 ”⟩ ∈ Word 𝐷 → ⟨“ 𝐼 𝐽 ”⟩ Fn ( 0 ..^ ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ) )
6		s2len	⊢ ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) = 2
7	6	oveq2i	⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ) = ( 0 ..^ 2 )
8		fzo0to2pr	⊢ ( 0 ..^ 2 ) = { 0 , 1 }
9	7 8	eqtri	⊢ ( 0 ..^ ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ) = { 0 , 1 }
10	9	fneq2i	⊢ ( ⟨“ 𝐼 𝐽 ”⟩ Fn ( 0 ..^ ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ) ↔ ⟨“ 𝐼 𝐽 ”⟩ Fn { 0 , 1 } )
11	10	biimpi	⊢ ( ⟨“ 𝐼 𝐽 ”⟩ Fn ( 0 ..^ ( ♯ ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ) → ⟨“ 𝐼 𝐽 ”⟩ Fn { 0 , 1 } )
12	4 5 11	3syl	⊢ ( 𝜑 → ⟨“ 𝐼 𝐽 ”⟩ Fn { 0 , 1 } )
13	12	fndmd	⊢ ( 𝜑 → dom ⟨“ 𝐼 𝐽 ”⟩ = { 0 , 1 } )
14	13	imaeq2d	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 ”⟩ “ dom ⟨“ 𝐼 𝐽 ”⟩ ) = ( ⟨“ 𝐼 𝐽 ”⟩ “ { 0 , 1 } ) )
15		c0ex	⊢ 0 ∈ V
16	15	prid1	⊢ 0 ∈ { 0 , 1 }
17	16	a1i	⊢ ( 𝜑 → 0 ∈ { 0 , 1 } )
18		1ex	⊢ 1 ∈ V
19	18	prid2	⊢ 1 ∈ { 0 , 1 }
20	19	a1i	⊢ ( 𝜑 → 1 ∈ { 0 , 1 } )
21		fnimapr	⊢ ( ( ⟨“ 𝐼 𝐽 ”⟩ Fn { 0 , 1 } ∧ 0 ∈ { 0 , 1 } ∧ 1 ∈ { 0 , 1 } ) → ( ⟨“ 𝐼 𝐽 ”⟩ “ { 0 , 1 } ) = { ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 0 ) , ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 1 ) } )
22	12 17 20 21	syl3anc	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 ”⟩ “ { 0 , 1 } ) = { ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 0 ) , ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 1 ) } )
23		s2fv0	⊢ ( 𝐼 ∈ 𝐷 → ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 0 ) = 𝐼 )
24	1 23	syl	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 0 ) = 𝐼 )
25		s2fv1	⊢ ( 𝐽 ∈ 𝐷 → ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 1 ) = 𝐽 )
26	2 25	syl	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 1 ) = 𝐽 )
27	24 26	preq12d	⊢ ( 𝜑 → { ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 0 ) , ( ⟨“ 𝐼 𝐽 ”⟩ ‘ 1 ) } = { 𝐼 , 𝐽 } )
28	14 22 27	3eqtrd	⊢ ( 𝜑 → ( ⟨“ 𝐼 𝐽 ”⟩ “ dom ⟨“ 𝐼 𝐽 ”⟩ ) = { 𝐼 , 𝐽 } )
29	3 28	eqtr3id	⊢ ( 𝜑 → ran ⟨“ 𝐼 𝐽 ”⟩ = { 𝐼 , 𝐽 } )