Theorem peano5n0s

Description: Peano's inductive postulate for non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025)

	Ref	Expression
Assertion	peano5n0s	$$⊢\left(0_s\in A\wedge \forall x\in Ax{+}_s{1}_s\in A\right)\to {\mathbb{N}}_{\mathrm{0s}}\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		df-n0s	$$⊢{\mathbb{N}}_{\mathrm{0s}}=\mathrm{rec}\left(\left(n\in \mathrm{V}⟼n{+}_s{1}_s\right),0_s\right)\left[\mathrm{\omega }\right]$$
2	1	a1i	$$⊢\left(0_s\in A\wedge \forall x\in Ax{+}_s{1}_s\in A\right)\to {\mathbb{N}}_{\mathrm{0s}}=\mathrm{rec}\left(\left(n\in \mathrm{V}⟼n{+}_s{1}_s\right),0_s\right)\left[\mathrm{\omega }\right]$$
3		0sno	$$⊢0_s\in \mathrm{No}$$
4	3	a1i	$$⊢\left(0_s\in A\wedge \forall x\in Ax{+}_s{1}_s\in A\right)\to 0_s\in \mathrm{No}$$
5		simpl	$$⊢\left(0_s\in A\wedge \forall x\in Ax{+}_s{1}_s\in A\right)\to 0_s\in A$$
6		oveq1	$$⊢x=y\to x{+}_s{1}_s=y{+}_s{1}_s$$
7	6	eleq1d	$$⊢x=y\to \left(x{+}_s{1}_s\in A\leftrightarrow y{+}_s{1}_s\in A\right)$$
8	7	rspccva	$$⊢\left(\forall x\in Ax{+}_s{1}_s\in A\wedge y\in A\right)\to y{+}_s{1}_s\in A$$
9	8	adantll	$$⊢\left(\left(0_s\in A\wedge \forall x\in Ax{+}_s{1}_s\in A\right)\wedge y\in A\right)\to y{+}_s{1}_s\in A$$
10	2 4 5 9	noseqind	$$⊢\left(0_s\in A\wedge \forall x\in Ax{+}_s{1}_s\in A\right)\to {\mathbb{N}}_{\mathrm{0s}}\subseteq A$$