Theorem 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 e. No /\ Y e. No /\ X ( ( _Left ` Y ) =/= (/) \/ ( _Right ` X ) =/= (/) ) )

Proof

Step	Hyp	Ref	Expression
1		lltropt	|- ( _Left ` X ) <
2	1	a1i	|- ( ( X e. No /\ Y e. No ) -> ( _Left ` X ) <
3		lltropt	|- ( _Left ` Y ) <
4	3	a1i	|- ( ( X e. No /\ Y e. No ) -> ( _Left ` Y ) <
5		lrcut	|- ( X e. No -> ( ( _Left ` X ) |s ( _Right ` X ) ) = X )
6	5	eqcomd	|- ( X e. No -> X = ( ( _Left ` X ) |s ( _Right ` X ) ) )
7	6	adantr	|- ( ( X e. No /\ Y e. No ) -> X = ( ( _Left ` X ) |s ( _Right ` X ) ) )
8		lrcut	|- ( Y e. No -> ( ( _Left ` Y ) |s ( _Right ` Y ) ) = Y )
9	8	eqcomd	|- ( Y e. No -> Y = ( ( _Left ` Y ) |s ( _Right ` Y ) ) )
10	9	adantl	|- ( ( X e. No /\ Y e. No ) -> Y = ( ( _Left ` Y ) |s ( _Right ` Y ) ) )
11		sltrec	|- ( ( ( ( _Left ` X ) < ( X ( E. y e. ( _Left ` Y ) X <_s y \/ E. x e. ( _Right ` X ) x <_s Y ) ) )
12	2 4 7 10 11	syl22anc	|- ( ( X e. No /\ Y e. No ) -> ( X ( E. y e. ( _Left ` Y ) X <_s y \/ E. x e. ( _Right ` X ) x <_s Y ) ) )
13	12	biimp3a	|- ( ( X e. No /\ Y e. No /\ X ( E. y e. ( _Left ` Y ) X <_s y \/ E. x e. ( _Right ` X ) x <_s Y ) )
14		rexn0	|- ( E. y e. ( _Left ` Y ) X <_s y -> ( _Left ` Y ) =/= (/) )
15		rexn0	|- ( E. x e. ( _Right ` X ) x <_s Y -> ( _Right ` X ) =/= (/) )
16	14 15	orim12i	|- ( ( E. y e. ( _Left ` Y ) X <_s y \/ E. x e. ( _Right ` X ) x <_s Y ) -> ( ( _Left ` Y ) =/= (/) \/ ( _Right ` X ) =/= (/) ) )
17	13 16	syl	|- ( ( X e. No /\ Y e. No /\ X ( ( _Left ` Y ) =/= (/) \/ ( _Right ` X ) =/= (/) ) )