Theorem slerecd

Description: A comparison law for surreals considered as cuts of sets of surreals. Definition from Conway p. 4. Theorem 4 of Alling p. 186. Theorem 2.5 of Gonshor p. 9. (Contributed by Scott Fenton, 5-Dec-2025)

	Ref	Expression
Hypotheses	slerecd.1	⊢ ( 𝜑 → 𝐴 <<s 𝐵 )
	slerecd.2	⊢ ( 𝜑 → 𝐶 <<s 𝐷 )
	slerecd.3	⊢ ( 𝜑 → 𝑋 = ( 𝐴 |s 𝐵 ) )
	slerecd.4	⊢ ( 𝜑 → 𝑌 = ( 𝐶 |s 𝐷 ) )
Assertion	slerecd	⊢ ( 𝜑 → ( 𝑋 ≤s 𝑌 ↔ ( ∀ 𝑑 ∈ 𝐷 𝑋 <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		slerecd.1	⊢ ( 𝜑 → 𝐴 <<s 𝐵 )
2		slerecd.2	⊢ ( 𝜑 → 𝐶 <<s 𝐷 )
3		slerecd.3	⊢ ( 𝜑 → 𝑋 = ( 𝐴 |s 𝐵 ) )
4		slerecd.4	⊢ ( 𝜑 → 𝑌 = ( 𝐶 |s 𝐷 ) )
5		slerec	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( 𝑋 ≤s 𝑌 ↔ ( ∀ 𝑑 ∈ 𝐷 𝑋 <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑌 ) ) )
6	1 2 3 4 5	syl22anc	⊢ ( 𝜑 → ( 𝑋 ≤s 𝑌 ↔ ( ∀ 𝑑 ∈ 𝐷 𝑋 <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑌 ) ) )