Theorem zsex

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

	Ref	Expression
Assertion	zsex	$$⊢{\mathbb{Z}}_s\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-zs	$$⊢{\mathbb{Z}}_s={-}_s\left[{\mathbb{N}}_s\times {\mathbb{N}}_s\right]$$
2		subsfn	$$⊢{-}_{s}Fn\left(\mathrm{No}\times \mathrm{No}\right)$$
3		fnfun	$$⊢{-}_{s}Fn\left(\mathrm{No}\times \mathrm{No}\right)\to \mathrm{Fun}{-}_s$$
4		nnsex	$$⊢{\mathbb{N}}_s\in \mathrm{V}$$
5	4 4	xpex	$$⊢{\mathbb{N}}_s\times {\mathbb{N}}_s\in \mathrm{V}$$
6	5	funimaex	$$⊢\mathrm{Fun}{-}_s\to {-}_s\left[{\mathbb{N}}_s\times {\mathbb{N}}_s\right]\in \mathrm{V}$$
7	2 3 6	mp2b	$$⊢{-}_s\left[{\mathbb{N}}_s\times {\mathbb{N}}_s\right]\in \mathrm{V}$$
8	1 7	eqeltri	$$⊢{\mathbb{Z}}_s\in \mathrm{V}$$