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	Could not format assertion : No typesetting found for |- ( _Left ` A ) <

Proof

Step	Hyp	Ref	Expression
1		ssltleft	Could not format ( A e. No -> ( _Left ` A ) < ( _Left ` A ) <
2		ssltright	Could not format ( A e. No -> { A } < { A } <
3		snnzg	$$⊢A\in \mathrm{No}\to \left\{A\right\}\ne \varnothing$$
4		sslttr	Could not format ( ( ( _Left ` A ) < ( _Left ` A ) < ( _Left ` A ) <
5	1 2 3 4	syl3anc	Could not format ( A e. No -> ( _Left ` A ) < ( _Left ` A ) <
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	Could not format _Left : No --> ~P No : No typesetting found for |- _Left : No --> ~P No with typecode |-
10	9	fdmi	Could not format dom _Left = No : No typesetting found for |- dom _Left = No with typecode |-
11	10	eleq2i	Could not format ( A e. dom _Left <-> A e. No ) : No typesetting found for |- ( A e. dom _Left <-> A e. No ) with typecode |-
12		ndmfv	Could not format ( -. A e. dom _Left -> ( _Left ` A ) = (/) ) : No typesetting found for |- ( -. A e. dom _Left -> ( _Left ` A ) = (/) ) with typecode |-
13	11 12	sylnbir	Could not format ( -. A e. No -> ( _Left ` A ) = (/) ) : No typesetting found for |- ( -. A e. No -> ( _Left ` A ) = (/) ) with typecode |-
14		rightf	Could not format _Right : No --> ~P No : No typesetting found for |- _Right : No --> ~P No with typecode |-
15	14	fdmi	Could not format dom _Right = No : No typesetting found for |- dom _Right = No with typecode |-
16	15	eleq2i	Could not format ( A e. dom _Right <-> A e. No ) : No typesetting found for |- ( A e. dom _Right <-> A e. No ) with typecode |-
17		ndmfv	Could not format ( -. A e. dom _Right -> ( _Right ` A ) = (/) ) : No typesetting found for |- ( -. A e. dom _Right -> ( _Right ` A ) = (/) ) with typecode |-
18	16 17	sylnbir	Could not format ( -. A e. No -> ( _Right ` A ) = (/) ) : No typesetting found for |- ( -. A e. No -> ( _Right ` A ) = (/) ) with typecode |-
19	8 13 18	3brtr4d	Could not format ( -. A e. No -> ( _Left ` A ) < ( _Left ` A ) <
20	5 19	pm2.61i	Could not format ( _Left ` A ) <