Theorem sltrecd

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

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

Proof

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