Theorem s3rexrd

Description: Converse of s3rex , deduction form. (Contributed by Thierry Arnoux, 23-Aug-2026)

	Ref	Expression
Hypotheses	s3rexrd.1	|- ( ph -> S e. V )
	s3rexrd.x	|- ( ph -> X e. S )
	s3rexrd.y	|- ( ph -> Y e. S )
	s3rexrd.z	|- ( ph -> Z e. S )
Assertion	s3rexrd	|- ( ph -> <" X Y Z "> e. ( S ^m ( 0 ..^ 3 ) ) )

Proof

Step	Hyp	Ref	Expression
1		s3rexrd.1	|- ( ph -> S e. V )
2		s3rexrd.x	|- ( ph -> X e. S )
3		s3rexrd.y	|- ( ph -> Y e. S )
4		s3rexrd.z	|- ( ph -> Z e. S )
5		ovexd	|- ( ph -> ( 0 ..^ 3 ) e. _V )
6		s3len	|- ( # ` <" X Y Z "> ) = 3
7	6	a1i	|- ( ph -> ( # ` <" X Y Z "> ) = 3 )
8	7	eqcomd	|- ( ph -> 3 = ( # ` <" X Y Z "> ) )
9	2 3 4	s3cld	|- ( ph -> <" X Y Z "> e. Word S )
10	8 9	wrdfd	|- ( ph -> <" X Y Z "> : ( 0 ..^ 3 ) --> S )
11	1 5 10	elmapdd	|- ( ph -> <" X Y Z "> e. ( S ^m ( 0 ..^ 3 ) ) )