Theorem ssltsepc

Description: Two elements of separated sets obey less-than. (Contributed by Scott Fenton, 20-Aug-2024)

	Ref	Expression
Assertion	ssltsepc	|- ( ( A < X

Proof

Step	Hyp	Ref	Expression
1		ssltsep	|- ( A < A. x e. A A. y e. B x
2		breq1	|- ( x = X -> ( x X
3		breq2	|- ( y = Y -> ( X X
4	2 3	rspc2va	|- ( ( ( X e. A /\ Y e. B ) /\ A. x e. A A. y e. B x X
5	4	ancoms	|- ( ( A. x e. A A. y e. B x X
6	1 5	sylan	|- ( ( A < X
7	6	3impb	|- ( ( A < X