Theorem sltsd

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

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

Proof

Step	Hyp	Ref	Expression
1		sltsd.1	$$⊢\phi \to A\in V$$
2		sltsd.2	$$⊢\phi \to B\in W$$
3		sltsd.3	$$⊢\phi \to A\subseteq \mathrm{No}$$
4		sltsd.4	$$⊢\phi \to B\subseteq \mathrm{No}$$
5		sltsd.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		brslts	$$⊢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$$