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	Could not format assertion : No typesetting found for |- ( ( X e. No /\ Y e. No /\ X ( ( _Left ` Y ) =/= (/) \/ ( _Right ` X ) =/= (/) ) ) with typecode |-

Proof

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