Theorem n0on

Description: A surreal natural is a surreal ordinal. (Contributed by Scott Fenton, 2-Apr-2025)

	Ref	Expression
Assertion	n0on	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A\in {On}_s$$

Proof

Step	Hyp	Ref	Expression
1		n0no	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A\in \mathrm{No}$$
2		1no	$$⊢1_s\in \mathrm{No}$$
3		subscl	$$⊢\left(A\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to A{-}_s{1}_s\in \mathrm{No}$$
4	1 2 3	sylancl	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A{-}_s{1}_s\in \mathrm{No}$$
5		ovex	$$⊢A{-}_s{1}_s\in \mathrm{V}$$
6	5	snelpw	$$⊢A{-}_s{1}_s\in \mathrm{No}\leftrightarrow \left\{A{-}_s{1}_s\right\}\in 𝒫\mathrm{No}$$
7	4 6	sylib	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \left\{A{-}_s{1}_s\right\}\in 𝒫\mathrm{No}$$
8		n0cut	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A=\left\{A{-}_s{1}_s\right\}{|}_s\varnothing$$
9		oveq1	$$⊢x=\left\{A{-}_s{1}_s\right\}\to x{|}_s\varnothing =\left\{A{-}_s{1}_s\right\}{|}_s\varnothing$$
10	9	eqeq2d	$$⊢x=\left\{A{-}_s{1}_s\right\}\to \left(A=x{|}_s\varnothing \leftrightarrow A=\left\{A{-}_s{1}_s\right\}{|}_s\varnothing \right)$$
11	10	rspcev	$$⊢\left(\left\{A{-}_s{1}_s\right\}\in 𝒫\mathrm{No}\wedge A=\left\{A{-}_s{1}_s\right\}{|}_s\varnothing \right)\to \exists x\in 𝒫\mathrm{No}A=x{|}_s\varnothing$$
12	7 8 11	syl2anc	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to \exists x\in 𝒫\mathrm{No}A=x{|}_s\varnothing$$
13		elons2	$$⊢A\in {On}_s\leftrightarrow \exists x\in 𝒫\mathrm{No}A=x{|}_s\varnothing$$
14	12 13	sylibr	$$⊢A\in {\mathbb{N}}_{\mathrm{0s}}\to A\in {On}_s$$