Theorem naddf

Description: Function statement for natural addition. (Contributed by Scott Fenton, 20-Jan-2025)

	Ref	Expression
Assertion	naddf	⊢ +no : ( On × On ) ⟶ On

Proof

Step	Hyp	Ref	Expression
1		naddfn	⊢ +no Fn ( On × On )
2		naddcl	⊢ ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ( 𝑦 +no 𝑧 ) ∈ On )
3	2	rgen2	⊢ ∀ 𝑦 ∈ On ∀ 𝑧 ∈ On ( 𝑦 +no 𝑧 ) ∈ On
4		fveq2	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( +no ‘ 𝑥 ) = ( +no ‘ ⟨ 𝑦 , 𝑧 ⟩ ) )
5		df-ov	⊢ ( 𝑦 +no 𝑧 ) = ( +no ‘ ⟨ 𝑦 , 𝑧 ⟩ )
6	4 5	eqtr4di	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( +no ‘ 𝑥 ) = ( 𝑦 +no 𝑧 ) )
7	6	eleq1d	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( +no ‘ 𝑥 ) ∈ On ↔ ( 𝑦 +no 𝑧 ) ∈ On ) )
8	7	ralxp	⊢ ( ∀ 𝑥 ∈ ( On × On ) ( +no ‘ 𝑥 ) ∈ On ↔ ∀ 𝑦 ∈ On ∀ 𝑧 ∈ On ( 𝑦 +no 𝑧 ) ∈ On )
9	3 8	mpbir	⊢ ∀ 𝑥 ∈ ( On × On ) ( +no ‘ 𝑥 ) ∈ On
10		ffnfv	⊢ ( +no : ( On × On ) ⟶ On ↔ ( +no Fn ( On × On ) ∧ ∀ 𝑥 ∈ ( On × On ) ( +no ‘ 𝑥 ) ∈ On ) )
11	1 9 10	mpbir2an	⊢ +no : ( On × On ) ⟶ On