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 e. No -> ( _L ` A ) <

Proof

Step	Hyp	Ref	Expression
1		ssltleft	|- ( A e. No -> ( _L ` A ) <
2		ssltright	|- ( A e. No -> { A } <
3		snnzg	|- ( A e. No -> { A } =/= (/) )
4		sslttr	|- ( ( ( _L ` A ) < ( _L ` A ) <
5	1 2 3 4	syl3anc	|- ( A e. No -> ( _L ` A ) <