Theorem sltn0

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

	Ref	Expression
Assertion	sltn0	⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ 𝑋 <s 𝑌 ) → ( ( L ‘ 𝑌 ) ≠ ∅ ∨ ( R ‘ 𝑋 ) ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		lltropt	⊢ ( 𝑋 ∈ No → ( L ‘ 𝑋 ) <<s ( R ‘ 𝑋 ) )
2	1	adantr	⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ) → ( L ‘ 𝑋 ) <<s ( R ‘ 𝑋 ) )
3		lltropt	⊢ ( 𝑌 ∈ No → ( L ‘ 𝑌 ) <<s ( R ‘ 𝑌 ) )
4	3	adantl	⊢ ( ( 𝑋 ∈ 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		sltrec	⊢ ( ( ( ( L ‘ 𝑋 ) <<s ( R ‘ 𝑋 ) ∧ ( L ‘ 𝑌 ) <<s ( R ‘ 𝑌 ) ) ∧ ( 𝑋 = ( ( L ‘ 𝑋 ) |s ( R ‘ 𝑋 ) ) ∧ 𝑌 = ( ( L ‘ 𝑌 ) |s ( R ‘ 𝑌 ) ) ) ) → ( 𝑋 <s 𝑌 ↔ ( ∃ 𝑦 ∈ ( L ‘ 𝑌 ) 𝑋 ≤s 𝑦 ∨ ∃ 𝑥 ∈ ( R ‘ 𝑋 ) 𝑥 ≤s 𝑌 ) ) )
12	2 4 7 10 11	syl22anc	⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ) → ( 𝑋 <s 𝑌 ↔ ( ∃ 𝑦 ∈ ( L ‘ 𝑌 ) 𝑋 ≤s 𝑦 ∨ ∃ 𝑥 ∈ ( R ‘ 𝑋 ) 𝑥 ≤s 𝑌 ) ) )
13	12	biimp3a	⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ 𝑋 <s 𝑌 ) → ( ∃ 𝑦 ∈ ( L ‘ 𝑌 ) 𝑋 ≤s 𝑦 ∨ ∃ 𝑥 ∈ ( R ‘ 𝑋 ) 𝑥 ≤s 𝑌 ) )
14		rexn0	⊢ ( ∃ 𝑦 ∈ ( L ‘ 𝑌 ) 𝑋 ≤s 𝑦 → ( L ‘ 𝑌 ) ≠ ∅ )
15		rexn0	⊢ ( ∃ 𝑥 ∈ ( R ‘ 𝑋 ) 𝑥 ≤s 𝑌 → ( R ‘ 𝑋 ) ≠ ∅ )
16	14 15	orim12i	⊢ ( ( ∃ 𝑦 ∈ ( L ‘ 𝑌 ) 𝑋 ≤s 𝑦 ∨ ∃ 𝑥 ∈ ( R ‘ 𝑋 ) 𝑥 ≤s 𝑌 ) → ( ( L ‘ 𝑌 ) ≠ ∅ ∨ ( R ‘ 𝑋 ) ≠ ∅ ) )
17	13 16	syl	⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ 𝑋 <s 𝑌 ) → ( ( L ‘ 𝑌 ) ≠ ∅ ∨ ( R ‘ 𝑋 ) ≠ ∅ ) )