Theorem naddfn

Description: Natural addition is a function over pairs of ordinals. (Contributed by Scott Fenton, 26-Aug-2024)

	Ref	Expression
Assertion	naddfn	⊢ +no Fn ( On × On )

Proof

Step	Hyp	Ref	Expression
1		df-nadd	⊢ +no = frecs ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1st ‘ 𝑥 ) E ( 1st ‘ 𝑦 ) ∨ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) ∧ ( ( 2nd ‘ 𝑥 ) E ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } , ( On × On ) , ( 𝑧 ∈ V , 𝑎 ∈ V ↦ ∩ { 𝑤 ∈ On ∣ ( ( 𝑎 “ ( { ( 1st ‘ 𝑧 ) } × ( 2nd ‘ 𝑧 ) ) ) ⊆ 𝑤 ∧ ( 𝑎 “ ( ( 1st ‘ 𝑧 ) × { ( 2nd ‘ 𝑧 ) } ) ) ⊆ 𝑤 ) } ) )
2	1	on2recsfn	⊢ +no Fn ( On × On )