Theorem elzs

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

	Ref	Expression
Assertion	elzs	⊢ ( 𝐴 ∈ ℤs ↔ ∃ 𝑥 ∈ ℕs ∃ 𝑦 ∈ ℕs 𝐴 = ( 𝑥 -s 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		df-zs	⊢ ℤs = ( -s “ ( ℕs × ℕs ) )
2	1	eleq2i	⊢ ( 𝐴 ∈ ℤs ↔ 𝐴 ∈ ( -s “ ( ℕs × ℕs ) ) )
3		subsfn	⊢ -s Fn ( No × No )
4		nnssno	⊢ ℕs ⊆ No
5		xpss12	⊢ ( ( ℕs ⊆ No ∧ ℕs ⊆ No ) → ( ℕs × ℕs ) ⊆ ( No × No ) )
6	4 4 5	mp2an	⊢ ( ℕs × ℕs ) ⊆ ( No × No )
7		ovelimab	⊢ ( ( -s Fn ( No × No ) ∧ ( ℕs × ℕs ) ⊆ ( No × No ) ) → ( 𝐴 ∈ ( -s “ ( ℕs × ℕs ) ) ↔ ∃ 𝑥 ∈ ℕs ∃ 𝑦 ∈ ℕs 𝐴 = ( 𝑥 -s 𝑦 ) ) )
8	3 6 7	mp2an	⊢ ( 𝐴 ∈ ( -s “ ( ℕs × ℕs ) ) ↔ ∃ 𝑥 ∈ ℕs ∃ 𝑦 ∈ ℕs 𝐴 = ( 𝑥 -s 𝑦 ) )
9	2 8	bitri	⊢ ( 𝐴 ∈ ℤs ↔ ∃ 𝑥 ∈ ℕs ∃ 𝑦 ∈ ℕs 𝐴 = ( 𝑥 -s 𝑦 ) )