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	$⊢ ω \in V \to ℕ_{0s} \in V$

Proof

Step	Hyp	Ref	Expression
1		df-n0s	$⊢ ℕ_{0s} = rec ((f \in V ⟼ f +_{s} 1_{s}), 0_{s}) [ω]$
2		rdgfun	$⊢ Fun rec ((f \in V ⟼ f +_{s} 1_{s}), 0_{s})$
3		funimaexg	$⊢ (Fun rec ((f \in V ⟼ f +_{s} 1_{s}), 0_{s}) \land ω \in V) \to rec ((f \in V ⟼ f +_{s} 1_{s}), 0_{s}) [ω] \in V$
4	2 3	mpan	$⊢ ω \in V \to rec ((f \in V ⟼ f +_{s} 1_{s}), 0_{s}) [ω] \in V$
5	1 4	eqeltrid	$⊢ ω \in V \to ℕ_{0s} \in V$

Metamath Proof Explorer

Theorem n0sexg

Proof