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	$$⊢\phi \to A{\ll }_{s}B$$
	sltrecd.2	$$⊢\phi \to C{\ll }_{s}D$$
	sltrecd.3	$$⊢\phi \to X=A{|}_{s}B$$
	sltrecd.4	$$⊢\phi \to Y=C{|}_{s}D$$
Assertion	sltrecd	$$⊢\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		sltrecd.1	$$⊢\phi \to A{\ll }_{s}B$$
2		sltrecd.2	$$⊢\phi \to C{\ll }_{s}D$$
3		sltrecd.3	$$⊢\phi \to X=A{|}_{s}B$$
4		sltrecd.4	$$⊢\phi \to Y=C{|}_{s}D$$
5		sltrec	$$⊢\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)$$