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