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

Proof

Step	Hyp	Ref	Expression
1		slerecd.1	|- ( ph -> A <
2		slerecd.2	|- ( ph -> C <
3		slerecd.3	|- ( ph -> X = ( A |s B ) )
4		slerecd.4	|- ( ph -> Y = ( C |s D ) )
5		slerec	|- ( ( ( 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