Metamath Proof Explorer

Theorem onltn0s

Description: A surreal ordinal that is less than a non-negative integer is a non-negative integer. (Contributed by Scott Fenton, 7-Nov-2025)

Ref Expression
Assertion onltn0s 
|- ( ( A e. On_s /\ B e. NN0_s /\ A  A e. NN0_s )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. On_s /\ B e. NN0_s /\ A  A e. On_s )
2 n0ons 
 |-  ( B e. NN0_s -> B e. On_s )
3 onslt 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( A  ( bday ` A ) e. ( bday ` B ) ) )
4 2 3 sylan2 
 |-  ( ( A e. On_s /\ B e. NN0_s ) -> ( A  ( bday ` A ) e. ( bday ` B ) ) )
5 4 biimp3a 
 |-  ( ( A e. On_s /\ B e. NN0_s /\ A  ( bday ` A ) e. ( bday ` B ) )
6 n0sbday 
 |-  ( B e. NN0_s -> ( bday ` B ) e. _om )
7 6 3ad2ant2 
 |-  ( ( A e. On_s /\ B e. NN0_s /\ A  ( bday ` B ) e. _om )
8 elnn 
 |-  ( ( ( bday ` A ) e. ( bday ` B ) /\ ( bday ` B ) e. _om ) -> ( bday ` A ) e. _om )
9 5 7 8 syl2anc 
 |-  ( ( A e. On_s /\ B e. NN0_s /\ A  ( bday ` A ) e. _om )
10 onsfi 
 |-  ( ( A e. On_s /\ ( bday ` A ) e. _om ) -> A e. NN0_s )
11 1 9 10 syl2anc 
 |-  ( ( A e. On_s /\ B e. NN0_s /\ A  A e. NN0_s )