Theorem ltsrecd

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

	Ref	Expression
Hypotheses	ltsrecd.1	|- ( ph -> A <
	ltsrecd.2	|- ( ph -> C <
	ltsrecd.3	|- ( ph -> X = ( A |s B ) )
	ltsrecd.4	|- ( ph -> Y = ( C |s D ) )
Assertion	ltsrecd	|- ( ph -> ( X ( E. c e. C X <_s c \/ E. b e. B b <_s Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		ltsrecd.1	|- ( ph -> A <
2		ltsrecd.2	|- ( ph -> C <
3		ltsrecd.3	|- ( ph -> X = ( A |s B ) )
4		ltsrecd.4	|- ( ph -> Y = ( C |s D ) )
5		ltsrec	|- ( ( ( A < ( X ( E. c e. C X <_s c \/ E. b e. B b <_s Y ) ) )
6	1 2 3 4 5	syl22anc	|- ( ph -> ( X ( E. c e. C X <_s c \/ E. b e. B b <_s Y ) ) )