Theorem lltropt

Description: The left options of a surreal are strictly less than the right options of the same surreal. (Contributed by Scott Fenton, 6-Aug-2024)

	Ref	Expression
Assertion	lltropt	$$⊢A\in \mathrm{No}\to L\left(A\right){\ll }_{s}R\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssltleft	$$⊢A\in \mathrm{No}\to L\left(A\right){\ll }_s\left\{A\right\}$$
2		ssltright	$$⊢A\in \mathrm{No}\to \left\{A\right\}{\ll }_{s}R\left(A\right)$$
3		snnzg	$$⊢A\in \mathrm{No}\to \left\{A\right\}\ne \varnothing$$
4		sslttr	$$⊢\left(L\left(A\right){\ll }_s\left\{A\right\}\wedge \left\{A\right\}{\ll }_{s}R\left(A\right)\wedge \left\{A\right\}\ne \varnothing \right)\to L\left(A\right){\ll }_{s}R\left(A\right)$$
5	1 2 3 4	syl3anc	$$⊢A\in \mathrm{No}\to L\left(A\right){\ll }_{s}R\left(A\right)$$