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		sltrec	$⊢ ((L (X) ≪_{s} R (X) \land L (Y) ≪_{s} R (Y)) \land (X = L (X) \|_{s} R (X) \land Y = L (Y) \|_{s} R (Y))) \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	2 4 7 10 11	syl22anc	$⊢ (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))$
13	12	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)$
14		rexn0	$⊢ \exists y \in L (Y) X \leq_{s} y \to L (Y) \neq \emptyset$
15		rexn0	$⊢ \exists x \in R (X) x \leq_{s} Y \to R (X) \neq \emptyset$
16	14 15	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)$
17	13 16	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