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	⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) <<s ( R ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ssltleft	⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) <<s { 𝐴 } )
2		ssltright	⊢ ( 𝐴 ∈ No → { 𝐴 } <<s ( R ‘ 𝐴 ) )
3		snnzg	⊢ ( 𝐴 ∈ No → { 𝐴 } ≠ ∅ )
4		sslttr	⊢ ( ( ( L ‘ 𝐴 ) <<s { 𝐴 } ∧ { 𝐴 } <<s ( R ‘ 𝐴 ) ∧ { 𝐴 } ≠ ∅ ) → ( L ‘ 𝐴 ) <<s ( R ‘ 𝐴 ) )
5	1 2 3 4	syl3anc	⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) <<s ( R ‘ 𝐴 ) )