Theorem leftssno

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

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

Proof

Step	Hyp	Ref	Expression
1		leftssold	⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) ⊆ ( O ‘ ( bday ‘ 𝐴 ) ) )
2		bdayelon	⊢ ( bday ‘ 𝐴 ) ∈ On
3		oldf	⊢ O : On ⟶ 𝒫 No
4	3	ffvelrni	⊢ ( ( bday ‘ 𝐴 ) ∈ On → ( O ‘ ( bday ‘ 𝐴 ) ) ∈ 𝒫 No )
5	4	elpwid	⊢ ( ( bday ‘ 𝐴 ) ∈ On → ( O ‘ ( bday ‘ 𝐴 ) ) ⊆ No )
6	2 5	ax-mp	⊢ ( O ‘ ( bday ‘ 𝐴 ) ) ⊆ No
7	1 6	sstrdi	⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) ⊆ No )