Theorem s3rexrd

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

	Ref	Expression
Hypotheses	s3rexrd.1	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	s3rexrd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
	s3rexrd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
	s3rexrd.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑆 )
Assertion	s3rexrd	⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( 𝑆 ↑m ( 0 ..^ 3 ) ) )

Proof

Step	Hyp	Ref	Expression
1		s3rexrd.1	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
2		s3rexrd.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
3		s3rexrd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
4		s3rexrd.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑆 )
5		ovexd	⊢ ( 𝜑 → ( 0 ..^ 3 ) ∈ V )
6		s3len	⊢ ( ♯ ‘ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) = 3
7	6	a1i	⊢ ( 𝜑 → ( ♯ ‘ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) = 3 )
8	7	eqcomd	⊢ ( 𝜑 → 3 = ( ♯ ‘ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ) )
9	2 3 4	s3cld	⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ Word 𝑆 )
10	8 9	wrdfd	⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ : ( 0 ..^ 3 ) ⟶ 𝑆 )
11	1 5 10	elmapdd	⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∈ ( 𝑆 ↑m ( 0 ..^ 3 ) ) )