ssltsepc

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

		Ref	Expression
	Assertion	ssltsepc	$⊢ (A ≪_{s} B \land X \in A \land Y \in B) \to X <_{s} Y$

Step	Hyp	Ref	Expression
1		ssltsep	$⊢ A ≪_{s} B \to \forall x \in A \forall y \in B x <_{s} y$
2		breq1	$⊢ x = X \to (x <_{s} y \leftrightarrow X <_{s} y)$
3		breq2	$⊢ y = Y \to (X <_{s} y \leftrightarrow X <_{s} Y)$
4	2 3	rspc2va	$⊢ ((X \in A \land Y \in B) \land \forall x \in A \forall y \in B x <_{s} y) \to X <_{s} Y$
5	4	ancoms	$⊢ (\forall x \in A \forall y \in B x <_{s} y \land (X \in A \land Y \in B)) \to X <_{s} Y$
6	1 5	sylan	$⊢ (A ≪_{s} B \land (X \in A \land Y \in B)) \to X <_{s} Y$
7	6	3impb	$⊢ (A ≪_{s} B \land X \in A \land Y \in B) \to X <_{s} Y$

Metamath Proof Explorer