Theorem n0sexg

Description: The set of all non-negative surreal integers exists. This theorem avoids the axiom of infinity by including it as an antecedent. (Contributed by Scott Fenton, 20-Feb-2025)

	Ref	Expression
Assertion	n0sexg	⊢ ( ω ∈ V → ℕ0s ∈ V )

Proof

Step	Hyp	Ref	Expression
1		df-n0s	⊢ ℕ0s = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 +s 1s ) ) , 0s ) “ ω )
2		rdgfun	⊢ Fun rec ( ( 𝑓 ∈ V ↦ ( 𝑓 +s 1s ) ) , 0s )
3		funimaexg	⊢ ( ( Fun rec ( ( 𝑓 ∈ V ↦ ( 𝑓 +s 1s ) ) , 0s ) ∧ ω ∈ V ) → ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 +s 1s ) ) , 0s ) “ ω ) ∈ V )
4	2 3	mpan	⊢ ( ω ∈ V → ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 +s 1s ) ) , 0s ) “ ω ) ∈ V )
5	1 4	eqeltrid	⊢ ( ω ∈ V → ℕ0s ∈ V )