Theorem oldssno

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

	Ref	Expression
Assertion	oldssno	⊢ ( O ‘ 𝐴 ) ⊆ No

Proof

Step	Hyp	Ref	Expression
1		oldf	⊢ O : On ⟶ 𝒫 No
2		0elpw	⊢ ∅ ∈ 𝒫 No
3	1 2	f0cli	⊢ ( O ‘ 𝐴 ) ∈ 𝒫 No
4		elpwi	⊢ ( ( O ‘ 𝐴 ) ∈ 𝒫 No → ( O ‘ 𝐴 ) ⊆ No )
5	3 4	ax-mp	⊢ ( O ‘ 𝐴 ) ⊆ No