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	|- ( ph -> A <
	lesrecd.2	|- ( ph -> C <
	lesrecd.3	|- ( ph -> X = ( A |s B ) )
	lesrecd.4	|- ( ph -> Y = ( C |s D ) )
Assertion	lesrecd	|- ( ph -> ( X <_s Y <-> ( A. d e. D X

Proof

Step	Hyp	Ref	Expression
1		lesrecd.1	|- ( ph -> A <
2		lesrecd.2	|- ( ph -> C <
3		lesrecd.3	|- ( ph -> X = ( A |s B ) )
4		lesrecd.4	|- ( ph -> Y = ( C |s D ) )
5		lesrec	|- ( ( ( A < ( X <_s Y <-> ( A. d e. D X
6	1 2 3 4 5	syl22anc	|- ( ph -> ( X <_s Y <-> ( A. d e. D X