Theorem zsex

Description: The surreal integers form a set. (Contributed by Scott Fenton, 17-May-2025)

	Ref	Expression
Assertion	zsex	⊢ ℤs ∈ V

Proof

Step	Hyp	Ref	Expression
1		df-zs	⊢ ℤs = ( −s “ ( ℕs × ℕs ) )
2		subsfn	⊢ −s Fn ( No × No )
3		fnfun	⊢ ( −s Fn ( No × No ) → Fun −s )
4		nnsex	⊢ ℕs ∈ V
5	4 4	xpex	⊢ ( ℕs × ℕs ) ∈ V
6	5	funimaex	⊢ ( Fun −s → ( −s “ ( ℕs × ℕs ) ) ∈ V )
7	2 3 6	mp2b	⊢ ( −s “ ( ℕs × ℕs ) ) ∈ V
8	1 7	eqeltri	⊢ ℤs ∈ V