Theorem elzs

Description: Membership in the set of surreal integers. (Contributed by Scott Fenton, 17-May-2025)

	Ref	Expression
Assertion	elzs	$$⊢A\in {\mathbb{Z}}_s\leftrightarrow \exists x\in {\mathbb{N}}_s\exists y\in {\mathbb{N}}_{s}A=x{-}_{s}y$$

Proof

Step	Hyp	Ref	Expression
1		df-zs	$$⊢{\mathbb{Z}}_s={-}_s\left[{\mathbb{N}}_s\times {\mathbb{N}}_s\right]$$
2	1	eleq2i	$$⊢A\in {\mathbb{Z}}_s\leftrightarrow A\in {-}_s\left[{\mathbb{N}}_s\times {\mathbb{N}}_s\right]$$
3		subsfn	$$⊢{-}_{s}Fn\left(\mathrm{No}\times \mathrm{No}\right)$$
4		nnssno	$$⊢{\mathbb{N}}_s\subseteq \mathrm{No}$$
5		xpss12	$$⊢\left({\mathbb{N}}_s\subseteq \mathrm{No}\wedge {\mathbb{N}}_s\subseteq \mathrm{No}\right)\to {\mathbb{N}}_s\times {\mathbb{N}}_s\subseteq \mathrm{No}\times \mathrm{No}$$
6	4 4 5	mp2an	$$⊢{\mathbb{N}}_s\times {\mathbb{N}}_s\subseteq \mathrm{No}\times \mathrm{No}$$
7		ovelimab	$$⊢\left({-}_{s}Fn\left(\mathrm{No}\times \mathrm{No}\right)\wedge {\mathbb{N}}_s\times {\mathbb{N}}_s\subseteq \mathrm{No}\times \mathrm{No}\right)\to \left(A\in {-}_s\left[{\mathbb{N}}_s\times {\mathbb{N}}_s\right]\leftrightarrow \exists x\in {\mathbb{N}}_s\exists y\in {\mathbb{N}}_{s}A=x{-}_{s}y\right)$$
8	3 6 7	mp2an	$$⊢A\in {-}_s\left[{\mathbb{N}}_s\times {\mathbb{N}}_s\right]\leftrightarrow \exists x\in {\mathbb{N}}_s\exists y\in {\mathbb{N}}_{s}A=x{-}_{s}y$$
9	2 8	bitri	$$⊢A\in {\mathbb{Z}}_s\leftrightarrow \exists x\in {\mathbb{N}}_s\exists y\in {\mathbb{N}}_{s}A=x{-}_{s}y$$