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	$$⊢\phi \to A{\ll }_{s}B$$
	ltsrecd.2	$$⊢\phi \to C{\ll }_{s}D$$
	ltsrecd.3	$$⊢\phi \to X=A{|}_{s}B$$
	ltsrecd.4	$$⊢\phi \to Y=C{|}_{s}D$$
Assertion	ltsrecd	$$⊢\phi \to \left(X{<}_{s}Y\leftrightarrow \left(\exists c\in CX{\le }_{s}c\vee \exists b\in Bb{\le }_{s}Y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ltsrecd.1	$$⊢\phi \to A{\ll }_{s}B$$
2		ltsrecd.2	$$⊢\phi \to C{\ll }_{s}D$$
3		ltsrecd.3	$$⊢\phi \to X=A{|}_{s}B$$
4		ltsrecd.4	$$⊢\phi \to Y=C{|}_{s}D$$
5		ltsrec	$$⊢\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{<}_{s}Y\leftrightarrow \left(\exists c\in CX{\le }_{s}c\vee \exists b\in Bb{\le }_{s}Y\right)\right)$$
6	1 2 3 4 5	syl22anc	$$⊢\phi \to \left(X{<}_{s}Y\leftrightarrow \left(\exists c\in CX{\le }_{s}c\vee \exists b\in Bb{\le }_{s}Y\right)\right)$$