Theorem ssltd

Description: Deduce surreal set less-than. (Contributed by Scott Fenton, 24-Sep-2024)

	Ref	Expression
Hypotheses	ssltd.1	$$⊢\phi \to A\in V$$
	ssltd.2	$$⊢\phi \to B\in W$$
	ssltd.3	$$⊢\phi \to A\subseteq \mathrm{No}$$
	ssltd.4	$$⊢\phi \to B\subseteq \mathrm{No}$$
	ssltd.5	$$⊢\left(\phi \wedge x\in A\wedge y\in B\right)\to x{<}_{s}y$$
Assertion	ssltd	$$⊢\phi \to A{\ll }_{s}B$$

Proof

Step	Hyp	Ref	Expression
1		ssltd.1	$$⊢\phi \to A\in V$$
2		ssltd.2	$$⊢\phi \to B\in W$$
3		ssltd.3	$$⊢\phi \to A\subseteq \mathrm{No}$$
4		ssltd.4	$$⊢\phi \to B\subseteq \mathrm{No}$$
5		ssltd.5	$$⊢\left(\phi \wedge x\in A\wedge y\in B\right)\to x{<}_{s}y$$
6	1	elexd	$$⊢\phi \to A\in \mathrm{V}$$
7	2	elexd	$$⊢\phi \to B\in \mathrm{V}$$
8	5	3expb	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in B\right)\right)\to x{<}_{s}y$$
9	8	ralrimivva	$$⊢\phi \to \forall x\in A\forall y\in Bx{<}_{s}y$$
10	3 4 9	3jca	$$⊢\phi \to \left(A\subseteq \mathrm{No}\wedge B\subseteq \mathrm{No}\wedge \forall x\in A\forall y\in Bx{<}_{s}y\right)$$
11		brsslt	$$⊢A{\ll }_{s}B\leftrightarrow \left(\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\wedge \left(A\subseteq \mathrm{No}\wedge B\subseteq \mathrm{No}\wedge \forall x\in A\forall y\in Bx{<}_{s}y\right)\right)$$
12	6 7 10 11	syl21anbrc	$$⊢\phi \to A{\ll }_{s}B$$