Theorem ssltsn

Description: Surreal set less-than of two singletons. (Contributed by Scott Fenton, 17-Mar-2025)

	Ref	Expression
Hypotheses	ssltsn.1	$$⊢\phi \to A\in \mathrm{No}$$
	ssltsn.2	$$⊢\phi \to B\in \mathrm{No}$$
	ssltsn.3	$$⊢\phi \to A{<}_{s}B$$
Assertion	ssltsn	$$⊢\phi \to \left\{A\right\}{\ll }_s\left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ssltsn.1	$$⊢\phi \to A\in \mathrm{No}$$
2		ssltsn.2	$$⊢\phi \to B\in \mathrm{No}$$
3		ssltsn.3	$$⊢\phi \to A{<}_{s}B$$
4		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
5	4	a1i	$$⊢\phi \to \left\{A\right\}\in \mathrm{V}$$
6		snex	$$⊢\left\{B\right\}\in \mathrm{V}$$
7	6	a1i	$$⊢\phi \to \left\{B\right\}\in \mathrm{V}$$
8	1	snssd	$$⊢\phi \to \left\{A\right\}\subseteq \mathrm{No}$$
9	2	snssd	$$⊢\phi \to \left\{B\right\}\subseteq \mathrm{No}$$
10		velsn	$$⊢x\in \left\{A\right\}\leftrightarrow x=A$$
11		velsn	$$⊢y\in \left\{B\right\}\leftrightarrow y=B$$
12		breq12	$$⊢\left(x=A\wedge y=B\right)\to \left(x{<}_{s}y\leftrightarrow A{<}_{s}B\right)$$
13	10 11 12	syl2anb	$$⊢\left(x\in \left\{A\right\}\wedge y\in \left\{B\right\}\right)\to \left(x{<}_{s}y\leftrightarrow A{<}_{s}B\right)$$
14	3 13	syl5ibrcom	$$⊢\phi \to \left(\left(x\in \left\{A\right\}\wedge y\in \left\{B\right\}\right)\to x{<}_{s}y\right)$$
15	14	3impib	$$⊢\left(\phi \wedge x\in \left\{A\right\}\wedge y\in \left\{B\right\}\right)\to x{<}_{s}y$$
16	5 7 8 9 15	ssltd	$$⊢\phi \to \left\{A\right\}{\ll }_s\left\{B\right\}$$