Theorem peano5n0s

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

	Ref	Expression
Assertion	peano5n0s	|- ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> NN0_s C_ A )

Proof

Step	Hyp	Ref	Expression
1		df-n0s	|- NN0_s = ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) " _om )
2	1	a1i	|- ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> NN0_s = ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) " _om ) )
3		0sno	|- 0s e. No
4	3	a1i	|- ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> 0s e. No )
5		simpl	|- ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> 0s e. A )
6		oveq1	|- ( x = y -> ( x +s 1s ) = ( y +s 1s ) )
7	6	eleq1d	|- ( x = y -> ( ( x +s 1s ) e. A <-> ( y +s 1s ) e. A ) )
8	7	rspccva	|- ( ( A. x e. A ( x +s 1s ) e. A /\ y e. A ) -> ( y +s 1s ) e. A )
9	8	adantll	|- ( ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) /\ y e. A ) -> ( y +s 1s ) e. A )
10	2 4 5 9	noseqind	|- ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> NN0_s C_ A )