Theorem addsfn

Description: Surreal addition is a function over pairs of surreals. (Contributed by Scott Fenton, 20-Aug-2024)

	Ref	Expression
Assertion	addsfn	⊢ +s Fn ( No × No )

Proof

Step	Hyp	Ref	Expression
1		df-adds	⊢ +s = norec2 ( ( 𝑥 ∈ V , 𝑎 ∈ V ↦ ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑙 𝑎 ( 2nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑙 ) } ) |s ( { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ ( 1st ‘ 𝑥 ) ) 𝑦 = ( 𝑟 𝑎 ( 2nd ‘ 𝑥 ) ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ ( 2nd ‘ 𝑥 ) ) 𝑧 = ( ( 1st ‘ 𝑥 ) 𝑎 𝑟 ) } ) ) ) )
2	1	norec2fn	⊢ +s Fn ( No × No )