Metamath Proof Explorer


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 )