Theorem oldssno

Description: Old sets are surreals. (Contributed by Scott Fenton, 9-Oct-2024)

	Ref	Expression
Assertion	oldssno	$$⊢\mathrm{Old}\left(A\right)\subseteq \mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		oldf	$$⊢\mathrm{Old}:\mathrm{On}⟶𝒫\mathrm{No}$$
2		0elpw	$$⊢\varnothing \in 𝒫\mathrm{No}$$
3	1 2	f0cli	$$⊢\mathrm{Old}\left(A\right)\in 𝒫\mathrm{No}$$
4		elpwi	$$⊢\mathrm{Old}\left(A\right)\in 𝒫\mathrm{No}\to \mathrm{Old}\left(A\right)\subseteq \mathrm{No}$$
5	3 4	ax-mp	$$⊢\mathrm{Old}\left(A\right)\subseteq \mathrm{No}$$