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) (Revised by Scott Fenton, 21-Feb-2025)

	Ref	Expression
Assertion	lltropt	$$⊢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)$$
6		0elpw	$$⊢\varnothing \in 𝒫\mathrm{No}$$
7		nulssgt	$$⊢\varnothing \in 𝒫\mathrm{No}\to \varnothing {\ll }_s\varnothing$$
8	6 7	mp1i	$$⊢\neg A\in \mathrm{No}\to \varnothing {\ll }_s\varnothing$$
9		leftf	$$⊢L:\mathrm{No}⟶𝒫\mathrm{No}$$
10	9	fdmi	$$⊢\mathrm{dom}L=\mathrm{No}$$
11	10	eleq2i	$$⊢A\in \mathrm{dom}L\leftrightarrow A\in \mathrm{No}$$
12		ndmfv	$$⊢\neg A\in \mathrm{dom}L\to L\left(A\right)=\varnothing$$
13	11 12	sylnbir	$$⊢\neg A\in \mathrm{No}\to L\left(A\right)=\varnothing$$
14		rightf	$$⊢R:\mathrm{No}⟶𝒫\mathrm{No}$$
15	14	fdmi	$$⊢\mathrm{dom}R=\mathrm{No}$$
16	15	eleq2i	$$⊢A\in \mathrm{dom}R\leftrightarrow A\in \mathrm{No}$$
17		ndmfv	$$⊢\neg A\in \mathrm{dom}R\to R\left(A\right)=\varnothing$$
18	16 17	sylnbir	$$⊢\neg A\in \mathrm{No}\to R\left(A\right)=\varnothing$$
19	8 13 18	3brtr4d	$$⊢\neg A\in \mathrm{No}\to L\left(A\right){\ll }_{s}R\left(A\right)$$
20	5 19	pm2.61i	$$⊢L\left(A\right){\ll }_{s}R\left(A\right)$$