Theorem leftssno

Description: The left set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024)

	Ref	Expression
Assertion	leftssno	⊢ ( L ‘ 𝐴 ) ⊆ No

Proof

Step	Hyp	Ref	Expression
1		leftssold	⊢ ( L ‘ 𝐴 ) ⊆ ( O ‘ ( bday ‘ 𝐴 ) )
2		oldssno	⊢ ( O ‘ ( bday ‘ 𝐴 ) ) ⊆ No
3	1 2	sstri	⊢ ( L ‘ 𝐴 ) ⊆ No