Theorem sltrecd

Description: A comparison law for surreals considered as cuts of sets of surreals. (Contributed by Scott Fenton, 5-Dec-2025)

	Ref	Expression
Hypotheses	sltrecd.1	⊢ ( 𝜑 → 𝐴 <<s 𝐵 )
	sltrecd.2	⊢ ( 𝜑 → 𝐶 <<s 𝐷 )
	sltrecd.3	⊢ ( 𝜑 → 𝑋 = ( 𝐴 |s 𝐵 ) )
	sltrecd.4	⊢ ( 𝜑 → 𝑌 = ( 𝐶 |s 𝐷 ) )
Assertion	sltrecd	⊢ ( 𝜑 → ( 𝑋 <s 𝑌 ↔ ( ∃ 𝑐 ∈ 𝐶 𝑋 ≤s 𝑐 ∨ ∃ 𝑏 ∈ 𝐵 𝑏 ≤s 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sltrecd.1	⊢ ( 𝜑 → 𝐴 <<s 𝐵 )
2		sltrecd.2	⊢ ( 𝜑 → 𝐶 <<s 𝐷 )
3		sltrecd.3	⊢ ( 𝜑 → 𝑋 = ( 𝐴 |s 𝐵 ) )
4		sltrecd.4	⊢ ( 𝜑 → 𝑌 = ( 𝐶 |s 𝐷 ) )
5		sltrec	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( 𝑋 <s 𝑌 ↔ ( ∃ 𝑐 ∈ 𝐶 𝑋 ≤s 𝑐 ∨ ∃ 𝑏 ∈ 𝐵 𝑏 ≤s 𝑌 ) ) )
6	1 2 3 4 5	syl22anc	⊢ ( 𝜑 → ( 𝑋 <s 𝑌 ↔ ( ∃ 𝑐 ∈ 𝐶 𝑋 ≤s 𝑐 ∨ ∃ 𝑏 ∈ 𝐵 𝑏 ≤s 𝑌 ) ) )