Metamath Proof Explorer

Theorem addscl

Description: Surreal numbers are closed under addition. Theorem 6(iii) of [Conway[ p. 18. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Assertion addscl 
|- ( ( A e. No /\ B e. No ) -> ( A +s B ) e. No )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. No /\ B e. No ) -> A e. No )
2 simpr 
 |-  ( ( A e. No /\ B e. No ) -> B e. No )
3 1 2 addscld 
 |-  ( ( A e. No /\ B e. No ) -> ( A +s B ) e. No )