Metamath Proof Explorer

Theorem zssno

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

Ref Expression
Assertion zssno 
|- ZZ_s C_ No

Proof

Step Hyp Ref Expression
1 imassrn 
 |-  ( -s " ( NN_s X. NN_s ) ) C_ ran -s
2 df-zs 
 |-  ZZ_s = ( -s " ( NN_s X. NN_s ) )
3 subsfo 
 |-  -s : ( No X. No ) -onto-> No
4 forn 
 |-  ( -s : ( No X. 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 
 |-  ZZ_s C_ No