Theorem zssno

Description: The surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-May-2025)

	Ref	Expression
Assertion	zssno	⊢ ℤs ⊆ No

Proof

Step	Hyp	Ref	Expression
1		imassrn	⊢ ( −s “ ( ℕs × ℕs ) ) ⊆ ran −s
2		df-zs	⊢ ℤs = ( −s “ ( ℕs × ℕs ) )
3		subsfo	⊢ −s : ( No × No ) –onto→ No
4		forn	⊢ ( −s : ( No × No ) –onto→ No → ran −s = No )
5	3 4	ax-mp	⊢ ran −s = No
6	5	eqcomi	⊢ No = ran −s
7	1 2 6	3sstr4i	⊢ ℤs ⊆ No