Theorem ssltsepcd

Description: Two elements of separated sets obey less-than. Deduction form of ssltsepc . (Contributed by Scott Fenton, 25-Sep-2024)

	Ref	Expression
Hypotheses	ssltsepcd.1	⊢ ( 𝜑 → 𝐴 <<s 𝐵 )
	ssltsepcd.2	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	ssltsepcd.3	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	ssltsepcd	⊢ ( 𝜑 → 𝑋 <s 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		ssltsepcd.1	⊢ ( 𝜑 → 𝐴 <<s 𝐵 )
2		ssltsepcd.2	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
3		ssltsepcd.3	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
4		ssltsepc	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 <s 𝑌 )
5	1 2 3 4	syl3anc	⊢ ( 𝜑 → 𝑋 <s 𝑌 )