Theorem ltsn0

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	ltsn0	⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ 𝑋 <s 𝑌 ) → ( ( L ‘ 𝑌 ) ≠ ∅ ∨ ( R ‘ 𝑋 ) ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		lltr	⊢ ( L ‘ 𝑋 ) <<s ( R ‘ 𝑋 )
2	1	a1i	⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ) → ( L ‘ 𝑋 ) <<s ( R ‘ 𝑋 ) )
3		lltr	⊢ ( L ‘ 𝑌 ) <<s ( R ‘ 𝑌 )
4	3	a1i	⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ) → ( L ‘ 𝑌 ) <<s ( R ‘ 𝑌 ) )
5		lrcut	⊢ ( 𝑋 ∈ No → ( ( L ‘ 𝑋 ) |s ( R ‘ 𝑋 ) ) = 𝑋 )
6	5	eqcomd	⊢ ( 𝑋 ∈ No → 𝑋 = ( ( L ‘ 𝑋 ) |s ( R ‘ 𝑋 ) ) )
7	6	adantr	⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ) → 𝑋 = ( ( L ‘ 𝑋 ) |s ( R ‘ 𝑋 ) ) )
8		lrcut	⊢ ( 𝑌 ∈ No → ( ( L ‘ 𝑌 ) |s ( R ‘ 𝑌 ) ) = 𝑌 )
9	8	eqcomd	⊢ ( 𝑌 ∈ No → 𝑌 = ( ( L ‘ 𝑌 ) |s ( R ‘ 𝑌 ) ) )
10	9	adantl	⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ) → 𝑌 = ( ( L ‘ 𝑌 ) |s ( R ‘ 𝑌 ) ) )
11	2 4 7 10	ltsrecd	⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ) → ( 𝑋 <s 𝑌 ↔ ( ∃ 𝑦 ∈ ( L ‘ 𝑌 ) 𝑋 ≤s 𝑦 ∨ ∃ 𝑥 ∈ ( R ‘ 𝑋 ) 𝑥 ≤s 𝑌 ) ) )
12	11	biimp3a	⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ 𝑋 <s 𝑌 ) → ( ∃ 𝑦 ∈ ( L ‘ 𝑌 ) 𝑋 ≤s 𝑦 ∨ ∃ 𝑥 ∈ ( R ‘ 𝑋 ) 𝑥 ≤s 𝑌 ) )
13		rexn0	⊢ ( ∃ 𝑦 ∈ ( L ‘ 𝑌 ) 𝑋 ≤s 𝑦 → ( L ‘ 𝑌 ) ≠ ∅ )
14		rexn0	⊢ ( ∃ 𝑥 ∈ ( R ‘ 𝑋 ) 𝑥 ≤s 𝑌 → ( R ‘ 𝑋 ) ≠ ∅ )
15	13 14	orim12i	⊢ ( ( ∃ 𝑦 ∈ ( L ‘ 𝑌 ) 𝑋 ≤s 𝑦 ∨ ∃ 𝑥 ∈ ( R ‘ 𝑋 ) 𝑥 ≤s 𝑌 ) → ( ( L ‘ 𝑌 ) ≠ ∅ ∨ ( R ‘ 𝑋 ) ≠ ∅ ) )
16	12 15	syl	⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ 𝑋 <s 𝑌 ) → ( ( L ‘ 𝑌 ) ≠ ∅ ∨ ( R ‘ 𝑋 ) ≠ ∅ ) )