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	⊢ ( 𝜑 → 𝑋 ∈ No )
	addscut.2	⊢ ( 𝜑 → 𝑌 ∈ No )
Assertion	addscld	⊢ ( 𝜑 → ( 𝑋 +s 𝑌 ) ∈ No )

Proof

Step	Hyp	Ref	Expression
1		addscut.1	⊢ ( 𝜑 → 𝑋 ∈ No )
2		addscut.2	⊢ ( 𝜑 → 𝑌 ∈ No )
3	1 2	addscut	⊢ ( 𝜑 → ( ( 𝑋 +s 𝑌 ) ∈ No ∧ ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) <<s { ( 𝑋 +s 𝑌 ) } ∧ { ( 𝑋 +s 𝑌 ) } <<s ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ) )
4	3	simp1d	⊢ ( 𝜑 → ( 𝑋 +s 𝑌 ) ∈ No )