Theorem lesrecd

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	lesrecd.1	$$⊢\phi \to A{\ll }_{s}B$$
	lesrecd.2	$$⊢\phi \to C{\ll }_{s}D$$
	lesrecd.3	$$⊢\phi \to X=A{|}_{s}B$$
	lesrecd.4	$$⊢\phi \to Y=C{|}_{s}D$$
Assertion	lesrecd	$$⊢\phi \to \left(X{\le }_{s}Y\leftrightarrow \left(\forall d\in DX{<}_{s}d\wedge \forall a\in Aa{<}_{s}Y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lesrecd.1	$$⊢\phi \to A{\ll }_{s}B$$
2		lesrecd.2	$$⊢\phi \to C{\ll }_{s}D$$
3		lesrecd.3	$$⊢\phi \to X=A{|}_{s}B$$
4		lesrecd.4	$$⊢\phi \to Y=C{|}_{s}D$$
5		lesrec	$$⊢\left(\left(A{\ll }_{s}B\wedge C{\ll }_{s}D\right)\wedge \left(X=A{|}_{s}B\wedge Y=C{|}_{s}D\right)\right)\to \left(X{\le }_{s}Y\leftrightarrow \left(\forall d\in DX{<}_{s}d\wedge \forall a\in Aa{<}_{s}Y\right)\right)$$
6	1 2 3 4 5	syl22anc	$$⊢\phi \to \left(X{\le }_{s}Y\leftrightarrow \left(\forall d\in DX{<}_{s}d\wedge \forall a\in Aa{<}_{s}Y\right)\right)$$