Theorem addscld

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

	Ref	Expression
Hypotheses	addscut.1	$$⊢\phi \to X\in \mathrm{No}$$
	addscut.2	$$⊢\phi \to Y\in \mathrm{No}$$
Assertion	addscld	Could not format assertion : No typesetting found for |- ( ph -> ( X +s Y ) e. No ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		addscut.1	$$⊢\phi \to X\in \mathrm{No}$$
2		addscut.2	$$⊢\phi \to Y\in \mathrm{No}$$
3	1 2	addscut	Could not format ( ph -> ( ( X +s Y ) e. No /\ ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) < ( ( X +s Y ) e. No /\ ( { p | E. l e. ( _Left ` X ) p = ( l +s Y ) } u. { q | E. m e. ( _Left ` Y ) q = ( X +s m ) } ) <
4	3	simp1d	Could not format ( ph -> ( X +s Y ) e. No ) : No typesetting found for |- ( ph -> ( X +s Y ) e. No ) with typecode |-