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 ) |
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 ) |