Metamath Proof Explorer

Theorem n0ssoldg

Description: The non-negative surreal integers are a subset of the old set of _om . To avoid the axiom of infinity, we include it as an antecedent. (Contributed by Scott Fenton, 20-Feb-2026)

Ref Expression
Assertion n0ssoldg 
|- ( _om e. _V -> NN0_s C_ ( _Old ` _om ) )

Proof

Step Hyp Ref Expression
1 n0sno 
 |-  ( x e. NN0_s -> x e. No )
2 n0sbday 
 |-  ( x e. NN0_s -> ( bday ` x ) e. _om )
3 1 2 jca 
 |-  ( x e. NN0_s -> ( x e. No /\ ( bday ` x ) e. _om ) )
4 omelon2 
 |-  ( _om e. _V -> _om e. On )
5 oldbday 
 |-  ( ( _om e. On /\ x e. No ) -> ( x e. ( _Old ` _om ) <-> ( bday ` x ) e. _om ) )
6 5 biimprd 
 |-  ( ( _om e. On /\ x e. No ) -> ( ( bday ` x ) e. _om -> x e. ( _Old ` _om ) ) )
7 6 ex 
 |-  ( _om e. On -> ( x e. No -> ( ( bday ` x ) e. _om -> x e. ( _Old ` _om ) ) ) )
8 4 7 syl 
 |-  ( _om e. _V -> ( x e. No -> ( ( bday ` x ) e. _om -> x e. ( _Old ` _om ) ) ) )
9 8 impd 
 |-  ( _om e. _V -> ( ( x e. No /\ ( bday ` x ) e. _om ) -> x e. ( _Old ` _om ) ) )
10 3 9 syl5 
 |-  ( _om e. _V -> ( x e. NN0_s -> x e. ( _Old ` _om ) ) )
11 10 ssrdv 
 |-  ( _om e. _V -> NN0_s C_ ( _Old ` _om ) )