s3rnOLD

Description: Obsolete version of s2rn as of 1-Aug-2025. Range of a length 3 string. (Contributed by Thierry Arnoux, 19-Sep-2023) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	s3rnOLD.i	\|- ( ph -> I e. D )
	s3rnOLD.j	\|- ( ph -> J e. D )
	s3rnOLD.k	\|- ( ph -> K e. D )
Assertion	s3rnOLD	\|- ( ph -> ran <" I J K "> = { I , J , K } )

Proof

Step	Hyp	Ref	Expression
1		s3rnOLD.i	\|- ( ph -> I e. D )
2		s3rnOLD.j	\|- ( ph -> J e. D )
3		s3rnOLD.k	\|- ( ph -> K e. D )
4		imadmrn	\|- ( <" I J K "> " dom <" I J K "> ) = ran <" I J K ">
5	1 2 3	s3cld	\|- ( ph -> <" I J K "> e. Word D )
6		wrdfn	\|- ( <" I J K "> e. Word D -> <" I J K "> Fn ( 0 ..^ ( # ` <" I J K "> ) ) )
7		s3len	\|- ( # ` <" I J K "> ) = 3
8	7	oveq2i	\|- ( 0 ..^ ( # ` <" I J K "> ) ) = ( 0 ..^ 3 )
9		fzo0to3tp	\|- ( 0 ..^ 3 ) = { 0 , 1 , 2 }
10	8 9	eqtri	\|- ( 0 ..^ ( # ` <" I J K "> ) ) = { 0 , 1 , 2 }
11	10	fneq2i	\|- ( <" I J K "> Fn ( 0 ..^ ( # ` <" I J K "> ) ) <-> <" I J K "> Fn { 0 , 1 , 2 } )
12	11	biimpi	\|- ( <" I J K "> Fn ( 0 ..^ ( # ` <" I J K "> ) ) -> <" I J K "> Fn { 0 , 1 , 2 } )
13	5 6 12	3syl	\|- ( ph -> <" I J K "> Fn { 0 , 1 , 2 } )
14	13	fndmd	\|- ( ph -> dom <" I J K "> = { 0 , 1 , 2 } )
15	14	imaeq2d	\|- ( ph -> ( <" I J K "> " dom <" I J K "> ) = ( <" I J K "> " { 0 , 1 , 2 } ) )
16		c0ex	\|- 0 e. _V
17	16	tpid1	\|- 0 e. { 0 , 1 , 2 }
18	17	a1i	\|- ( ph -> 0 e. { 0 , 1 , 2 } )
19		1ex	\|- 1 e. _V
20	19	tpid2	\|- 1 e. { 0 , 1 , 2 }
21	20	a1i	\|- ( ph -> 1 e. { 0 , 1 , 2 } )
22		2ex	\|- 2 e. _V
23	22	tpid3	\|- 2 e. { 0 , 1 , 2 }
24	23	a1i	\|- ( ph -> 2 e. { 0 , 1 , 2 } )
25	13 18 21 24	fnimatpd	\|- ( ph -> ( <" I J K "> " { 0 , 1 , 2 } ) = { ( <" I J K "> ` 0 ) , ( <" I J K "> ` 1 ) , ( <" I J K "> ` 2 ) } )
26		s3fv0	\|- ( I e. D -> ( <" I J K "> ` 0 ) = I )
27	1 26	syl	\|- ( ph -> ( <" I J K "> ` 0 ) = I )
28		s3fv1	\|- ( J e. D -> ( <" I J K "> ` 1 ) = J )
29	2 28	syl	\|- ( ph -> ( <" I J K "> ` 1 ) = J )
30		s3fv2	\|- ( K e. D -> ( <" I J K "> ` 2 ) = K )
31	3 30	syl	\|- ( ph -> ( <" I J K "> ` 2 ) = K )
32	27 29 31	tpeq123d	\|- ( ph -> { ( <" I J K "> ` 0 ) , ( <" I J K "> ` 1 ) , ( <" I J K "> ` 2 ) } = { I , J , K } )
33	15 25 32	3eqtrd	\|- ( ph -> ( <" I J K "> " dom <" I J K "> ) = { I , J , K } )
34	4 33	eqtr3id	\|- ( ph -> ran <" I J K "> = { I , J , K } )

Metamath Proof Explorer

Theorem s3rnOLD

Proof