Theorem sltssepcd

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

	Ref	Expression
Hypotheses	sltssepcd.1	$$⊢\phi \to A{\ll }_{s}B$$
	sltssepcd.2	$$⊢\phi \to X\in A$$
	sltssepcd.3	$$⊢\phi \to Y\in B$$
Assertion	sltssepcd	$$⊢\phi \to X{<}_{s}Y$$

Proof

Step	Hyp	Ref	Expression
1		sltssepcd.1	$$⊢\phi \to A{\ll }_{s}B$$
2		sltssepcd.2	$$⊢\phi \to X\in A$$
3		sltssepcd.3	$$⊢\phi \to Y\in B$$
4		sltssepc	$$⊢\left(A{\ll }_{s}B\wedge X\in A\wedge Y\in B\right)\to X{<}_{s}Y$$
5	1 2 3 4	syl3anc	$$⊢\phi \to X{<}_{s}Y$$