Theorem peano5n0s

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

	Ref	Expression
Assertion	peano5n0s	⊢ ( ( 0s ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +s 1s ) ∈ 𝐴 ) → ℕ0s ⊆ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-n0s	⊢ ℕ0s = ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 +s 1s ) ) , 0s ) “ ω )
2	1	a1i	⊢ ( ( 0s ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +s 1s ) ∈ 𝐴 ) → ℕ0s = ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 +s 1s ) ) , 0s ) “ ω ) )
3		0sno	⊢ 0s ∈ No
4	3	a1i	⊢ ( ( 0s ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +s 1s ) ∈ 𝐴 ) → 0s ∈ No )
5		simpl	⊢ ( ( 0s ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +s 1s ) ∈ 𝐴 ) → 0s ∈ 𝐴 )
6		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 +s 1s ) = ( 𝑦 +s 1s ) )
7	6	eleq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 +s 1s ) ∈ 𝐴 ↔ ( 𝑦 +s 1s ) ∈ 𝐴 ) )
8	7	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 +s 1s ) ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 +s 1s ) ∈ 𝐴 )
9	8	adantll	⊢ ( ( ( 0s ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +s 1s ) ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 +s 1s ) ∈ 𝐴 )
10	2 4 5 9	noseqind	⊢ ( ( 0s ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 +s 1s ) ∈ 𝐴 ) → ℕ0s ⊆ 𝐴 )