Theorem s3rexrd

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

	Ref	Expression
Hypotheses	s3rexrd.1	$$⊢\phi \to S\in V$$
	s3rexrd.x	$$⊢\phi \to X\in S$$
	s3rexrd.y	$$⊢\phi \to Y\in S$$
	s3rexrd.z	$$⊢\phi \to Z\in S$$
Assertion	s3rexrd	$$⊢\phi \to ⟨“XYZ”⟩\in \left(S^{\left(0..^3\right)}\right)$$

Proof

Step	Hyp	Ref	Expression
1		s3rexrd.1	$$⊢\phi \to S\in V$$
2		s3rexrd.x	$$⊢\phi \to X\in S$$
3		s3rexrd.y	$$⊢\phi \to Y\in S$$
4		s3rexrd.z	$$⊢\phi \to Z\in S$$
5		ovexd	$$⊢\phi \to \left(0..^3\right)\in \mathrm{V}$$
6		s3len	$$⊢\left|⟨“XYZ”⟩\right|=3$$
7	6	a1i	$$⊢\phi \to \left|⟨“XYZ”⟩\right|=3$$
8	7	eqcomd	$$⊢\phi \to 3=\left|⟨“XYZ”⟩\right|$$
9	2 3 4	s3cld	$$⊢\phi \to ⟨“XYZ”⟩\in \mathrm{Word}S$$
10	8 9	wrdfd	$$⊢\phi \to ⟨“XYZ”⟩:\left(0..^3\right)⟶S$$
11	1 5 10	elmapdd	$$⊢\phi \to ⟨“XYZ”⟩\in \left(S^{\left(0..^3\right)}\right)$$