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	$$⊢A\in \mathrm{No}\to L\left(A\right)\subseteq \mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		leftssold	$$⊢A\in \mathrm{No}\to L\left(A\right)\subseteq \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)$$
2		bdayelon	$$⊢\mathrm{bday}\left(A\right)\in \mathrm{On}$$
3		oldf	$$⊢\mathrm{Old}:\mathrm{On}⟶𝒫\mathrm{No}$$
4	3	ffvelrni	$$⊢\mathrm{bday}\left(A\right)\in \mathrm{On}\to \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\in 𝒫\mathrm{No}$$
5	4	elpwid	$$⊢\mathrm{bday}\left(A\right)\in \mathrm{On}\to \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\subseteq \mathrm{No}$$
6	2 5	ax-mp	$$⊢\mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\subseteq \mathrm{No}$$
7	1 6	sstrdi	$$⊢A\in \mathrm{No}\to L\left(A\right)\subseteq \mathrm{No}$$