sltn0

Description: If X is less than Y , then either (LeftY ) or ( RightX ) is non-empty. (Contributed by Scott Fenton, 10-Dec-2024)

		Ref	Expression
	Assertion	sltn0	$⊢ (X \in No \land Y \in No \land X <_{s} Y) \to (L (Y) \neq \emptyset \lor R (X) \neq \emptyset)$

Step	Hyp	Ref	Expression
1		lltropt	$⊢ L (X) ≪_{s} R (X)$
2	1	a1i	$⊢ (X \in No \land Y \in No) \to L (X) ≪_{s} R (X)$
3		lltropt	$⊢ L (Y) ≪_{s} R (Y)$
4	3	a1i	$⊢ (X \in No \land Y \in No) \to L (Y) ≪_{s} R (Y)$
5		lrcut	$⊢ X \in No \to L (X) \|_{s} R (X) = X$
6	5	eqcomd	$⊢ X \in No \to X = L (X) \|_{s} R (X)$
7	6	adantr	$⊢ (X \in No \land Y \in No) \to X = L (X) \|_{s} R (X)$
8		lrcut	$⊢ Y \in No \to L (Y) \|_{s} R (Y) = Y$
9	8	eqcomd	$⊢ Y \in No \to Y = L (Y) \|_{s} R (Y)$
10	9	adantl	$⊢ (X \in No \land Y \in No) \to Y = L (Y) \|_{s} R (Y)$
11	2 4 7 10	sltrecd	$⊢ (X \in No \land Y \in No) \to (X <_{s} Y \leftrightarrow (\exists y \in L (Y) X \leq_{s} y \lor \exists x \in R (X) x \leq_{s} Y))$
12	11	biimp3a	$⊢ (X \in No \land Y \in No \land X <_{s} Y) \to (\exists y \in L (Y) X \leq_{s} y \lor \exists x \in R (X) x \leq_{s} Y)$
13		rexn0	$⊢ \exists y \in L (Y) X \leq_{s} y \to L (Y) \neq \emptyset$
14		rexn0	$⊢ \exists x \in R (X) x \leq_{s} Y \to R (X) \neq \emptyset$
15	13 14	orim12i	$⊢ (\exists y \in L (Y) X \leq_{s} y \lor \exists x \in R (X) x \leq_{s} Y) \to (L (Y) \neq \emptyset \lor R (X) \neq \emptyset)$
16	12 15	syl	$⊢ (X \in No \land Y \in No \land X <_{s} Y) \to (L (Y) \neq \emptyset \lor R (X) \neq \emptyset)$

Metamath Proof Explorer